:: PARTFUN2 semantic presentation
begin
theorem Th1: :: PARTFUN2:1
for D, C being non empty set
for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f = g
proof
let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D st dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f = g
let f, g be PartFunc of C,D; ::_thesis: ( dom f = dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) implies f = g )
assume that
A1: dom f = dom g and
A2: for c being Element of C st c in dom f holds
f /. c = g /. c ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A3: x in dom f ; ::_thesis: f . x = g . x
then reconsider y = x as Element of C ;
f /. y = g /. y by A2, A3;
then f . y = g /. y by A3, PARTFUN1:def_6;
hence f . x = g . x by A1, A3, PARTFUN1:def_6; ::_thesis: verum
end;
hence f = g by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th2: :: PARTFUN2:2
for y being set
for D, C being non empty set
for f being PartFunc of C,D holds
( y in rng f iff ex c being Element of C st
( c in dom f & y = f /. c ) )
proof
let y be set ; ::_thesis: for D, C being non empty set
for f being PartFunc of C,D holds
( y in rng f iff ex c being Element of C st
( c in dom f & y = f /. c ) )
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds
( y in rng f iff ex c being Element of C st
( c in dom f & y = f /. c ) )
let f be PartFunc of C,D; ::_thesis: ( y in rng f iff ex c being Element of C st
( c in dom f & y = f /. c ) )
thus ( y in rng f implies ex c being Element of C st
( c in dom f & y = f /. c ) ) ::_thesis: ( ex c being Element of C st
( c in dom f & y = f /. c ) implies y in rng f )
proof
assume y in rng f ; ::_thesis: ex c being Element of C st
( c in dom f & y = f /. c )
then consider x being set such that
A1: x in dom f and
A2: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of C by A1;
take x ; ::_thesis: ( x in dom f & y = f /. x )
thus ( x in dom f & y = f /. x ) by A1, A2, PARTFUN1:def_6; ::_thesis: verum
end;
given c being Element of C such that A3: c in dom f and
A4: y = f /. c ; ::_thesis: y in rng f
f . c in rng f by A3, FUNCT_1:def_3;
hence y in rng f by A3, A4, PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th3: :: PARTFUN2:3
for D, E, C being non empty set
for f being PartFunc of C,D
for s being PartFunc of D,E
for h being PartFunc of C,E holds
( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )
proof
let D, E, C be non empty set ; ::_thesis: for f being PartFunc of C,D
for s being PartFunc of D,E
for h being PartFunc of C,E holds
( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )
let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E
for h being PartFunc of C,E holds
( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )
let s be PartFunc of D,E; ::_thesis: for h being PartFunc of C,E holds
( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )
let h be PartFunc of C,E; ::_thesis: ( h = s * f iff ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) )
thus ( h = s * f implies ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) ) ) ::_thesis: ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) implies h = s * f )
proof
assume A1: h = s * f ; ::_thesis: ( ( for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ) & ( for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ) )
A2: now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_dom_h_implies_(_c_in_dom_f_&_f_/._c_in_dom_s_)_)_&_(_c_in_dom_f_&_f_/._c_in_dom_s_implies_c_in_dom_h_)_)
let c be Element of C; ::_thesis: ( ( c in dom h implies ( c in dom f & f /. c in dom s ) ) & ( c in dom f & f /. c in dom s implies c in dom h ) )
thus ( c in dom h implies ( c in dom f & f /. c in dom s ) ) ::_thesis: ( c in dom f & f /. c in dom s implies c in dom h )
proof
assume c in dom h ; ::_thesis: ( c in dom f & f /. c in dom s )
then ( c in dom f & f . c in dom s ) by A1, FUNCT_1:11;
hence ( c in dom f & f /. c in dom s ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A3: c in dom f and
A4: f /. c in dom s ; ::_thesis: c in dom h
f . c in dom s by A3, A4, PARTFUN1:def_6;
hence c in dom h by A1, A3, FUNCT_1:11; ::_thesis: verum
end;
hence for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) ; ::_thesis: for c being Element of C st c in dom h holds
h /. c = s /. (f /. c)
let c be Element of C; ::_thesis: ( c in dom h implies h /. c = s /. (f /. c) )
assume A5: c in dom h ; ::_thesis: h /. c = s /. (f /. c)
then h . c = s . (f . c) by A1, FUNCT_1:12;
then A6: h /. c = s . (f . c) by A5, PARTFUN1:def_6;
c in dom f by A2, A5;
then A7: h /. c = s . (f /. c) by A6, PARTFUN1:def_6;
f /. c in dom s by A2, A5;
hence h /. c = s /. (f /. c) by A7, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A8: for c being Element of C holds
( c in dom h iff ( c in dom f & f /. c in dom s ) ) and
A9: for c being Element of C st c in dom h holds
h /. c = s /. (f /. c) ; ::_thesis: h = s * f
A10: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_h_implies_(_x_in_dom_f_&_f_._x_in_dom_s_)_)_&_(_x_in_dom_f_&_f_._x_in_dom_s_implies_x_in_dom_h_)_)
let x be set ; ::_thesis: ( ( x in dom h implies ( x in dom f & f . x in dom s ) ) & ( x in dom f & f . x in dom s implies x in dom h ) )
thus ( x in dom h implies ( x in dom f & f . x in dom s ) ) ::_thesis: ( x in dom f & f . x in dom s implies x in dom h )
proof
assume A11: x in dom h ; ::_thesis: ( x in dom f & f . x in dom s )
then reconsider y = x as Element of C ;
( y in dom f & f /. y in dom s ) by A8, A11;
hence ( x in dom f & f . x in dom s ) by PARTFUN1:def_6; ::_thesis: verum
end;
thus ( x in dom f & f . x in dom s implies x in dom h ) ::_thesis: verum
proof
assume that
A12: x in dom f and
A13: f . x in dom s ; ::_thesis: x in dom h
reconsider y = x as Element of C by A12;
f /. y in dom s by A12, A13, PARTFUN1:def_6;
hence x in dom h by A8, A12; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_s_._(f_._x)
let x be set ; ::_thesis: ( x in dom h implies h . x = s . (f . x) )
assume A14: x in dom h ; ::_thesis: h . x = s . (f . x)
then reconsider y = x as Element of C ;
h /. y = s /. (f /. y) by A9, A14;
then A15: h . y = s /. (f /. y) by A14, PARTFUN1:def_6;
f /. y in dom s by A8, A14;
then A16: h . x = s . (f /. y) by A15, PARTFUN1:def_6;
y in dom f by A8, A14;
hence h . x = s . (f . x) by A16, PARTFUN1:def_6; ::_thesis: verum
end;
hence h = s * f by A10, FUNCT_1:10; ::_thesis: verum
end;
theorem Th4: :: PARTFUN2:4
for C, D, E being non empty set
for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
proof
let C, D, E be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
let c be Element of C; ::_thesis: for f being PartFunc of C,D
for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st c in dom f & f /. c in dom s holds
(s * f) /. c = s /. (f /. c)
let s be PartFunc of D,E; ::_thesis: ( c in dom f & f /. c in dom s implies (s * f) /. c = s /. (f /. c) )
assume ( c in dom f & f /. c in dom s ) ; ::_thesis: (s * f) /. c = s /. (f /. c)
then c in dom (s * f) by Th3;
hence (s * f) /. c = s /. (f /. c) by Th3; ::_thesis: verum
end;
theorem :: PARTFUN2:5
for C, D, E being non empty set
for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
proof
let C, D, E be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let c be Element of C; ::_thesis: for f being PartFunc of C,D
for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st rng f c= dom s & c in dom f holds
(s * f) /. c = s /. (f /. c)
let s be PartFunc of D,E; ::_thesis: ( rng f c= dom s & c in dom f implies (s * f) /. c = s /. (f /. c) )
assume that
A1: rng f c= dom s and
A2: c in dom f ; ::_thesis: (s * f) /. c = s /. (f /. c)
f /. c in rng f by A2, Th2;
hence (s * f) /. c = s /. (f /. c) by A1, A2, Th4; ::_thesis: verum
end;
definition
let D be non empty set ;
let SD be Subset of D;
:: original: id
redefine func id SD -> PartFunc of D,D;
coherence
id SD is PartFunc of D,D
proof
( dom (id SD) = SD & rng (id SD) = SD ) by RELAT_1:45;
hence id SD is PartFunc of D,D by RELSET_1:4; ::_thesis: verum
end;
end;
theorem Th6: :: PARTFUN2:6
for D being non empty set
for SD being Subset of D
for F being PartFunc of D,D holds
( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )
proof
let D be non empty set ; ::_thesis: for SD being Subset of D
for F being PartFunc of D,D holds
( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )
let SD be Subset of D; ::_thesis: for F being PartFunc of D,D holds
( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )
let F be PartFunc of D,D; ::_thesis: ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )
thus ( F = id SD implies ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) ) ::_thesis: ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) implies F = id SD )
proof
assume A1: F = id SD ; ::_thesis: ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) )
hence A2: dom F = SD by RELAT_1:45; ::_thesis: for d being Element of D st d in SD holds
F /. d = d
let d be Element of D; ::_thesis: ( d in SD implies F /. d = d )
assume A3: d in SD ; ::_thesis: F /. d = d
then F . d = d by A1, FUNCT_1:18;
hence F /. d = d by A2, A3, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A4: dom F = SD and
A5: for d being Element of D st d in SD holds
F /. d = d ; ::_thesis: F = id SD
now__::_thesis:_for_x_being_set_st_x_in_SD_holds_
F_._x_=_x
let x be set ; ::_thesis: ( x in SD implies F . x = x )
assume A6: x in SD ; ::_thesis: F . x = x
then reconsider x1 = x as Element of D ;
F /. x1 = x1 by A5, A6;
hence F . x = x by A4, A6, PARTFUN1:def_6; ::_thesis: verum
end;
hence F = id SD by A4, FUNCT_1:17; ::_thesis: verum
end;
theorem :: PARTFUN2:7
for D being non empty set
for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D st d in (dom F) /\ SD holds
F /. d = (F * (id SD)) /. d
proof
let D be non empty set ; ::_thesis: for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D st d in (dom F) /\ SD holds
F /. d = (F * (id SD)) /. d
let SD be Subset of D; ::_thesis: for d being Element of D
for F being PartFunc of D,D st d in (dom F) /\ SD holds
F /. d = (F * (id SD)) /. d
let d be Element of D; ::_thesis: for F being PartFunc of D,D st d in (dom F) /\ SD holds
F /. d = (F * (id SD)) /. d
let F be PartFunc of D,D; ::_thesis: ( d in (dom F) /\ SD implies F /. d = (F * (id SD)) /. d )
assume A1: d in (dom F) /\ SD ; ::_thesis: F /. d = (F * (id SD)) /. d
then A2: d in dom F by XBOOLE_0:def_4;
F . d = (F * (id SD)) . d by A1, FUNCT_1:20;
then A3: F /. d = (F * (id SD)) . d by A2, PARTFUN1:def_6;
A4: d in SD by A1, XBOOLE_0:def_4;
then A5: d in dom (id SD) by RELAT_1:45;
(id SD) /. d in dom F by A2, A4, Th6;
then d in dom (F * (id SD)) by A5, Th3;
hence F /. d = (F * (id SD)) /. d by A3, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:8
for D being non empty set
for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
proof
let D be non empty set ; ::_thesis: for SD being Subset of D
for d being Element of D
for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let SD be Subset of D; ::_thesis: for d being Element of D
for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let d be Element of D; ::_thesis: for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let F be PartFunc of D,D; ::_thesis: ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
thus ( d in dom ((id SD) * F) implies ( d in dom F & F /. d in SD ) ) ::_thesis: ( d in dom F & F /. d in SD implies d in dom ((id SD) * F) )
proof
assume A1: d in dom ((id SD) * F) ; ::_thesis: ( d in dom F & F /. d in SD )
then F /. d in dom (id SD) by Th3;
hence ( d in dom F & F /. d in SD ) by A1, Th3, RELAT_1:45; ::_thesis: verum
end;
assume that
A2: d in dom F and
A3: F /. d in SD ; ::_thesis: d in dom ((id SD) * F)
F /. d in dom (id SD) by A3, RELAT_1:45;
hence d in dom ((id SD) * F) by A2, Th3; ::_thesis: verum
end;
theorem :: PARTFUN2:9
for D, C being non empty set
for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) holds
f is one-to-one
proof
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) holds
f is one-to-one
let f be PartFunc of C,D; ::_thesis: ( ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) implies f is one-to-one )
assume A1: for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ; ::_thesis: f is one-to-one
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_&_f_._x_=_f_._y_holds_
x_=_y
let x, y be set ; ::_thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A2: x in dom f and
A3: y in dom f and
A4: f . x = f . y ; ::_thesis: x = y
reconsider y1 = y as Element of C by A3;
reconsider x1 = x as Element of C by A2;
f /. x1 = f . y1 by A2, A4, PARTFUN1:def_6;
then f /. x1 = f /. y1 by A3, PARTFUN1:def_6;
hence x = y by A1, A2, A3; ::_thesis: verum
end;
hence f is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
theorem :: PARTFUN2:10
for x, y being set
for C, D being non empty set
for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y
proof
let x, y be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y
let f be PartFunc of C,D; ::_thesis: ( f is one-to-one & x in dom f & y in dom f & f /. x = f /. y implies x = y )
assume that
A1: f is one-to-one and
A2: x in dom f and
A3: y in dom f ; ::_thesis: ( not f /. x = f /. y or x = y )
assume f /. x = f /. y ; ::_thesis: x = y
then f . x = f /. y by A2, PARTFUN1:def_6
.= f . y by A3, PARTFUN1:def_6 ;
hence x = y by A1, A2, A3, FUNCT_1:def_4; ::_thesis: verum
end;
definition
let X, Y be set ;
let f be one-to-one PartFunc of X,Y;
:: original: "
redefine funcf " -> PartFunc of Y,X;
coherence
f " is PartFunc of Y,X by PARTFUN1:9;
end;
theorem Th11: :: PARTFUN2:11
for C, D being non empty set
for f being one-to-one PartFunc of C,D
for g being PartFunc of D,C holds
( g = f " iff ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )
proof
let C, D be non empty set ; ::_thesis: for f being one-to-one PartFunc of C,D
for g being PartFunc of D,C holds
( g = f " iff ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )
let f be one-to-one PartFunc of C,D; ::_thesis: for g being PartFunc of D,C holds
( g = f " iff ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )
let g be PartFunc of D,C; ::_thesis: ( g = f " iff ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) )
thus ( g = f " implies ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) ) ) ::_thesis: ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) implies g = f " )
proof
assume A1: g = f " ; ::_thesis: ( dom g = rng f & ( for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) ) )
hence dom g = rng f by FUNCT_1:32; ::_thesis: for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )
let d be Element of D; ::_thesis: for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )
let c be Element of C; ::_thesis: ( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) )
A2: dom g = rng f by A1, FUNCT_1:32;
thus ( d in rng f & c = g /. d implies ( c in dom f & d = f /. c ) ) ::_thesis: ( c in dom f & d = f /. c implies ( d in rng f & c = g /. d ) )
proof
assume that
A3: d in rng f and
A4: c = g /. d ; ::_thesis: ( c in dom f & d = f /. c )
c = g . d by A2, A3, A4, PARTFUN1:def_6;
then ( c in dom f & d = f . c ) by A1, A3, FUNCT_1:32;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A5: c in dom f and
A6: d = f /. c ; ::_thesis: ( d in rng f & c = g /. d )
d = f . c by A5, A6, PARTFUN1:def_6;
then ( d in rng f & c = g . d ) by A1, A5, FUNCT_1:32;
hence ( d in rng f & c = g /. d ) by A2, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A7: dom g = rng f and
A8: for d being Element of D
for c being Element of C holds
( d in rng f & c = g /. d iff ( c in dom f & d = f /. c ) ) and
A9: g <> f " ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( dom (f ") <> dom g or ex d being Element of D st
( d in dom (f ") & (f ") /. d <> g /. d ) ) by A9, Th1;
suppose dom (f ") <> dom g ; ::_thesis: contradiction
hence contradiction by A7, FUNCT_1:33; ::_thesis: verum
end;
suppose ex d being Element of D st
( d in dom (f ") & (f ") /. d <> g /. d ) ; ::_thesis: contradiction
then consider d being Element of D such that
A10: d in dom (f ") and
A11: (f ") /. d <> g /. d ;
(f ") /. d in rng (f ") by A10, Th2;
then A12: (f ") /. d in dom f by FUNCT_1:33;
d in rng f by A10, FUNCT_1:33;
then d = f . ((f ") . d) by FUNCT_1:35;
then d = f . ((f ") /. d) by A10, PARTFUN1:def_6;
then d = f /. ((f ") /. d) by A12, PARTFUN1:def_6;
hence contradiction by A8, A11, A12; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: PARTFUN2:12
for C, D being non empty set
for c being Element of C
for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
let c be Element of C; ::_thesis: for f being one-to-one PartFunc of C,D st c in dom f holds
( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
let f be one-to-one PartFunc of C,D; ::_thesis: ( c in dom f implies ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c ) )
assume A1: c in dom f ; ::_thesis: ( c = (f ") /. (f /. c) & c = ((f ") * f) /. c )
hence A2: c = (f ") /. (f /. c) by Th11; ::_thesis: c = ((f ") * f) /. c
f " = f " ;
then f /. c in rng f by A1, Th11;
then f /. c in dom (f ") by FUNCT_1:33;
hence c = ((f ") * f) /. c by A1, A2, Th4; ::_thesis: verum
end;
theorem :: PARTFUN2:13
for C, D being non empty set
for d being Element of D
for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )
proof
let C, D be non empty set ; ::_thesis: for d being Element of D
for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )
let d be Element of D; ::_thesis: for f being one-to-one PartFunc of C,D st d in rng f holds
( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )
let f be one-to-one PartFunc of C,D; ::_thesis: ( d in rng f implies ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) )
assume A1: d in rng f ; ::_thesis: ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d )
then ( d = (f * (f ")) . d & d in dom (f * (f ")) ) by FUNCT_1:35, FUNCT_1:37;
hence ( d = f /. ((f ") /. d) & d = (f * (f ")) /. d ) by A1, Th11, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:14
for C, D being non empty set
for f being PartFunc of C,D
for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ) holds
t = f "
proof
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D
for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ) holds
t = f "
let f be PartFunc of C,D; ::_thesis: for t being PartFunc of D,C st f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ) holds
t = f "
let t be PartFunc of D,C; ::_thesis: ( f is one-to-one & dom f = rng t & rng f = dom t & ( for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ) implies t = f " )
assume that
A1: ( f is one-to-one & dom f = rng t & rng f = dom t ) and
A2: for c being Element of C
for d being Element of D st c in dom f & d in dom t holds
( f /. c = d iff t /. d = c ) ; ::_thesis: t = f "
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_t_holds_
(_(_f_._x_=_y_implies_t_._y_=_x_)_&_(_t_._y_=_x_implies_f_._x_=_y_)_)
let x, y be set ; ::_thesis: ( x in dom f & y in dom t implies ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) ) )
assume that
A3: x in dom f and
A4: y in dom t ; ::_thesis: ( ( f . x = y implies t . y = x ) & ( t . y = x implies f . x = y ) )
reconsider y1 = y as Element of D by A4;
reconsider x1 = x as Element of C by A3;
thus ( f . x = y implies t . y = x ) ::_thesis: ( t . y = x implies f . x = y )
proof
assume f . x = y ; ::_thesis: t . y = x
then f /. x1 = y1 by A3, PARTFUN1:def_6;
then t /. y1 = x1 by A2, A3, A4;
hence t . y = x by A4, PARTFUN1:def_6; ::_thesis: verum
end;
assume t . y = x ; ::_thesis: f . x = y
then t /. y1 = x1 by A4, PARTFUN1:def_6;
then f /. x1 = y1 by A2, A3, A4;
hence f . x = y by A3, PARTFUN1:def_6; ::_thesis: verum
end;
hence t = f " by A1, FUNCT_1:38; ::_thesis: verum
end;
theorem Th15: :: PARTFUN2:15
for X being set
for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
proof
let X be set ; ::_thesis: for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let D, C be non empty set ; ::_thesis: for g, f being PartFunc of C,D holds
( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let g, f be PartFunc of C,D; ::_thesis: ( g = f | X iff ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
thus ( g = f | X implies ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) ) ::_thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) implies g = f | X )
proof
assume A1: g = f | X ; ::_thesis: ( dom g = (dom f) /\ X & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) )
hence dom g = (dom f) /\ X by RELAT_1:61; ::_thesis: for c being Element of C st c in dom g holds
g /. c = f /. c
let c be Element of C; ::_thesis: ( c in dom g implies g /. c = f /. c )
assume A2: c in dom g ; ::_thesis: g /. c = f /. c
then g . c = f . c by A1, FUNCT_1:47;
then A3: g /. c = f . c by A2, PARTFUN1:def_6;
dom g = (dom f) /\ X by A1, RELAT_1:61;
then c in dom f by A2, XBOOLE_0:def_4;
hence g /. c = f /. c by A3, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A4: dom g = (dom f) /\ X and
A5: for c being Element of C st c in dom g holds
g /. c = f /. c ; ::_thesis: g = f | X
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_f_._x
let x be set ; ::_thesis: ( x in dom g implies g . x = f . x )
assume A6: x in dom g ; ::_thesis: g . x = f . x
then reconsider y = x as Element of C ;
g /. y = f /. y by A5, A6;
then A7: g . y = f /. y by A6, PARTFUN1:def_6;
x in dom f by A4, A6, XBOOLE_0:def_4;
hence g . x = f . x by A7, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = f | X by A4, FUNCT_1:46; ::_thesis: verum
end;
theorem Th16: :: PARTFUN2:16
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
proof
let X be set ; ::_thesis: for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in (dom f) /\ X holds
(f | X) /. c = f /. c
let f be PartFunc of C,D; ::_thesis: ( c in (dom f) /\ X implies (f | X) /. c = f /. c )
assume c in (dom f) /\ X ; ::_thesis: (f | X) /. c = f /. c
then c in dom (f | X) by RELAT_1:61;
hence (f | X) /. c = f /. c by Th15; ::_thesis: verum
end;
theorem :: PARTFUN2:17
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
(f | X) /. c = f /. c
proof
let X be set ; ::_thesis: for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
(f | X) /. c = f /. c
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
(f | X) /. c = f /. c
let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f & c in X holds
(f | X) /. c = f /. c
let f be PartFunc of C,D; ::_thesis: ( c in dom f & c in X implies (f | X) /. c = f /. c )
assume ( c in dom f & c in X ) ; ::_thesis: (f | X) /. c = f /. c
then c in (dom f) /\ X by XBOOLE_0:def_4;
hence (f | X) /. c = f /. c by Th16; ::_thesis: verum
end;
theorem :: PARTFUN2:18
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
proof
let X be set ; ::_thesis: for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f & c in X holds
f /. c in rng (f | X)
let f be PartFunc of C,D; ::_thesis: ( c in dom f & c in X implies f /. c in rng (f | X) )
assume that
A1: c in dom f and
A2: c in X ; ::_thesis: f /. c in rng (f | X)
f . c in rng (f | X) by A1, A2, FUNCT_1:50;
hence f /. c in rng (f | X) by A1, PARTFUN1:def_6; ::_thesis: verum
end;
definition
let C, D be non empty set ;
let X be set ;
let f be PartFunc of C,D;
:: original: |`
redefine funcX |` f -> PartFunc of C,D;
coherence
X |` f is PartFunc of C,D by PARTFUN1:13;
end;
theorem Th19: :: PARTFUN2:19
for X being set
for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = X |` f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
proof
let X be set ; ::_thesis: for D, C being non empty set
for g, f being PartFunc of C,D holds
( g = X |` f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let D, C be non empty set ; ::_thesis: for g, f being PartFunc of C,D holds
( g = X |` f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
let g, f be PartFunc of C,D; ::_thesis: ( g = X |` f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )
thus ( g = X |` f implies ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) ) ::_thesis: ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) implies g = X |` f )
proof
assume A1: g = X |` f ; ::_thesis: ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) )
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_dom_g_implies_(_c_in_dom_f_&_f_/._c_in_X_)_)_&_(_c_in_dom_f_&_f_/._c_in_X_implies_c_in_dom_g_)_)
let c be Element of C; ::_thesis: ( ( c in dom g implies ( c in dom f & f /. c in X ) ) & ( c in dom f & f /. c in X implies c in dom g ) )
thus ( c in dom g implies ( c in dom f & f /. c in X ) ) ::_thesis: ( c in dom f & f /. c in X implies c in dom g )
proof
assume c in dom g ; ::_thesis: ( c in dom f & f /. c in X )
then ( c in dom f & f . c in X ) by A1, FUNCT_1:54;
hence ( c in dom f & f /. c in X ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A2: c in dom f and
A3: f /. c in X ; ::_thesis: c in dom g
f . c in X by A2, A3, PARTFUN1:def_6;
hence c in dom g by A1, A2, FUNCT_1:54; ::_thesis: verum
end;
hence for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ; ::_thesis: for c being Element of C st c in dom g holds
g /. c = f /. c
let c be Element of C; ::_thesis: ( c in dom g implies g /. c = f /. c )
assume A4: c in dom g ; ::_thesis: g /. c = f /. c
then g . c = f . c by A1, FUNCT_1:55;
then A5: g /. c = f . c by A4, PARTFUN1:def_6;
c in dom f by A1, A4, FUNCT_1:54;
hence g /. c = f /. c by A5, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A6: for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) and
A7: for c being Element of C st c in dom g holds
g /. c = f /. c ; ::_thesis: g = X |` f
A8: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_g_implies_(_x_in_dom_f_&_f_._x_in_X_)_)_&_(_x_in_dom_f_&_f_._x_in_X_implies_x_in_dom_g_)_)
let x be set ; ::_thesis: ( ( x in dom g implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in dom g ) )
thus ( x in dom g implies ( x in dom f & f . x in X ) ) ::_thesis: ( x in dom f & f . x in X implies x in dom g )
proof
assume A9: x in dom g ; ::_thesis: ( x in dom f & f . x in X )
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A6, A9;
hence ( x in dom f & f . x in X ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A10: x in dom f and
A11: f . x in X ; ::_thesis: x in dom g
reconsider x1 = x as Element of C by A10;
f /. x1 in X by A10, A11, PARTFUN1:def_6;
hence x in dom g by A6, A10; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_f_._x
let x be set ; ::_thesis: ( x in dom g implies g . x = f . x )
assume A12: x in dom g ; ::_thesis: g . x = f . x
then reconsider x1 = x as Element of C ;
g /. x1 = f /. x1 by A7, A12;
then A13: g . x1 = f /. x1 by A12, PARTFUN1:def_6;
x1 in dom f by A6, A12;
hence g . x = f . x by A13, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = X |` f by A8, FUNCT_1:53; ::_thesis: verum
end;
theorem :: PARTFUN2:20
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D holds
( c in dom (X |` f) iff ( c in dom f & f /. c in X ) ) by Th19;
theorem :: PARTFUN2:21
for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom (X |` f) holds
(X |` f) /. c = f /. c by Th19;
theorem Th22: :: PARTFUN2:22
for X being set
for D, C being non empty set
for SD being Subset of D
for f being PartFunc of C,D holds
( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )
proof
let X be set ; ::_thesis: for D, C being non empty set
for SD being Subset of D
for f being PartFunc of C,D holds
( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )
let D, C be non empty set ; ::_thesis: for SD being Subset of D
for f being PartFunc of C,D holds
( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )
let SD be Subset of D; ::_thesis: for f being PartFunc of C,D holds
( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )
let f be PartFunc of C,D; ::_thesis: ( SD = f .: X iff for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) )
thus ( SD = f .: X implies for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) ) ::_thesis: ( ( for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) ) implies SD = f .: X )
proof
assume A1: SD = f .: X ; ::_thesis: for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) )
let d be Element of D; ::_thesis: ( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) )
thus ( d in SD implies ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) ::_thesis: ( ex c being Element of C st
( c in dom f & c in X & d = f /. c ) implies d in SD )
proof
assume d in SD ; ::_thesis: ex c being Element of C st
( c in dom f & c in X & d = f /. c )
then consider x being set such that
A2: x in dom f and
A3: x in X and
A4: d = f . x by A1, FUNCT_1:def_6;
reconsider x = x as Element of C by A2;
take x ; ::_thesis: ( x in dom f & x in X & d = f /. x )
thus ( x in dom f & x in X ) by A2, A3; ::_thesis: d = f /. x
thus d = f /. x by A2, A4, PARTFUN1:def_6; ::_thesis: verum
end;
given c being Element of C such that A5: c in dom f and
A6: ( c in X & d = f /. c ) ; ::_thesis: d in SD
f /. c = f . c by A5, PARTFUN1:def_6;
hence d in SD by A1, A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
assume that
A7: for d being Element of D holds
( d in SD iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) and
A8: SD <> f .: X ; ::_thesis: contradiction
consider x being set such that
A9: ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A8, TARSKI:1;
now__::_thesis:_contradiction
percases ( ( x in SD & not x in f .: X ) or ( x in f .: X & not x in SD ) ) by A9;
supposeA10: ( x in SD & not x in f .: X ) ; ::_thesis: contradiction
then reconsider x = x as Element of D ;
consider c being Element of C such that
A11: c in dom f and
A12: c in X and
A13: x = f /. c by A7, A10;
x = f . c by A11, A13, PARTFUN1:def_6;
hence contradiction by A10, A11, A12, FUNCT_1:def_6; ::_thesis: verum
end;
supposeA14: ( x in f .: X & not x in SD ) ; ::_thesis: contradiction
then consider y being set such that
A15: y in dom f and
A16: y in X and
A17: x = f . y by FUNCT_1:def_6;
reconsider y = y as Element of C by A15;
x = f /. y by A15, A17, PARTFUN1:def_6;
hence contradiction by A7, A14, A15, A16; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: PARTFUN2:23
for X being set
for C, D being non empty set
for d being Element of D
for f being PartFunc of C,D holds
( d in f .: X iff ex c being Element of C st
( c in dom f & c in X & d = f /. c ) ) by Th22;
theorem :: PARTFUN2:24
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}
let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f holds
Im (f,c) = {(f /. c)}
let f be PartFunc of C,D; ::_thesis: ( c in dom f implies Im (f,c) = {(f /. c)} )
assume A1: c in dom f ; ::_thesis: Im (f,c) = {(f /. c)}
hence Im (f,c) = {(f . c)} by FUNCT_1:59
.= {(f /. c)} by A1, PARTFUN1:def_6 ;
::_thesis: verum
end;
theorem :: PARTFUN2:25
for C, D being non empty set
for c1, c2 being Element of C
for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}
proof
let C, D be non empty set ; ::_thesis: for c1, c2 being Element of C
for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}
let c1, c2 be Element of C; ::_thesis: for f being PartFunc of C,D st c1 in dom f & c2 in dom f holds
f .: {c1,c2} = {(f /. c1),(f /. c2)}
let f be PartFunc of C,D; ::_thesis: ( c1 in dom f & c2 in dom f implies f .: {c1,c2} = {(f /. c1),(f /. c2)} )
assume that
A1: c1 in dom f and
A2: c2 in dom f ; ::_thesis: f .: {c1,c2} = {(f /. c1),(f /. c2)}
thus f .: {c1,c2} = {(f . c1),(f . c2)} by A1, A2, FUNCT_1:60
.= {(f /. c1),(f . c2)} by A1, PARTFUN1:def_6
.= {(f /. c1),(f /. c2)} by A2, PARTFUN1:def_6 ; ::_thesis: verum
end;
theorem Th26: :: PARTFUN2:26
for X being set
for D, C being non empty set
for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
proof
let X be set ; ::_thesis: for D, C being non empty set
for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let D, C be non empty set ; ::_thesis: for SC being Subset of C
for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let SC be Subset of C; ::_thesis: for f being PartFunc of C,D holds
( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
let f be PartFunc of C,D; ::_thesis: ( SC = f " X iff for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) )
thus ( SC = f " X implies for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ) ::_thesis: ( ( for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ) implies SC = f " X )
proof
assume A1: SC = f " X ; ::_thesis: for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) )
let c be Element of C; ::_thesis: ( c in SC iff ( c in dom f & f /. c in X ) )
thus ( c in SC implies ( c in dom f & f /. c in X ) ) ::_thesis: ( c in dom f & f /. c in X implies c in SC )
proof
assume c in SC ; ::_thesis: ( c in dom f & f /. c in X )
then ( c in dom f & f . c in X ) by A1, FUNCT_1:def_7;
hence ( c in dom f & f /. c in X ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A2: c in dom f and
A3: f /. c in X ; ::_thesis: c in SC
f . c in X by A2, A3, PARTFUN1:def_6;
hence c in SC by A1, A2, FUNCT_1:def_7; ::_thesis: verum
end;
assume A4: for c being Element of C holds
( c in SC iff ( c in dom f & f /. c in X ) ) ; ::_thesis: SC = f " X
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_SC_implies_(_x_in_dom_f_&_f_._x_in_X_)_)_&_(_x_in_dom_f_&_f_._x_in_X_implies_x_in_SC_)_)
let x be set ; ::_thesis: ( ( x in SC implies ( x in dom f & f . x in X ) ) & ( x in dom f & f . x in X implies x in SC ) )
thus ( x in SC implies ( x in dom f & f . x in X ) ) ::_thesis: ( x in dom f & f . x in X implies x in SC )
proof
assume A5: x in SC ; ::_thesis: ( x in dom f & f . x in X )
then reconsider x1 = x as Element of C ;
( x1 in dom f & f /. x1 in X ) by A4, A5;
hence ( x in dom f & f . x in X ) by PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A6: x in dom f and
A7: f . x in X ; ::_thesis: x in SC
reconsider x1 = x as Element of C by A6;
f /. x1 in X by A6, A7, PARTFUN1:def_6;
hence x in SC by A4, A6; ::_thesis: verum
end;
hence SC = f " X by FUNCT_1:def_7; ::_thesis: verum
end;
theorem :: PARTFUN2:27
for D, C being non empty set
for f being PartFunc of C,D ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c
proof
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c
let f be PartFunc of C,D; ::_thesis: ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c
consider g being Function of C,D such that
A1: for x being set st x in dom f holds
g . x = f . x by FUNCT_2:71;
take g ; ::_thesis: for c being Element of C st c in dom f holds
g . c = f /. c
let c be Element of C; ::_thesis: ( c in dom f implies g . c = f /. c )
assume A2: c in dom f ; ::_thesis: g . c = f /. c
then g . c = f . c by A1;
hence g . c = f /. c by A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:28
for D, C being non empty set
for f, g being PartFunc of C,D holds
( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )
proof
let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D holds
( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )
let f, g be PartFunc of C,D; ::_thesis: ( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )
thus ( f tolerates g implies for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ) ::_thesis: ( ( for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ) implies f tolerates g )
proof
assume A1: f tolerates g ; ::_thesis: for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c
let c be Element of C; ::_thesis: ( c in (dom f) /\ (dom g) implies f /. c = g /. c )
assume A2: c in (dom f) /\ (dom g) ; ::_thesis: f /. c = g /. c
then A3: c in dom f by XBOOLE_0:def_4;
f . c = g . c by A1, A2, PARTFUN1:def_4;
then A4: f /. c = g . c by A3, PARTFUN1:def_6;
c in dom g by A2, XBOOLE_0:def_4;
hence f /. c = g /. c by A4, PARTFUN1:def_6; ::_thesis: verum
end;
assume A5: for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ; ::_thesis: f tolerates g
now__::_thesis:_for_x_being_set_st_x_in_(dom_f)_/\_(dom_g)_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A6: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of C ;
( x in dom f & f /. x1 = g /. x1 ) by A5, A6, XBOOLE_0:def_4;
then A7: f . x = g /. x1 by PARTFUN1:def_6;
x in dom g by A6, XBOOLE_0:def_4;
hence f . x = g . x by A7, PARTFUN1:def_6; ::_thesis: verum
end;
hence f tolerates g by PARTFUN1:def_4; ::_thesis: verum
end;
scheme :: PARTFUN2:sch 1
PartFuncExD{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
proof
defpred S1[ set ] means ex c being Element of F2() st P1[$1,c];
set x = the Element of F2();
defpred S2[ set , set ] means ( ( ex c being Element of F2() st P1[$1,c] implies P1[$1,$2] ) & ( ( for c being Element of F2() holds P1[$1,c] ) implies $2 = the Element of F2() ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1();
for x being set st x in X holds
x in F1() by A1;
then reconsider X = X as Subset of F1() by TARSKI:def_3;
A2: for d being Element of F1() ex z being Element of F2() st S2[d,z]
proof
let d be Element of F1(); ::_thesis: ex z being Element of F2() st S2[d,z]
( ( for c being Element of F2() holds P1[d,c] ) implies ex z being Element of F2() st
( ( ex c being Element of F2() st P1[d,c] implies P1[d,z] ) & ( ( for c being Element of F2() holds P1[d,c] ) implies z = the Element of F2() ) ) ) ;
hence ex z being Element of F2() st S2[d,z] ; ::_thesis: verum
end;
consider g being Function of F1(),F2() such that
A3: for d being Element of F1() holds S2[d,g . d] from FUNCT_2:sch_3(A2);
reconsider f = g | X as PartFunc of F1(),F2() ;
take f ; ::_thesis: ( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
A4: dom g = F1() by FUNCT_2:def_1;
thus for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ::_thesis: for d being Element of F1() st d in dom f holds
P1[d,f /. d]
proof
let d be Element of F1(); ::_thesis: ( d in dom f iff ex c being Element of F2() st P1[d,c] )
dom f c= X by RELAT_1:58;
hence ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A1; ::_thesis: ( ex c being Element of F2() st P1[d,c] implies d in dom f )
assume ex c being Element of F2() st P1[d,c] ; ::_thesis: d in dom f
then d in X by A1;
then d in (dom g) /\ X by A4, XBOOLE_0:def_4;
hence d in dom f by RELAT_1:61; ::_thesis: verum
end;
let d be Element of F1(); ::_thesis: ( d in dom f implies P1[d,f /. d] )
assume A5: d in dom f ; ::_thesis: P1[d,f /. d]
dom f c= X by RELAT_1:58;
then ex c being Element of F2() st P1[d,c] by A1, A5;
then P1[d,g . d] by A3;
then P1[d,f . d] by A5, FUNCT_1:47;
hence P1[d,f /. d] by A5, PARTFUN1:def_6; ::_thesis: verum
end;
scheme :: PARTFUN2:sch 2
LambdaPFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
ex f being PartFunc of F1(),F2() st
( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f /. d = F3(d) ) )
proof
defpred S1[ set , set ] means ( P1[$1] & $2 = F3($1) );
consider f being PartFunc of F1(),F2() such that
A1: for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st S1[d,c] ) and
A2: for d being Element of F1() st d in dom f holds
S1[d,f /. d] from PARTFUN2:sch_1();
take f ; ::_thesis: ( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f /. d = F3(d) ) )
thus for d being Element of F1() holds
( d in dom f iff P1[d] ) ::_thesis: for d being Element of F1() st d in dom f holds
f /. d = F3(d)
proof
let d be Element of F1(); ::_thesis: ( d in dom f iff P1[d] )
thus ( d in dom f implies P1[d] ) ::_thesis: ( P1[d] implies d in dom f )
proof
assume d in dom f ; ::_thesis: P1[d]
then ex c being Element of F2() st
( P1[d] & c = F3(d) ) by A1;
hence P1[d] ; ::_thesis: verum
end;
assume P1[d] ; ::_thesis: d in dom f
then ex c being Element of F2() st
( P1[d] & c = F3(d) ) ;
hence d in dom f by A1; ::_thesis: verum
end;
thus for d being Element of F1() st d in dom f holds
f /. d = F3(d) by A2; ::_thesis: verum
end;
scheme :: PARTFUN2:sch 3
UnPartFuncD{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4( set ) -> Element of F2() } :
for f, g being PartFunc of F1(),F2() st dom f = F3() & ( for c being Element of F1() st c in dom f holds
f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g /. c = F4(c) ) holds
f = g
proof
let f, g be PartFunc of F1(),F2(); ::_thesis: ( dom f = F3() & ( for c being Element of F1() st c in dom f holds
f /. c = F4(c) ) & dom g = F3() & ( for c being Element of F1() st c in dom g holds
g /. c = F4(c) ) implies f = g )
assume that
A1: dom f = F3() and
A2: for c being Element of F1() st c in dom f holds
f /. c = F4(c) and
A3: dom g = F3() and
A4: for c being Element of F1() st c in dom g holds
g /. c = F4(c) ; ::_thesis: f = g
now__::_thesis:_for_c_being_Element_of_F1()_st_c_in_dom_f_holds_
f_/._c_=_g_/._c
let c be Element of F1(); ::_thesis: ( c in dom f implies f /. c = g /. c )
assume A5: c in dom f ; ::_thesis: f /. c = g /. c
hence f /. c = F4(c) by A2
.= g /. c by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence f = g by A1, A3, Th1; ::_thesis: verum
end;
definition
let C, D be non empty set ;
let SC be Subset of C;
let d be Element of D;
:: original: -->
redefine funcSC --> d -> PartFunc of C,D;
coherence
SC --> d is PartFunc of C,D
proof
dom (SC --> d) = SC by FUNCOP_1:13;
hence SC --> d is PartFunc of C,D by RELSET_1:7; ::_thesis: verum
end;
end;
theorem Th29: :: PARTFUN2:29
for C, D being non empty set
for SC being Subset of C
for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d
proof
let C, D be non empty set ; ::_thesis: for SC being Subset of C
for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d
let SC be Subset of C; ::_thesis: for c being Element of C
for d being Element of D st c in SC holds
(SC --> d) /. c = d
let c be Element of C; ::_thesis: for d being Element of D st c in SC holds
(SC --> d) /. c = d
let d be Element of D; ::_thesis: ( c in SC implies (SC --> d) /. c = d )
assume A1: c in SC ; ::_thesis: (SC --> d) /. c = d
then ( dom (SC --> d) = SC & (SC --> d) . c = d ) by FUNCOP_1:7, FUNCOP_1:13;
hence (SC --> d) /. c = d by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:30
for D, C being non empty set
for d being Element of D
for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d
proof
let D, C be non empty set ; ::_thesis: for d being Element of D
for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d
let d be Element of D; ::_thesis: for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds
f /. c = d ) holds
f = (dom f) --> d
let f be PartFunc of C,D; ::_thesis: ( ( for c being Element of C st c in dom f holds
f /. c = d ) implies f = (dom f) --> d )
assume A1: for c being Element of C st c in dom f holds
f /. c = d ; ::_thesis: f = (dom f) --> d
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_d
let x be set ; ::_thesis: ( x in dom f implies f . x = d )
assume A2: x in dom f ; ::_thesis: f . x = d
then reconsider x1 = x as Element of C ;
f /. x1 = d by A1, A2;
hence f . x = d by A2, PARTFUN1:def_6; ::_thesis: verum
end;
hence f = (dom f) --> d by FUNCOP_1:11; ::_thesis: verum
end;
theorem :: PARTFUN2:31
for E, C, D being non empty set
for SE being Subset of E
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
proof
let E, C, D be non empty set ; ::_thesis: for SE being Subset of E
for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let SE be Subset of E; ::_thesis: for c being Element of C
for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let c be Element of C; ::_thesis: for f being PartFunc of C,D st c in dom f holds
f * (SE --> c) = SE --> (f /. c)
let f be PartFunc of C,D; ::_thesis: ( c in dom f implies f * (SE --> c) = SE --> (f /. c) )
assume A1: c in dom f ; ::_thesis: f * (SE --> c) = SE --> (f /. c)
then f * (SE --> c) = SE --> (f . c) by FUNCOP_1:17;
hence f * (SE --> c) = SE --> (f /. c) by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:32
for C being non empty set
for SC being Subset of C holds
( id SC is total iff SC = C )
proof
let C be non empty set ; ::_thesis: for SC being Subset of C holds
( id SC is total iff SC = C )
let SC be Subset of C; ::_thesis: ( id SC is total iff SC = C )
thus ( id SC is total implies SC = C ) ::_thesis: ( SC = C implies id SC is total )
proof
assume id SC is total ; ::_thesis: SC = C
then dom (id SC) = C by PARTFUN1:def_2;
hence SC = C by RELAT_1:45; ::_thesis: verum
end;
assume SC = C ; ::_thesis: id SC is total
then dom (id SC) = C by RELAT_1:45;
hence id SC is total by PARTFUN1:def_2; ::_thesis: verum
end;
theorem :: PARTFUN2:33
for C, D being non empty set
for SC being Subset of C
for d being Element of D st SC --> d is total holds
SC <> {}
proof
let C, D be non empty set ; ::_thesis: for SC being Subset of C
for d being Element of D st SC --> d is total holds
SC <> {}
let SC be Subset of C; ::_thesis: for d being Element of D st SC --> d is total holds
SC <> {}
let d be Element of D; ::_thesis: ( SC --> d is total implies SC <> {} )
assume that
A1: SC --> d is total and
A2: SC = {} ; ::_thesis: contradiction
dom (SC --> d) = C by A1, PARTFUN1:def_2;
hence contradiction by A2, FUNCOP_1:10; ::_thesis: verum
end;
theorem :: PARTFUN2:34
for D, C being non empty set
for SC being Subset of C
for d being Element of D holds
( SC --> d is total iff SC = C )
proof
let D, C be non empty set ; ::_thesis: for SC being Subset of C
for d being Element of D holds
( SC --> d is total iff SC = C )
let SC be Subset of C; ::_thesis: for d being Element of D holds
( SC --> d is total iff SC = C )
let d be Element of D; ::_thesis: ( SC --> d is total iff SC = C )
thus ( SC --> d is total implies SC = C ) ::_thesis: ( SC = C implies SC --> d is total )
proof
assume SC --> d is total ; ::_thesis: SC = C
then dom (SC --> d) = C by PARTFUN1:def_2;
hence SC = C by FUNCOP_1:13; ::_thesis: verum
end;
assume SC = C ; ::_thesis: SC --> d is total
then dom (SC --> d) = C by FUNCOP_1:13;
hence SC --> d is total by PARTFUN1:def_2; ::_thesis: verum
end;
definition
let C, D be non empty set ;
let f be PartFunc of C,D;
:: original: constant
redefine attrf is constant means :: PARTFUN2:def 1
ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d;
compatibility
( f is constant iff ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d )
proof
thus ( f is constant implies ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d ) ::_thesis: ( ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d implies f is constant )
proof
assume A1: f is constant ; ::_thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d
percases ( dom f = {} or dom f <> {} ) ;
supposeA2: dom f = {} ; ::_thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d
set d = the Element of D;
take the Element of D ; ::_thesis: for c being Element of C st c in dom f holds
f . c = the Element of D
thus for c being Element of C st c in dom f holds
f . c = the Element of D by A2; ::_thesis: verum
end;
suppose dom f <> {} ; ::_thesis: ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d
then consider c0 being set such that
A3: c0 in dom f by XBOOLE_0:def_1;
reconsider c0 = c0 as Element of C by A3;
take d = f /. c0; ::_thesis: for c being Element of C st c in dom f holds
f . c = d
let c be Element of C; ::_thesis: ( c in dom f implies f . c = d )
assume c in dom f ; ::_thesis: f . c = d
hence f . c = f . c0 by A1, A3, FUNCT_1:def_10
.= d by A3, PARTFUN1:def_6 ;
::_thesis: verum
end;
end;
end;
given d being Element of D such that A4: for c being Element of C st c in dom f holds
f . c = d ; ::_thesis: f is constant
let x, y be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume that
A5: x in dom f and
A6: y in dom f ; ::_thesis: f . x = f . y
thus f . x = d by A4, A5
.= f . y by A4, A6 ; ::_thesis: verum
end;
end;
:: deftheorem defines constant PARTFUN2:def_1_:_
for C, D being non empty set
for f being PartFunc of C,D holds
( f is constant iff ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d );
theorem Th35: :: PARTFUN2:35
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
proof
let X be set ; ::_thesis: for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d )
thus ( f | X is V8() implies ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d ) ::_thesis: ( ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d implies f | X is V8() )
proof
given d being Element of D such that A1: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d ; :: according to PARTFUN2:def_1 ::_thesis: ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f /. c = d
take d ; ::_thesis: for c being Element of C st c in X /\ (dom f) holds
f /. c = d
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d )
assume A2: c in X /\ (dom f) ; ::_thesis: f /. c = d
then A3: c in dom (f | X) by RELAT_1:61;
c in dom f by A2, XBOOLE_0:def_4;
hence f /. c = f . c by PARTFUN1:def_6
.= (f | X) . c by A3, FUNCT_1:47
.= d by A1, A3 ;
::_thesis: verum
end;
given d being Element of D such that A4: for c being Element of C st c in X /\ (dom f) holds
f /. c = d ; ::_thesis: f | X is V8()
take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d
let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d )
assume A5: c in dom (f | X) ; ::_thesis: (f | X) . c = d
then A6: c in X /\ (dom f) by RELAT_1:61;
then A7: c in dom f by XBOOLE_0:def_4;
thus (f | X) . c = f . c by A5, FUNCT_1:47
.= f /. c by A7, PARTFUN1:def_6
.= d by A4, A6 ; ::_thesis: verum
end;
theorem :: PARTFUN2:36
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 )
proof
let X be set ; ::_thesis: for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 )
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 )
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 )
thus ( f | X is V8() implies for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 ) ::_thesis: ( ( for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 ) implies f | X is V8() )
proof
assume f | X is V8() ; ::_thesis: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2
then consider d being Element of D such that
A1: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Th35;
let c1, c2 be Element of C; ::_thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f /. c1 = f /. c2 )
assume that
A2: c1 in X /\ (dom f) and
A3: c2 in X /\ (dom f) ; ::_thesis: f /. c1 = f /. c2
f /. c1 = d by A1, A2;
hence f /. c1 = f /. c2 by A1, A3; ::_thesis: verum
end;
assume A4: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f /. c1 = f /. c2 ; ::_thesis: f | X is V8()
now__::_thesis:_f_|_X_is_V8()
percases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ;
supposeA5: X /\ (dom f) = {} ; ::_thesis: f | X is V8()
now__::_thesis:_ex_d_being_Element_of_D_st_
for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_
f_/._c_=_d
set d = the Element of D;
take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds
f /. c = d
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d )
thus ( c in X /\ (dom f) implies f /. c = d ) by A5; ::_thesis: verum
end;
hence f | X is V8() by Th35; ::_thesis: verum
end;
supposeA6: X /\ (dom f) <> {} ; ::_thesis: f | X is V8()
set x = the Element of X /\ (dom f);
the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def_4;
then reconsider x = the Element of X /\ (dom f) as Element of C ;
for c being Element of C st c in X /\ (dom f) holds
f /. c = f /. x by A4;
hence f | X is V8() by Th35; ::_thesis: verum
end;
end;
end;
hence f | X is V8() ; ::_thesis: verum
end;
theorem :: PARTFUN2:37
for X being set
for C, D being non empty set
for f being PartFunc of C,D st X meets dom f holds
( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )
proof
let X be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st X meets dom f holds
( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st X meets dom f holds
( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )
let f be PartFunc of C,D; ::_thesis: ( X meets dom f implies ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) )
assume A1: X /\ (dom f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )
thus ( f | X is V8() implies ex d being Element of D st rng (f | X) = {d} ) ::_thesis: ( ex d being Element of D st rng (f | X) = {d} implies f | X is V8() )
proof
assume f | X is V8() ; ::_thesis: ex d being Element of D st rng (f | X) = {d}
then consider d being Element of D such that
A2: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Th35;
take d ; ::_thesis: rng (f | X) = {d}
thus rng (f | X) c= {d} :: according to XBOOLE_0:def_10 ::_thesis: {d} c= rng (f | X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | X) or x in {d} )
assume x in rng (f | X) ; ::_thesis: x in {d}
then consider y being set such that
A3: y in dom (f | X) and
A4: (f | X) . y = x by FUNCT_1:def_3;
reconsider y = y as Element of C by A3;
dom (f | X) = X /\ (dom f) by RELAT_1:61;
then d = f /. y by A2, A3
.= (f | X) /. y by A3, Th15
.= x by A3, A4, PARTFUN1:def_6 ;
hence x in {d} by TARSKI:def_1; ::_thesis: verum
end;
thus {d} c= rng (f | X) ::_thesis: verum
proof
set y = the Element of X /\ (dom f);
the Element of X /\ (dom f) in dom f by A1, XBOOLE_0:def_4;
then reconsider y = the Element of X /\ (dom f) as Element of C ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {d} or x in rng (f | X) )
assume A5: x in {d} ; ::_thesis: x in rng (f | X)
A6: dom (f | X) = X /\ (dom f) by RELAT_1:61;
then (f | X) /. y = f /. y by A1, Th15
.= d by A1, A2
.= x by A5, TARSKI:def_1 ;
hence x in rng (f | X) by A1, A6, Th2; ::_thesis: verum
end;
end;
given d being Element of D such that A7: rng (f | X) = {d} ; ::_thesis: f | X is V8()
take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d
let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d )
assume A8: c in dom (f | X) ; ::_thesis: (f | X) . c = d
then (f | X) /. c in {d} by A7, Th2;
then (f | X) . c in {d} by A8, PARTFUN1:def_6;
hence (f | X) . c = d by TARSKI:def_1; ::_thesis: verum
end;
theorem :: PARTFUN2:38
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & Y c= X holds
f | Y is V8()
proof
let X, Y be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & Y c= X holds
f | Y is V8()
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | X is V8() & Y c= X holds
f | Y is V8()
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() & Y c= X implies f | Y is V8() )
assume that
A1: f | X is V8() and
A2: Y c= X ; ::_thesis: f | Y is V8()
consider d being Element of D such that
A3: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by A1, Th35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_
f_/._c_=_d
let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies f /. c = d )
assume c in Y /\ (dom f) ; ::_thesis: f /. c = d
then ( c in Y & c in dom f ) by XBOOLE_0:def_4;
then c in X /\ (dom f) by A2, XBOOLE_0:def_4;
hence f /. c = d by A3; ::_thesis: verum
end;
hence f | Y is V8() by Th35; ::_thesis: verum
end;
theorem Th39: :: PARTFUN2:39
for X being set
for C, D being non empty set
for f being PartFunc of C,D st X misses dom f holds
f | X is V8()
proof
let X be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st X misses dom f holds
f | X is V8()
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st X misses dom f holds
f | X is V8()
let f be PartFunc of C,D; ::_thesis: ( X misses dom f implies f | X is V8() )
assume A1: X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X is V8()
now__::_thesis:_ex_d_being_Element_of_D_st_
for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_
f_/._c_=_d
set d = the Element of D;
take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds
f /. c = d
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f /. c = d )
thus ( c in X /\ (dom f) implies f /. c = d ) by A1; ::_thesis: verum
end;
hence f | X is V8() by Th35; ::_thesis: verum
end;
theorem :: PARTFUN2:40
for C, D being non empty set
for SC being Subset of C
for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is V8()
proof
let C, D be non empty set ; ::_thesis: for SC being Subset of C
for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is V8()
let SC be Subset of C; ::_thesis: for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is V8()
let d be Element of D; ::_thesis: for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is V8()
let f be PartFunc of C,D; ::_thesis: ( f | SC = (dom (f | SC)) --> d implies f | SC is V8() )
assume A1: f | SC = (dom (f | SC)) --> d ; ::_thesis: f | SC is V8()
now__::_thesis:_for_c_being_Element_of_C_st_c_in_SC_/\_(dom_f)_holds_
f_/._c_=_d
let c be Element of C; ::_thesis: ( c in SC /\ (dom f) implies f /. c = d )
assume c in SC /\ (dom f) ; ::_thesis: f /. c = d
then A2: c in dom (f | SC) by RELAT_1:61;
then (f | SC) /. c = d by A1, Th29;
hence f /. c = d by A2, Th15; ::_thesis: verum
end;
hence f | SC is V8() by Th35; ::_thesis: verum
end;
theorem :: PARTFUN2:41
for x being set
for C, D being non empty set
for f being PartFunc of C,D holds f | {x} is V8()
proof
let x be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D holds f | {x} is V8()
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D holds f | {x} is V8()
let f be PartFunc of C,D; ::_thesis: f | {x} is V8()
now__::_thesis:_f_|_{x}_is_V8()
percases ( {x} /\ (dom f) = {} or {x} /\ (dom f) <> {} ) ;
suppose {x} /\ (dom f) = {} ; ::_thesis: f | {x} is V8()
then {x} misses dom f by XBOOLE_0:def_7;
hence f | {x} is V8() by Th39; ::_thesis: verum
end;
supposeA1: {x} /\ (dom f) <> {} ; ::_thesis: f | {x} is V8()
set y = the Element of {x} /\ (dom f);
( the Element of {x} /\ (dom f) in {x} & the Element of {x} /\ (dom f) in dom f ) by A1, XBOOLE_0:def_4;
then reconsider x1 = x as Element of C by TARSKI:def_1;
now__::_thesis:_ex_d_being_Element_of_D_st_
for_c_being_Element_of_C_st_c_in_{x}_/\_(dom_f)_holds_
f_/._c_=_f_/._x1
take d = f /. x1; ::_thesis: for c being Element of C st c in {x} /\ (dom f) holds
f /. c = f /. x1
let c be Element of C; ::_thesis: ( c in {x} /\ (dom f) implies f /. c = f /. x1 )
assume c in {x} /\ (dom f) ; ::_thesis: f /. c = f /. x1
then c in {x} by XBOOLE_0:def_4;
hence f /. c = f /. x1 by TARSKI:def_1; ::_thesis: verum
end;
hence f | {x} is V8() by Th35; ::_thesis: verum
end;
end;
end;
hence f | {x} is V8() ; ::_thesis: verum
end;
theorem :: PARTFUN2:42
for X, Y being set
for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds
f | (X \/ Y) is V8()
proof
let X, Y be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds
f | (X \/ Y) is V8()
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds
f | (X \/ Y) is V8()
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() & f | Y is V8() & X /\ Y meets dom f implies f | (X \/ Y) is V8() )
assume that
A1: f | X is V8() and
A2: f | Y is V8() and
A3: (X /\ Y) /\ (dom f) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | (X \/ Y) is V8()
consider d1 being Element of D such that
A4: for c being Element of C st c in X /\ (dom f) holds
f /. c = d1 by A1, Th35;
set x = the Element of (X /\ Y) /\ (dom f);
A5: the Element of (X /\ Y) /\ (dom f) in X /\ Y by A3, XBOOLE_0:def_4;
A6: the Element of (X /\ Y) /\ (dom f) in dom f by A3, XBOOLE_0:def_4;
then reconsider x = the Element of (X /\ Y) /\ (dom f) as Element of C ;
x in Y by A5, XBOOLE_0:def_4;
then A7: x in Y /\ (dom f) by A6, XBOOLE_0:def_4;
consider d2 being Element of D such that
A8: for c being Element of C st c in Y /\ (dom f) holds
f /. c = d2 by A2, Th35;
x in X by A5, XBOOLE_0:def_4;
then x in X /\ (dom f) by A6, XBOOLE_0:def_4;
then f /. x = d1 by A4;
then A9: d1 = d2 by A8, A7;
take d1 ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | (X \/ Y)) holds
(f | (X \/ Y)) . c = d1
let c be Element of C; ::_thesis: ( c in dom (f | (X \/ Y)) implies (f | (X \/ Y)) . c = d1 )
assume A10: c in dom (f | (X \/ Y)) ; ::_thesis: (f | (X \/ Y)) . c = d1
then A11: c in (X \/ Y) /\ (dom f) by RELAT_1:61;
then A12: c in dom f by XBOOLE_0:def_4;
A13: c in X \/ Y by A11, XBOOLE_0:def_4;
now__::_thesis:_f_/._c_=_d1
percases ( c in X or c in Y ) by A13, XBOOLE_0:def_3;
suppose c in X ; ::_thesis: f /. c = d1
then c in X /\ (dom f) by A12, XBOOLE_0:def_4;
hence f /. c = d1 by A4; ::_thesis: verum
end;
suppose c in Y ; ::_thesis: f /. c = d1
then c in Y /\ (dom f) by A12, XBOOLE_0:def_4;
hence f /. c = d1 by A8, A9; ::_thesis: verum
end;
end;
end;
then (f | (X \/ Y)) /. c = d1 by A11, Th16;
hence (f | (X \/ Y)) . c = d1 by A10, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:43
for Y, X being set
for C, D being non empty set
for f being PartFunc of C,D st f | Y is V8() holds
(f | X) | Y is V8()
proof
let Y, X be set ; ::_thesis: for C, D being non empty set
for f being PartFunc of C,D st f | Y is V8() holds
(f | X) | Y is V8()
let C, D be non empty set ; ::_thesis: for f being PartFunc of C,D st f | Y is V8() holds
(f | X) | Y is V8()
let f be PartFunc of C,D; ::_thesis: ( f | Y is V8() implies (f | X) | Y is V8() )
assume f | Y is V8() ; ::_thesis: (f | X) | Y is V8()
then consider d being Element of D such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = d by Th35;
take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom ((f | X) | Y) holds
((f | X) | Y) . c = d
let c be Element of C; ::_thesis: ( c in dom ((f | X) | Y) implies ((f | X) | Y) . c = d )
assume A2: c in dom ((f | X) | Y) ; ::_thesis: ((f | X) | Y) . c = d
then A3: c in Y /\ (dom (f | X)) by RELAT_1:61;
then A4: c in Y by XBOOLE_0:def_4;
A5: c in dom (f | X) by A3, XBOOLE_0:def_4;
then c in (dom f) /\ X by RELAT_1:61;
then c in dom f by XBOOLE_0:def_4;
then c in Y /\ (dom f) by A4, XBOOLE_0:def_4;
then f /. c = d by A1;
then (f | X) /. c = d by A5, Th15;
then ((f | X) | Y) /. c = d by A3, Th16;
hence ((f | X) | Y) . c = d by A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:44
for C, D being non empty set
for SC being Subset of C
for d being Element of D holds (SC --> d) | SC is V8()
proof
let C, D be non empty set ; ::_thesis: for SC being Subset of C
for d being Element of D holds (SC --> d) | SC is V8()
let SC be Subset of C; ::_thesis: for d being Element of D holds (SC --> d) | SC is V8()
let d be Element of D; ::_thesis: (SC --> d) | SC is V8()
take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom ((SC --> d) | SC) holds
((SC --> d) | SC) . c = d
let c be Element of C; ::_thesis: ( c in dom ((SC --> d) | SC) implies ((SC --> d) | SC) . c = d )
assume A1: c in dom ((SC --> d) | SC) ; ::_thesis: ((SC --> d) | SC) . c = d
then A2: c in SC /\ (dom (SC --> d)) by RELAT_1:61;
then c in SC by XBOOLE_0:def_4;
then (SC --> d) /. c = d by Th29;
then ((SC --> d) | SC) /. c = d by A2, Th16;
hence ((SC --> d) | SC) . c = d by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:45
for D, C being non empty set
for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f c= g
proof
let D, C be non empty set ; ::_thesis: for f, g being PartFunc of C,D st dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) holds
f c= g
let f, g be PartFunc of C,D; ::_thesis: ( dom f c= dom g & ( for c being Element of C st c in dom f holds
f /. c = g /. c ) implies f c= g )
assume that
A1: dom f c= dom g and
A2: for c being Element of C st c in dom f holds
f /. c = g /. c ; ::_thesis: f c= g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A3: x in dom f ; ::_thesis: f . x = g . x
then reconsider x1 = x as Element of C ;
f /. x1 = g /. x1 by A2, A3;
then f . x = g /. x1 by A3, PARTFUN1:def_6;
hence f . x = g . x by A1, A3, PARTFUN1:def_6; ::_thesis: verum
end;
hence f c= g by A1, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th46: :: PARTFUN2:46
for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for d being Element of D
for f being PartFunc of C,D holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )
let c be Element of C; ::_thesis: for d being Element of D
for f being PartFunc of C,D holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )
let d be Element of D; ::_thesis: for f being PartFunc of C,D holds
( ( c in dom f & d = f /. c ) iff [c,d] in f )
let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & d = f /. c ) iff [c,d] in f )
thus ( c in dom f & d = f /. c implies [c,d] in f ) ::_thesis: ( [c,d] in f implies ( c in dom f & d = f /. c ) )
proof
assume that
A1: c in dom f and
A2: d = f /. c ; ::_thesis: [c,d] in f
d = f . c by A1, A2, PARTFUN1:def_6;
hence [c,d] in f by A1, FUNCT_1:1; ::_thesis: verum
end;
assume [c,d] in f ; ::_thesis: ( c in dom f & d = f /. c )
then ( c in dom f & d = f . c ) by FUNCT_1:1;
hence ( c in dom f & d = f /. c ) by PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:47
for C, D, E being non empty set
for c being Element of C
for e being Element of E
for f being PartFunc of C,D
for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )
proof
let C, D, E be non empty set ; ::_thesis: for c being Element of C
for e being Element of E
for f being PartFunc of C,D
for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )
let c be Element of C; ::_thesis: for e being Element of E
for f being PartFunc of C,D
for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )
let e be Element of E; ::_thesis: for f being PartFunc of C,D
for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )
let f be PartFunc of C,D; ::_thesis: for s being PartFunc of D,E st [c,e] in s * f holds
( [c,(f /. c)] in f & [(f /. c),e] in s )
let s be PartFunc of D,E; ::_thesis: ( [c,e] in s * f implies ( [c,(f /. c)] in f & [(f /. c),e] in s ) )
assume A1: [c,e] in s * f ; ::_thesis: ( [c,(f /. c)] in f & [(f /. c),e] in s )
then A2: [(f . c),e] in s by GRFUNC_1:4;
A3: [c,(f . c)] in f by A1, GRFUNC_1:4;
then c in dom f by FUNCT_1:1;
hence ( [c,(f /. c)] in f & [(f /. c),e] in s ) by A3, A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:48
for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let c be Element of C; ::_thesis: for d being Element of D
for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let d be Element of D; ::_thesis: for f being PartFunc of C,D st f = {[c,d]} holds
f /. c = d
let f be PartFunc of C,D; ::_thesis: ( f = {[c,d]} implies f /. c = d )
assume A1: f = {[c,d]} ; ::_thesis: f /. c = d
then [c,d] in f by TARSKI:def_1;
then A2: c in dom f by FUNCT_1:1;
f . c = d by A1, GRFUNC_1:6;
hence f /. c = d by A2, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:49
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st dom f = {c} holds
f = {[c,(f /. c)]}
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,D st dom f = {c} holds
f = {[c,(f /. c)]}
let c be Element of C; ::_thesis: for f being PartFunc of C,D st dom f = {c} holds
f = {[c,(f /. c)]}
let f be PartFunc of C,D; ::_thesis: ( dom f = {c} implies f = {[c,(f /. c)]} )
assume dom f = {c} ; ::_thesis: f = {[c,(f /. c)]}
then ( c in dom f & f = {[c,(f . c)]} ) by GRFUNC_1:7, TARSKI:def_1;
hence f = {[c,(f /. c)]} by PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:50
for C, D being non empty set
for c being Element of C
for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds
( f1 /. c = f /. c & f1 /. c = g /. c )
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds
( f1 /. c = f /. c & f1 /. c = g /. c )
let c be Element of C; ::_thesis: for f1, f, g being PartFunc of C,D st f1 = f /\ g & c in dom f1 holds
( f1 /. c = f /. c & f1 /. c = g /. c )
let f1, f, g be PartFunc of C,D; ::_thesis: ( f1 = f /\ g & c in dom f1 implies ( f1 /. c = f /. c & f1 /. c = g /. c ) )
assume that
A1: f1 = f /\ g and
A2: c in dom f1 ; ::_thesis: ( f1 /. c = f /. c & f1 /. c = g /. c )
f1 . c = g . c by A1, A2, GRFUNC_1:11;
then A3: f1 /. c = g . c by A2, PARTFUN1:def_6;
A4: [c,(f1 . c)] in f1 by A2, FUNCT_1:1;
then [c,(f1 . c)] in f by A1, XBOOLE_0:def_4;
then A5: c in dom f by FUNCT_1:1;
[c,(f1 . c)] in g by A1, A4, XBOOLE_0:def_4;
then A6: c in dom g by FUNCT_1:1;
f1 . c = f . c by A1, A2, GRFUNC_1:11;
then f1 /. c = f . c by A2, PARTFUN1:def_6;
hence ( f1 /. c = f /. c & f1 /. c = g /. c ) by A5, A6, A3, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:51
for C, D being non empty set
for c being Element of C
for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds
f1 /. c = f /. c
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds
f1 /. c = f /. c
let c be Element of C; ::_thesis: for f, f1, g being PartFunc of C,D st c in dom f & f1 = f \/ g holds
f1 /. c = f /. c
let f, f1, g be PartFunc of C,D; ::_thesis: ( c in dom f & f1 = f \/ g implies f1 /. c = f /. c )
assume that
A1: c in dom f and
A2: f1 = f \/ g ; ::_thesis: f1 /. c = f /. c
[c,(f . c)] in f by A1, FUNCT_1:1;
then [c,(f . c)] in f1 by A2, XBOOLE_0:def_3;
then A3: c in dom f1 by FUNCT_1:1;
f1 . c = f . c by A1, A2, GRFUNC_1:15;
then f1 /. c = f . c by A3, PARTFUN1:def_6;
hence f1 /. c = f /. c by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:52
for C, D being non empty set
for c being Element of C
for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c
let c be Element of C; ::_thesis: for g, f1, f being PartFunc of C,D st c in dom g & f1 = f \/ g holds
f1 /. c = g /. c
let g, f1, f be PartFunc of C,D; ::_thesis: ( c in dom g & f1 = f \/ g implies f1 /. c = g /. c )
assume that
A1: c in dom g and
A2: f1 = f \/ g ; ::_thesis: f1 /. c = g /. c
[c,(g . c)] in g by A1, FUNCT_1:1;
then [c,(g . c)] in f1 by A2, XBOOLE_0:def_3;
then A3: c in dom f1 by FUNCT_1:1;
f1 . c = g . c by A1, A2, GRFUNC_1:15;
then f1 /. c = g . c by A3, PARTFUN1:def_6;
hence f1 /. c = g /. c by A1, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:53
for C, D being non empty set
for c being Element of C
for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds
f1 /. c = g /. c
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds
f1 /. c = g /. c
let c be Element of C; ::_thesis: for f1, f, g being PartFunc of C,D st c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c holds
f1 /. c = g /. c
let f1, f, g be PartFunc of C,D; ::_thesis: ( c in dom f1 & f1 = f \/ g & not f1 /. c = f /. c implies f1 /. c = g /. c )
assume that
A1: c in dom f1 and
A2: f1 = f \/ g ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )
[c,(f1 /. c)] in f1 by A1, Th46;
then A3: ( [c,(f1 /. c)] in f or [c,(f1 /. c)] in g ) by A2, XBOOLE_0:def_3;
now__::_thesis:_(_f1_/._c_=_f_/._c_or_f1_/._c_=_g_/._c_)
percases ( c in dom f or c in dom g ) by A3, FUNCT_1:1;
suppose c in dom f ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )
then [c,(f /. c)] in f by Th46;
then [c,(f /. c)] in f1 by A2, XBOOLE_0:def_3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; ::_thesis: verum
end;
suppose c in dom g ; ::_thesis: ( f1 /. c = f /. c or f1 /. c = g /. c )
then [c,(g /. c)] in g by Th46;
then [c,(g /. c)] in f1 by A2, XBOOLE_0:def_3;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) by Th46; ::_thesis: verum
end;
end;
end;
hence ( f1 /. c = f /. c or f1 /. c = g /. c ) ; ::_thesis: verum
end;
theorem :: PARTFUN2:54
for C, D being non empty set
for SC being Subset of C
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )
proof
let C, D be non empty set ; ::_thesis: for SC being Subset of C
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )
let SC be Subset of C; ::_thesis: for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )
let c be Element of C; ::_thesis: for f being PartFunc of C,D holds
( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )
let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & c in SC ) iff [c,(f /. c)] in f | SC )
thus ( c in dom f & c in SC implies [c,(f /. c)] in f | SC ) ::_thesis: ( [c,(f /. c)] in f | SC implies ( c in dom f & c in SC ) )
proof
assume that
A1: c in dom f and
A2: c in SC ; ::_thesis: [c,(f /. c)] in f | SC
[c,(f . c)] in f | SC by A1, A2, GRFUNC_1:22;
hence [c,(f /. c)] in f | SC by A1, PARTFUN1:def_6; ::_thesis: verum
end;
assume [c,(f /. c)] in f | SC ; ::_thesis: ( c in dom f & c in SC )
then c in dom (f | SC) by FUNCT_1:1;
then c in (dom f) /\ SC by RELAT_1:61;
hence ( c in dom f & c in SC ) by XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: PARTFUN2:55
for C, D being non empty set
for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )
proof
let C, D be non empty set ; ::_thesis: for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )
let SD be Subset of D; ::_thesis: for c being Element of C
for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )
let c be Element of C; ::_thesis: for f being PartFunc of C,D holds
( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )
let f be PartFunc of C,D; ::_thesis: ( ( c in dom f & f /. c in SD ) iff [c,(f /. c)] in SD |` f )
thus ( c in dom f & f /. c in SD implies [c,(f /. c)] in SD |` f ) ::_thesis: ( [c,(f /. c)] in SD |` f implies ( c in dom f & f /. c in SD ) )
proof
assume that
A1: c in dom f and
A2: f /. c in SD ; ::_thesis: [c,(f /. c)] in SD |` f
f . c in SD by A1, A2, PARTFUN1:def_6;
then [c,(f . c)] in SD |` f by A1, GRFUNC_1:24;
hence [c,(f /. c)] in SD |` f by A1, PARTFUN1:def_6; ::_thesis: verum
end;
assume [c,(f /. c)] in SD |` f ; ::_thesis: ( c in dom f & f /. c in SD )
then c in dom (SD |` f) by FUNCT_1:1;
then ( c in dom f & f . c in SD ) by FUNCT_1:54;
hence ( c in dom f & f /. c in SD ) by PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: PARTFUN2:56
for C, D being non empty set
for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
proof
let C, D be non empty set ; ::_thesis: for SD being Subset of D
for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let SD be Subset of D; ::_thesis: for c being Element of C
for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let c be Element of C; ::_thesis: for f being PartFunc of C,D holds
( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
let f be PartFunc of C,D; ::_thesis: ( c in f " SD iff ( [c,(f /. c)] in f & f /. c in SD ) )
thus ( c in f " SD implies ( [c,(f /. c)] in f & f /. c in SD ) ) ::_thesis: ( [c,(f /. c)] in f & f /. c in SD implies c in f " SD )
proof
assume A1: c in f " SD ; ::_thesis: ( [c,(f /. c)] in f & f /. c in SD )
then A2: f . c in SD by GRFUNC_1:26;
A3: [c,(f . c)] in f by A1, GRFUNC_1:26;
then c in dom f by FUNCT_1:1;
hence ( [c,(f /. c)] in f & f /. c in SD ) by A3, A2, PARTFUN1:def_6; ::_thesis: verum
end;
assume that
A4: [c,(f /. c)] in f and
A5: f /. c in SD ; ::_thesis: c in f " SD
c in dom f by A4, Th46;
hence c in f " SD by A5, Th26; ::_thesis: verum
end;
theorem Th57: :: PARTFUN2:57
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d )
proof
let X be set ; ::_thesis: for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d )
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds
( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d )
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d )
hereby ::_thesis: ( ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d implies f | X is V8() )
assume f | X is V8() ; ::_thesis: ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d
then consider d being Element of D such that
A1: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Th35;
take d = d; ::_thesis: for c being Element of C st c in X /\ (dom f) holds
f . c = d
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = d )
assume A2: c in X /\ (dom f) ; ::_thesis: f . c = d
then c in dom f by XBOOLE_0:def_4;
hence f . c = f /. c by PARTFUN1:def_6
.= d by A1, A2 ;
::_thesis: verum
end;
given d being Element of D such that A3: for c being Element of C st c in X /\ (dom f) holds
f . c = d ; ::_thesis: f | X is V8()
take d ; :: according to PARTFUN2:def_1 ::_thesis: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d
let c be Element of C; ::_thesis: ( c in dom (f | X) implies (f | X) . c = d )
assume A4: c in dom (f | X) ; ::_thesis: (f | X) . c = d
then A5: c in X /\ (dom f) by RELAT_1:61;
then A6: c in dom f by XBOOLE_0:def_4;
thus (f | X) . c = (f | X) /. c by A4, PARTFUN1:def_6
.= f /. c by A5, Th16
.= f . c by A6, PARTFUN1:def_6
.= d by A3, A5 ; ::_thesis: verum
end;
theorem :: PARTFUN2:58
for X being set
for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
proof
let X be set ; ::_thesis: for D, C being non empty set
for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
let D, C be non empty set ; ::_thesis: for f being PartFunc of C,D holds
( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
let f be PartFunc of C,D; ::_thesis: ( f | X is V8() iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
thus ( f | X is V8() implies for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ) ::_thesis: ( ( for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ) implies f | X is V8() )
proof
assume f | X is V8() ; ::_thesis: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2
then consider d being Element of D such that
A1: for c being Element of C st c in X /\ (dom f) holds
f . c = d by Th57;
let c1, c2 be Element of C; ::_thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f . c1 = f . c2 )
assume that
A2: c1 in X /\ (dom f) and
A3: c2 in X /\ (dom f) ; ::_thesis: f . c1 = f . c2
f . c1 = d by A1, A2;
hence f . c1 = f . c2 by A1, A3; ::_thesis: verum
end;
assume A4: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ; ::_thesis: f | X is V8()
now__::_thesis:_f_|_X_is_V8()
percases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ;
supposeA5: X /\ (dom f) = {} ; ::_thesis: f | X is V8()
now__::_thesis:_ex_d_being_Element_of_D_st_
for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_
f_._c_=_d
set d = the Element of D;
take d = the Element of D; ::_thesis: for c being Element of C st c in X /\ (dom f) holds
f . c = d
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = d )
thus ( c in X /\ (dom f) implies f . c = d ) by A5; ::_thesis: verum
end;
hence f | X is V8() by Th57; ::_thesis: verum
end;
supposeA6: X /\ (dom f) <> {} ; ::_thesis: f | X is V8()
set x = the Element of X /\ (dom f);
now__::_thesis:_for_c_being_Element_of_C_st_c_in_X_/\_(dom_f)_holds_
f_._c_=_f_/._the_Element_of_X_/\_(dom_f)
let c be Element of C; ::_thesis: ( c in X /\ (dom f) implies f . c = f /. the Element of X /\ (dom f) )
A7: the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def_4;
assume c in X /\ (dom f) ; ::_thesis: f . c = f /. the Element of X /\ (dom f)
hence f . c = f . the Element of X /\ (dom f) by A4, A7
.= f /. the Element of X /\ (dom f) by A7, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence f | X is V8() by Th57; ::_thesis: verum
end;
end;
end;
hence f | X is V8() ; ::_thesis: verum
end;
theorem :: PARTFUN2:59
for X being set
for D, C being non empty set
for d being Element of D
for f being PartFunc of C,D st d in f .: X holds
ex c being Element of C st
( c in dom f & c in X & d = f . c )
proof
let X be set ; ::_thesis: for D, C being non empty set
for d being Element of D
for f being PartFunc of C,D st d in f .: X holds
ex c being Element of C st
( c in dom f & c in X & d = f . c )
let D, C be non empty set ; ::_thesis: for d being Element of D
for f being PartFunc of C,D st d in f .: X holds
ex c being Element of C st
( c in dom f & c in X & d = f . c )
let d be Element of D; ::_thesis: for f being PartFunc of C,D st d in f .: X holds
ex c being Element of C st
( c in dom f & c in X & d = f . c )
let f be PartFunc of C,D; ::_thesis: ( d in f .: X implies ex c being Element of C st
( c in dom f & c in X & d = f . c ) )
assume d in f .: X ; ::_thesis: ex c being Element of C st
( c in dom f & c in X & d = f . c )
then consider x being set such that
A1: x in dom f and
A2: ( x in X & d = f . x ) by FUNCT_1:def_6;
reconsider x = x as Element of C by A1;
take x ; ::_thesis: ( x in dom f & x in X & d = f . x )
thus ( x in dom f & x in X & d = f . x ) by A1, A2; ::_thesis: verum
end;
theorem :: PARTFUN2:60
for C, D being non empty set
for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )
proof
let C, D be non empty set ; ::_thesis: for c being Element of C
for d being Element of D
for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )
let c be Element of C; ::_thesis: for d being Element of D
for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )
let d be Element of D; ::_thesis: for f being PartFunc of C,D st f is one-to-one holds
( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )
let f be PartFunc of C,D; ::_thesis: ( f is one-to-one implies ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) )
A1: f " = f " ;
assume f is one-to-one ; ::_thesis: ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )
hence ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) by A1, FUNCT_1:32; ::_thesis: verum
end;
theorem :: PARTFUN2:61
for Y being set
for f, g being b1 -valued Function st f c= g holds
for x being set st x in dom f holds
f /. x = g /. x
proof
let Y be set ; ::_thesis: for f, g being Y -valued Function st f c= g holds
for x being set st x in dom f holds
f /. x = g /. x
let f, g be Y -valued Function; ::_thesis: ( f c= g implies for x being set st x in dom f holds
f /. x = g /. x )
assume A1: f c= g ; ::_thesis: for x being set st x in dom f holds
f /. x = g /. x
then A2: dom f c= dom g by GRFUNC_1:2;
let x be set ; ::_thesis: ( x in dom f implies f /. x = g /. x )
assume A3: x in dom f ; ::_thesis: f /. x = g /. x
then f . x = g . x by A1, GRFUNC_1:2;
then f /. x = g . x by A3, PARTFUN1:def_6;
hence f /. x = g /. x by A2, A3, PARTFUN1:def_6; ::_thesis: verum
end;