:: PARTFUN1 semantic presentation begin theorem Th1: :: PARTFUN1:1 for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ) holds ex h being Function st f \/ g = h proof let f, g be Function; ::_thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ) implies ex h being Function st f \/ g = h ) assume A1: for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ; ::_thesis: ex h being Function st f \/ g = h defpred S1[ set , set ] means [\$1,\$2] in f \/ g; A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume that A3: [x,y1] in f \/ g and A4: [x,y2] in f \/ g ; ::_thesis: y1 = y2 now__::_thesis:_y1_=_y2 ( [x,y1] in f or [x,y1] in g ) by A3, XBOOLE_0:def_3; then A5: ( ( x in dom f & f . x = y1 ) or ( x in dom g & g . x = y1 ) ) by FUNCT_1:1; A6: ( [x,y2] in f or [x,y2] in g ) by A4, XBOOLE_0:def_3; then A7: ( ( x in dom f & f . x = y2 ) or ( x in dom g & g . x = y2 ) ) by FUNCT_1:1; percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) ) by A6, XTUPLE_0:def_12; suppose ( x in dom f & x in dom g ) ; ::_thesis: y1 = y2 then x in (dom f) /\ (dom g) by XBOOLE_0:def_4; hence y1 = y2 by A1, A5, A7; ::_thesis: verum end; suppose ( x in dom f & not x in dom g ) ; ::_thesis: y1 = y2 hence y1 = y2 by A6, A5, FUNCT_1:1; ::_thesis: verum end; suppose ( not x in dom f & x in dom g ) ; ::_thesis: y1 = y2 hence y1 = y2 by A6, A5, FUNCT_1:1; ::_thesis: verum end; end; end; hence y1 = y2 ; ::_thesis: verum end; consider h being Function such that A8: for x, y being set holds ( [x,y] in h iff ( x in (dom f) \/ (dom g) & S1[x,y] ) ) from FUNCT_1:sch_1(A2); take h ; ::_thesis: f \/ g = h let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds ( ( not [x,b1] in f \/ g or [x,b1] in h ) & ( not [x,b1] in h or [x,b1] in f \/ g ) ) let y be set ; ::_thesis: ( ( not [x,y] in f \/ g or [x,y] in h ) & ( not [x,y] in h or [x,y] in f \/ g ) ) thus ( [x,y] in f \/ g implies [x,y] in h ) ::_thesis: ( not [x,y] in h or [x,y] in f \/ g ) proof assume A9: [x,y] in f \/ g ; ::_thesis: [x,y] in h then ( [x,y] in f or [x,y] in g ) by XBOOLE_0:def_3; then ( x in dom f or x in dom g ) by XTUPLE_0:def_12; then x in (dom f) \/ (dom g) by XBOOLE_0:def_3; hence [x,y] in h by A8, A9; ::_thesis: verum end; thus ( not [x,y] in h or [x,y] in f \/ g ) by A8; ::_thesis: verum end; theorem Th2: :: PARTFUN1:2 for f, g, h being Function st f \/ g = h holds for x being set st x in (dom f) /\ (dom g) holds f . x = g . x proof let f, g, h be Function; ::_thesis: ( f \/ g = h implies for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ) assume A1: f \/ g = h ; ::_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 A2: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x then x in dom f by XBOOLE_0:def_4; then A3: h . x = f . x by A1, GRFUNC_1:15; x in dom g by A2, XBOOLE_0:def_4; hence f . x = g . x by A1, A3, GRFUNC_1:15; ::_thesis: verum end; scheme :: PARTFUN1:sch 1 LambdaC{ F1() -> set , P1[ set ], F2( set ) -> set , F3( set ) -> set } : ex f being Function st ( dom f = F1() & ( for x being set st x in F1() holds ( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) proof defpred S1[ set , set ] means ( ( P1[\$1] implies \$2 = F2(\$1) ) & ( P1[\$1] implies \$2 = F3(\$1) ) ); A1: for x being set st x in F1() holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] ) ( P1[x] implies ( ( P1[x] implies F3(x) = F2(x) ) & ( P1[x] implies F3(x) = F3(x) ) ) ) ; hence ( x in F1() implies ex y being set st S1[x,y] ) ; ::_thesis: verum end; A2: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds y1 = y2 ; thus ex f being Function st ( dom f = F1() & ( for x being set st x in F1() holds S1[x,f . x] ) ) from FUNCT_1:sch_2(A2, A1); ::_thesis: verum end; Lm1: now__::_thesis:_for_X,_Y_being_set_ex_E_being_set_st_ (_dom_E_c=_X_&_rng_E_c=_Y_) let X, Y be set ; ::_thesis: ex E being set st ( dom E c= X & rng E c= Y ) take E = {} ; ::_thesis: ( dom E c= X & rng E c= Y ) thus ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; ::_thesis: verum end; registration let X, Y be set ; cluster Relation-like X -defined Y -valued Function-like for Element of bool [:X,Y:]; existence ex b1 being Relation of X,Y st b1 is Function-like proof consider E being Function such that A1: ( dom E c= X & rng E c= Y ) by Lm1; reconsider E = E as Relation of X,Y by A1, RELSET_1:4; take E ; ::_thesis: E is Function-like thus E is Function-like ; ::_thesis: verum end; end; definition let X, Y be set ; mode PartFunc of X,Y is Function-like Relation of X,Y; end; theorem :: PARTFUN1:3 for X, Y, y being set for f being PartFunc of X,Y st y in rng f holds ex x being Element of X st ( x in dom f & y = f . x ) proof let X, Y, y be set ; ::_thesis: for f being PartFunc of X,Y st y in rng f holds ex x being Element of X st ( x in dom f & y = f . x ) let f be PartFunc of X,Y; ::_thesis: ( y in rng f implies ex x being Element of X st ( x in dom f & y = f . x ) ) assume y in rng f ; ::_thesis: ex x being Element of X st ( x in dom f & y = f . x ) then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence ex x being Element of X st ( x in dom f & y = f . x ) ; ::_thesis: verum end; theorem Th4: :: PARTFUN1:4 for Y, x being set for f being b1 -valued Function st x in dom f holds f . x in Y proof let Y, x be set ; ::_thesis: for f being Y -valued Function st x in dom f holds f . x in Y let f be Y -valued Function; ::_thesis: ( x in dom f implies f . x in Y ) assume x in dom f ; ::_thesis: f . x in Y then A1: f . x in rng f by FUNCT_1:def_3; rng f c= Y by RELAT_1:def_19; hence f . x in Y by A1; ::_thesis: verum end; theorem :: PARTFUN1:5 for X, Y being set for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds f1 . x = f2 . x ) holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being PartFunc of X,Y st dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds f1 . x = f2 . x ) holds f1 = f2 let f1, f2 be PartFunc of X,Y; ::_thesis: ( dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds f1 . x = f2 . x ) implies f1 = f2 ) assume that A1: dom f1 = dom f2 and A2: for x being Element of X st x in dom f1 holds f1 . x = f2 . x ; ::_thesis: f1 = f2 for x being set st x in dom f1 holds f1 . x = f2 . x by A2; hence f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum end; scheme :: PARTFUN1:sch 2 PartFuncEx{ F1() -> set , F2() -> set , P1[ set , set ] } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) provided A1: for x, y being set st x in F1() & P1[x,y] holds y in F2() and A2: for x, y1, y2 being set st x in F1() & P1[x,y1] & P1[x,y2] holds y1 = y2 proof A3: now__::_thesis:_(_F2()_<>_{}_implies_ex_f_being_PartFunc_of_F1(),F2()_st_ (_(_for_x_being_set_holds_ (_x_in_dom_f_iff_(_x_in_F1()_&_ex_y_being_set_st_P1[x,y]_)_)_)_&_(_for_x_being_set_st_x_in_dom_f_holds_ P1[x,f_._x]_)_)_) defpred S1[ set ] means ex y being set st P1[\$1,y]; set y1 = the set ; assume F2() <> {} ; ::_thesis: ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) defpred S2[ set , set ] means ( ( ex y being set st P1[\$1,y] implies P1[\$1,\$2] ) & ( ( for y being set holds P1[\$1,y] ) implies \$2 = the set ) ); A4: for x being set st x in F1() holds ex z being set st S2[x,z] proof let x be set ; ::_thesis: ( x in F1() implies ex z being set st S2[x,z] ) assume x in F1() ; ::_thesis: ex z being set st S2[x,z] ( ( for y being set holds P1[x,y] ) implies ( ( ex y being set st P1[x,y] implies P1[x, the set ] ) & ( ( for y being set holds P1[x,y] ) implies the set = the set ) ) ) ; hence ex z being set st S2[x,z] ; ::_thesis: verum end; A5: for x, z1, z2 being set st x in F1() & S2[x,z1] & S2[x,z2] holds z1 = z2 by A2; consider g being Function such that A6: dom g = F1() and A7: for x being set st x in F1() holds S2[x,g . x] from FUNCT_1:sch_2(A5, A4); consider X being set such that A8: for x being set holds ( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1(); set f = g | X; A9: dom (g | X) c= F1() by A6, RELAT_1:60; rng (g | X) c= F2() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (g | X) or y in F2() ) assume y in rng (g | X) ; ::_thesis: y in F2() then consider x being set such that A10: x in dom (g | X) and A11: y = (g | X) . x by FUNCT_1:def_3; A12: dom (g | X) c= X by RELAT_1:58; then ( x in F1() & ex y being set st P1[x,y] ) by A8, A10; then P1[x,g . x] by A7; then A13: P1[x,y] by A10, A11, FUNCT_1:47; x in F1() by A8, A10, A12; hence y in F2() by A1, A13; ::_thesis: verum end; then reconsider f = g | X as PartFunc of F1(),F2() by A9, RELSET_1:4; take f = f; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) thus for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ::_thesis: for x being set st x in dom f holds P1[x,f . x] proof let x be set ; ::_thesis: ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) dom f c= X by RELAT_1:58; hence ( x in dom f implies ( x in F1() & ex y being set st P1[x,y] ) ) by A8; ::_thesis: ( x in F1() & ex y being set st P1[x,y] implies x in dom f ) assume that A14: x in F1() and A15: ex y being set st P1[x,y] ; ::_thesis: x in dom f x in X by A8, A14, A15; then x in (dom g) /\ X by A6, A14, XBOOLE_0:def_4; hence x in dom f by RELAT_1:61; ::_thesis: verum end; let x be set ; ::_thesis: ( x in dom f implies P1[x,f . x] ) assume A16: x in dom f ; ::_thesis: P1[x,f . x] dom f c= X by RELAT_1:58; then ex y being set st P1[x,y] by A8, A16; then P1[x,g . x] by A7, A16; hence P1[x,f . x] by A16, FUNCT_1:47; ::_thesis: verum end; now__::_thesis:_(_F2()_=_{}_implies_ex_f_being_PartFunc_of_F1(),F2()_st_ (_(_for_x_being_set_holds_ (_x_in_dom_f_iff_(_x_in_F1()_&_ex_y_being_set_st_P1[x,y]_)_)_)_&_(_for_x_being_set_st_x_in_dom_f_holds_ P1[x,f_._x]_)_)_) consider f being Function such that A17: ( dom f c= F1() & rng f c= F2() ) by Lm1; reconsider f = f as PartFunc of F1(),F2() by A17, RELSET_1:4; assume A18: F2() = {} ; ::_thesis: ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) take f = f; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) thus for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) by A1, A18; ::_thesis: for x being set st x in dom f holds P1[x,f . x] thus for x being set st x in dom f holds P1[x,f . x] by A18; ::_thesis: verum end; hence ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds P1[x,f . x] ) ) by A3; ::_thesis: verum end; scheme :: PARTFUN1:sch 3 LambdaR{ F1() -> set , F2() -> set , F3( set ) -> set , P1[ set ] } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & P1[x] ) ) ) & ( for x being set st x in dom f holds f . x = F3(x) ) ) provided A1: for x being set st P1[x] holds F3(x) in F2() proof defpred S1[ set , set ] means ( P1[\$1] & \$2 = F3(\$1) ); A2: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds y1 = y2 ; A3: for x, y being set st x in F1() & S1[x,y] holds y in F2() by A1; consider f being PartFunc of F1(),F2() such that A4: for x being set holds ( x in dom f iff ( x in F1() & ex y being set st S1[x,y] ) ) and A5: for x being set st x in dom f holds S1[x,f . x] from PARTFUN1:sch_2(A3, A2); take f ; ::_thesis: ( ( for x being set holds ( x in dom f iff ( x in F1() & P1[x] ) ) ) & ( for x being set st x in dom f holds f . x = F3(x) ) ) thus for x being set holds ( x in dom f iff ( x in F1() & P1[x] ) ) ::_thesis: for x being set st x in dom f holds f . x = F3(x) proof let x be set ; ::_thesis: ( x in dom f iff ( x in F1() & P1[x] ) ) thus ( x in dom f implies ( x in F1() & P1[x] ) ) ::_thesis: ( x in F1() & P1[x] implies x in dom f ) proof assume A6: x in dom f ; ::_thesis: ( x in F1() & P1[x] ) then ex y being set st ( P1[x] & y = F3(x) ) by A4; hence ( x in F1() & P1[x] ) by A6; ::_thesis: verum end; assume that A7: x in F1() and A8: P1[x] ; ::_thesis: x in dom f ex y being set st ( P1[x] & y = F3(x) ) by A8; hence x in dom f by A4, A7; ::_thesis: verum end; thus for x being set st x in dom f holds f . x = F3(x) by A5; ::_thesis: verum end; definition let X, Y, V, Z be set ; let f be PartFunc of X,Y; let g be PartFunc of V,Z; :: original: * redefine funcg * f -> PartFunc of X,Z; coherence f * g is PartFunc of X,Z proof A1: dom (g * f) c= X ; rng (g * f) c= Z by RELAT_1:def_19; hence f * g is PartFunc of X,Z by A1, RELSET_1:4; ::_thesis: verum end; end; theorem :: PARTFUN1:6 for X, Y being set for f being Relation of X,Y holds (id X) * f = f proof let X, Y be set ; ::_thesis: for f being Relation of X,Y holds (id X) * f = f let f be Relation of X,Y; ::_thesis: (id X) * f = f dom f c= X ; hence (id X) * f = f by RELAT_1:51; ::_thesis: verum end; theorem :: PARTFUN1:7 for X, Y being set for f being Relation of X,Y holds f * (id Y) = f proof let X, Y be set ; ::_thesis: for f being Relation of X,Y holds f * (id Y) = f let f be Relation of X,Y; ::_thesis: f * (id Y) = f rng f c= Y ; hence f * (id Y) = f by RELAT_1:53; ::_thesis: verum end; theorem :: PARTFUN1:8 for X, Y being set for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 ) holds f is one-to-one proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 ) holds f is one-to-one let f be PartFunc of X,Y; ::_thesis: ( ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 ) implies f is one-to-one ) assume for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 ; ::_thesis: f is one-to-one then for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 ; hence f is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; theorem :: PARTFUN1:9 for X, Y being set for f being PartFunc of X,Y st f is one-to-one holds f " is PartFunc of Y,X proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st f is one-to-one holds f " is PartFunc of Y,X let f be PartFunc of X,Y; ::_thesis: ( f is one-to-one implies f " is PartFunc of Y,X ) assume A1: f is one-to-one ; ::_thesis: f " is PartFunc of Y,X rng f c= Y by RELAT_1:def_19; then A2: dom (f ") c= Y by A1, FUNCT_1:33; dom f c= X ; then rng (f ") c= X by A1, FUNCT_1:33; hence f " is PartFunc of Y,X by A2, RELSET_1:4; ::_thesis: verum end; theorem :: PARTFUN1:10 for X, Y, Z being set for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y proof let X, Y, Z be set ; ::_thesis: for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y let f be PartFunc of X,Y; ::_thesis: f | Z is PartFunc of Z,Y ( dom (f | Z) c= Z & rng (f | Z) c= Y ) by RELAT_1:58, RELAT_1:def_19; hence f | Z is PartFunc of Z,Y by RELSET_1:4; ::_thesis: verum end; theorem Th11: :: PARTFUN1:11 for X, Y, Z being set for f being PartFunc of X,Y holds f | Z is PartFunc of X,Y ; definition let X, Y be set ; let f be PartFunc of X,Y; let Z be set ; :: original: | redefine funcf | Z -> PartFunc of X,Y; coherence f | Z is PartFunc of X,Y by Th11; end; theorem :: PARTFUN1:12 for X, Y, Z being set for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Z proof let X, Y, Z be set ; ::_thesis: for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Z let f be PartFunc of X,Y; ::_thesis: Z |` f is PartFunc of X,Z ( dom (Z |` f) c= X & rng (Z |` f) c= Z ) by RELAT_1:85; hence Z |` f is PartFunc of X,Z by RELSET_1:4; ::_thesis: verum end; theorem :: PARTFUN1:13 for X, Y, Z being set for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Y ; theorem Th14: :: PARTFUN1:14 for Y, X being set for f being Function holds (Y |` f) | X is PartFunc of X,Y proof let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X is PartFunc of X,Y let f be Function; ::_thesis: (Y |` f) | X is PartFunc of X,Y (Y |` f) | X = Y |` (f | X) by RELAT_1:109; then ( dom ((Y |` f) | X) c= X & rng ((Y |` f) | X) c= Y ) by RELAT_1:58, RELAT_1:85; hence (Y |` f) | X is PartFunc of X,Y by RELSET_1:4; ::_thesis: verum end; theorem :: PARTFUN1:15 for X, Y, y being set for f being PartFunc of X,Y st y in f .: X holds ex x being Element of X st ( x in dom f & y = f . x ) proof let X, Y, y be set ; ::_thesis: for f being PartFunc of X,Y st y in f .: X holds ex x being Element of X st ( x in dom f & y = f . x ) let f be PartFunc of X,Y; ::_thesis: ( y in f .: X implies ex x being Element of X st ( x in dom f & y = f . x ) ) assume y in f .: X ; ::_thesis: ex x being Element of X st ( x in dom f & y = f . x ) then ex x being set st ( x in dom f & x in X & y = f . x ) by FUNCT_1:def_6; hence ex x being Element of X st ( x in dom f & y = f . x ) ; ::_thesis: verum end; theorem Th16: :: PARTFUN1:16 for x, Y being set for f being PartFunc of {x},Y holds rng f c= {(f . x)} proof let x, Y be set ; ::_thesis: for f being PartFunc of {x},Y holds rng f c= {(f . x)} let f be PartFunc of {x},Y; ::_thesis: rng f c= {(f . x)} ( dom f = {} or dom f = {x} ) by ZFMISC_1:33; then ( rng f = {} or rng f = {(f . x)} ) by FUNCT_1:4, RELAT_1:42; hence rng f c= {(f . x)} by ZFMISC_1:33; ::_thesis: verum end; theorem :: PARTFUN1:17 for x, Y being set for f being PartFunc of {x},Y holds f is one-to-one proof let x, Y be set ; ::_thesis: for f being PartFunc of {x},Y holds f is one-to-one let f be PartFunc of {x},Y; ::_thesis: f is one-to-one let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in dom f or not b1 in dom f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A1: x1 in dom f and A2: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) ( dom f <> {} implies ( x1 = x & x2 = x ) ) by A1, A2, TARSKI:def_1; hence ( not f . x1 = f . x2 or x1 = x2 ) by A1; ::_thesis: verum end; theorem :: PARTFUN1:18 for x, Y, P being set for f being PartFunc of {x},Y holds f .: P c= {(f . x)} proof let x, Y, P be set ; ::_thesis: for f being PartFunc of {x},Y holds f .: P c= {(f . x)} let f be PartFunc of {x},Y; ::_thesis: f .: P c= {(f . x)} ( f .: P c= rng f & rng f c= {(f . x)} ) by Th16, RELAT_1:111; hence f .: P c= {(f . x)} by XBOOLE_1:1; ::_thesis: verum end; theorem :: PARTFUN1:19 for x, X, Y being set for f being Function st dom f = {x} & x in X & f . x in Y holds f is PartFunc of X,Y proof let x, X, Y be set ; ::_thesis: for f being Function st dom f = {x} & x in X & f . x in Y holds f is PartFunc of X,Y let f be Function; ::_thesis: ( dom f = {x} & x in X & f . x in Y implies f is PartFunc of X,Y ) assume that A1: dom f = {x} and A2: x in X and A3: f . x in Y ; ::_thesis: f is PartFunc of X,Y rng f = {(f . x)} by A1, FUNCT_1:4; then A4: rng f c= Y by A3, ZFMISC_1:31; dom f c= X by A1, A2, ZFMISC_1:31; hence f is PartFunc of X,Y by A4, RELSET_1:4; ::_thesis: verum end; theorem Th20: :: PARTFUN1:20 for X, y, x being set for f being PartFunc of X,{y} st x in dom f holds f . x = y proof let X, y, x be set ; ::_thesis: for f being PartFunc of X,{y} st x in dom f holds f . x = y let f be PartFunc of X,{y}; ::_thesis: ( x in dom f implies f . x = y ) ( x in dom f implies f . x in {y} ) by Th4; hence ( x in dom f implies f . x = y ) by TARSKI:def_1; ::_thesis: verum end; theorem :: PARTFUN1:21 for X, y being set for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds f1 = f2 proof let X, y be set ; ::_thesis: for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds f1 = f2 let f1, f2 be PartFunc of X,{y}; ::_thesis: ( dom f1 = dom f2 implies f1 = f2 ) assume A1: dom f1 = dom f2 ; ::_thesis: f1 = f2 for x being set st x in dom f1 holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume A2: x in dom f1 ; ::_thesis: f1 . x = f2 . x then f1 . x = y by Th20; hence f1 . x = f2 . x by A1, A2, Th20; ::_thesis: verum end; hence f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum end; definition let f be Function; let X, Y be set ; func<:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 1 (Y |` f) | X; coherence (Y |` f) | X is PartFunc of X,Y by Th14; end; :: deftheorem defines <: PARTFUN1:def_1_:_ for f being Function for X, Y being set holds <:f,X,Y:> = (Y |` f) | X; theorem Th22: :: PARTFUN1:22 for X, Y being set for f being Function holds <:f,X,Y:> c= f proof let X, Y be set ; ::_thesis: for f being Function holds <:f,X,Y:> c= f let f be Function; ::_thesis: <:f,X,Y:> c= f ( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86; hence <:f,X,Y:> c= f by XBOOLE_1:1; ::_thesis: verum end; theorem Th23: :: PARTFUN1:23 for X, Y being set for f being Function holds ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) proof let X, Y be set ; ::_thesis: for f being Function holds ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) let f be Function; ::_thesis: ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) <:f,X,Y:> c= f by Th22; hence ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) by RELAT_1:11; ::_thesis: verum end; theorem Th24: :: PARTFUN1:24 for x, X, Y being set for f being Function holds ( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) ) proof let x, X, Y be set ; ::_thesis: for f being Function holds ( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) ) let f be Function; ::_thesis: ( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) ) thus ( x in dom <:f,X,Y:> implies ( x in dom f & x in X & f . x in Y ) ) ::_thesis: ( x in dom f & x in X & f . x in Y implies x in dom <:f,X,Y:> ) proof assume A1: x in dom <:f,X,Y:> ; ::_thesis: ( x in dom f & x in X & f . x in Y ) then x in (dom (Y |` f)) /\ X by RELAT_1:61; then x in dom (Y |` f) by XBOOLE_0:def_4; hence ( x in dom f & x in X & f . x in Y ) by A1, FUNCT_1:54; ::_thesis: verum end; assume that A2: x in dom f and A3: x in X and A4: f . x in Y ; ::_thesis: x in dom <:f,X,Y:> x in dom (Y |` f) by A2, A4, FUNCT_1:54; then x in (dom (Y |` f)) /\ X by A3, XBOOLE_0:def_4; hence x in dom <:f,X,Y:> by RELAT_1:61; ::_thesis: verum end; theorem Th25: :: PARTFUN1:25 for x, X, Y being set for f being Function st x in dom f & x in X & f . x in Y holds <:f,X,Y:> . x = f . x proof let x, X, Y be set ; ::_thesis: for f being Function st x in dom f & x in X & f . x in Y holds <:f,X,Y:> . x = f . x let f be Function; ::_thesis: ( x in dom f & x in X & f . x in Y implies <:f,X,Y:> . x = f . x ) assume that A1: x in dom f and A2: x in X and A3: f . x in Y ; ::_thesis: <:f,X,Y:> . x = f . x x in dom (Y |` f) by A1, A3, FUNCT_1:54; then f . x = (Y |` f) . x by FUNCT_1:55 .= ((Y |` f) | X) . x by A2, FUNCT_1:49 ; hence <:f,X,Y:> . x = f . x ; ::_thesis: verum end; theorem Th26: :: PARTFUN1:26 for x, X, Y being set for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:> . x = f . x proof let x, X, Y be set ; ::_thesis: for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:> . x = f . x let f be Function; ::_thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = f . x ) assume A1: x in dom <:f,X,Y:> ; ::_thesis: <:f,X,Y:> . x = f . x then ( x in dom f & f . x in Y ) by Th24; hence <:f,X,Y:> . x = f . x by A1, Th25; ::_thesis: verum end; theorem :: PARTFUN1:27 for X, Y being set for f, g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:> proof let X, Y be set ; ::_thesis: for f, g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:> let f, g be Function; ::_thesis: ( f c= g implies <:f,X,Y:> c= <:g,X,Y:> ) assume A1: f c= g ; ::_thesis: <:f,X,Y:> c= <:g,X,Y:> A2: dom <:f,X,Y:> c= dom f by Th23; now__::_thesis:_(_dom_<:f,X,Y:>_c=_dom_<:g,X,Y:>_&_(_for_x_being_set_st_x_in_dom_<:f,X,Y:>_holds_ <:f,X,Y:>_._x_=_<:g,X,Y:>_._x_)_) thus A3: dom <:f,X,Y:> c= dom <:g,X,Y:> ::_thesis: for x being set st x in dom <:f,X,Y:> holds <:f,X,Y:> . x = <:g,X,Y:> . x proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,X,Y:> or x in dom <:g,X,Y:> ) A4: dom f c= dom g by A1, RELAT_1:11; assume A5: x in dom <:f,X,Y:> ; ::_thesis: x in dom <:g,X,Y:> then A6: f . x = g . x by A1, A2, GRFUNC_1:2; ( x in dom f & f . x in Y ) by A5, Th24; hence x in dom <:g,X,Y:> by A5, A4, A6, Th24; ::_thesis: verum end; let x be set ; ::_thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = <:g,X,Y:> . x ) assume A7: x in dom <:f,X,Y:> ; ::_thesis: <:f,X,Y:> . x = <:g,X,Y:> . x then A8: <:f,X,Y:> . x = f . x by Th26; <:g,X,Y:> . x = g . x by A3, A7, Th26; hence <:f,X,Y:> . x = <:g,X,Y:> . x by A1, A2, A7, A8, GRFUNC_1:2; ::_thesis: verum end; hence <:f,X,Y:> c= <:g,X,Y:> by GRFUNC_1:2; ::_thesis: verum end; theorem Th28: :: PARTFUN1:28 for Z, X, Y being set for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:> proof let Z, X, Y be set ; ::_thesis: for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:> let f be Function; ::_thesis: ( Z c= X implies <:f,Z,Y:> c= <:f,X,Y:> ) assume A1: Z c= X ; ::_thesis: <:f,Z,Y:> c= <:f,X,Y:> A2: dom <:f,Z,Y:> c= dom <:f,X,Y:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,Z,Y:> or x in dom <:f,X,Y:> ) assume A3: x in dom <:f,Z,Y:> ; ::_thesis: x in dom <:f,X,Y:> then A4: f . x in Y by Th24; ( x in Z & x in dom f ) by A3, Th24; hence x in dom <:f,X,Y:> by A1, A4, Th24; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_<:f,Z,Y:>_holds_ <:f,Z,Y:>_._x_=_<:f,X,Y:>_._x let x be set ; ::_thesis: ( x in dom <:f,Z,Y:> implies <:f,Z,Y:> . x = <:f,X,Y:> . x ) assume A5: x in dom <:f,Z,Y:> ; ::_thesis: <:f,Z,Y:> . x = <:f,X,Y:> . x then <:f,Z,Y:> . x = f . x by Th26; hence <:f,Z,Y:> . x = <:f,X,Y:> . x by A2, A5, Th26; ::_thesis: verum end; hence <:f,Z,Y:> c= <:f,X,Y:> by A2, GRFUNC_1:2; ::_thesis: verum end; theorem Th29: :: PARTFUN1:29 for Z, Y, X being set for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:> proof let Z, Y, X be set ; ::_thesis: for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:> let f be Function; ::_thesis: ( Z c= Y implies <:f,X,Z:> c= <:f,X,Y:> ) assume A1: Z c= Y ; ::_thesis: <:f,X,Z:> c= <:f,X,Y:> A2: dom <:f,X,Z:> c= dom <:f,X,Y:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,X,Z:> or x in dom <:f,X,Y:> ) assume A3: x in dom <:f,X,Z:> ; ::_thesis: x in dom <:f,X,Y:> then ( f . x in Z & x in dom f ) by Th24; hence x in dom <:f,X,Y:> by A1, A3, Th24; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_<:f,X,Z:>_holds_ <:f,X,Z:>_._x_=_<:f,X,Y:>_._x let x be set ; ::_thesis: ( x in dom <:f,X,Z:> implies <:f,X,Z:> . x = <:f,X,Y:> . x ) assume A4: x in dom <:f,X,Z:> ; ::_thesis: <:f,X,Z:> . x = <:f,X,Y:> . x then <:f,X,Z:> . x = f . x by Th26; hence <:f,X,Z:> . x = <:f,X,Y:> . x by A2, A4, Th26; ::_thesis: verum end; hence <:f,X,Z:> c= <:f,X,Y:> by A2, GRFUNC_1:2; ::_thesis: verum end; theorem :: PARTFUN1:30 for X1, X2, Y1, Y2 being set for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f,X2,Y2:> proof let X1, X2, Y1, Y2 be set ; ::_thesis: for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f,X2,Y2:> let f be Function; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies <:f,X1,Y1:> c= <:f,X2,Y2:> ) assume ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: <:f,X1,Y1:> c= <:f,X2,Y2:> then ( <:f,X1,Y1:> c= <:f,X2,Y1:> & <:f,X2,Y1:> c= <:f,X2,Y2:> ) by Th28, Th29; hence <:f,X1,Y1:> c= <:f,X2,Y2:> by XBOOLE_1:1; ::_thesis: verum end; theorem Th31: :: PARTFUN1:31 for X, Y being set for f being Function st dom f c= X & rng f c= Y holds f = <:f,X,Y:> proof let X, Y be set ; ::_thesis: for f being Function st dom f c= X & rng f c= Y holds f = <:f,X,Y:> let f be Function; ::_thesis: ( dom f c= X & rng f c= Y implies f = <:f,X,Y:> ) assume A1: ( dom f c= X & rng f c= Y ) ; ::_thesis: f = <:f,X,Y:> A2: dom f c= dom <:f,X,Y:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom <:f,X,Y:> ) assume A3: x in dom f ; ::_thesis: x in dom <:f,X,Y:> then f . x in rng f by FUNCT_1:def_3; hence x in dom <:f,X,Y:> by A1, A3, Th24; ::_thesis: verum end; dom <:f,X,Y:> c= dom f by Th23; then A4: dom f = dom <:f,X,Y:> by A2, XBOOLE_0:def_10; for x being set st x in dom f holds f . x = <:f,X,Y:> . x by A2, Th26; hence f = <:f,X,Y:> by A4, FUNCT_1:2; ::_thesis: verum end; theorem :: PARTFUN1:32 for f being Function holds f = <:f,(dom f),(rng f):> ; theorem :: PARTFUN1:33 for X, Y being set for f being PartFunc of X,Y holds <:f,X,Y:> = f proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds <:f,X,Y:> = f let f be PartFunc of X,Y; ::_thesis: <:f,X,Y:> = f thus <:f,X,Y:> = f ; ::_thesis: verum end; theorem Th34: :: PARTFUN1:34 for X, Y being set holds <:{},X,Y:> = {} proof let X, Y be set ; ::_thesis: <:{},X,Y:> = {} ( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2; hence <:{},X,Y:> = {} by Th31; ::_thesis: verum end; theorem Th35: :: PARTFUN1:35 for Y, Z, X being set for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> proof let Y, Z, X be set ; ::_thesis: for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> let f, g be Function; ::_thesis: <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> A1: for x being set st x in dom (<:g,Y,Z:> * <:f,X,Y:>) holds (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x proof let x be set ; ::_thesis: ( x in dom (<:g,Y,Z:> * <:f,X,Y:>) implies (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x ) assume A2: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; ::_thesis: (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x then A3: x in dom <:f,X,Y:> by FUNCT_1:11; then A4: x in dom f by Th24; <:f,X,Y:> . x in dom <:g,Y,Z:> by A2, FUNCT_1:11; then A5: f . x in dom <:g,Y,Z:> by A3, Th26; then g . (f . x) in Z by Th24; then A6: (g * f) . x in Z by A4, FUNCT_1:13; f . x in dom g by A5, Th24; then x in dom (g * f) by A4, FUNCT_1:11; then A7: x in dom <:(g * f),X,Z:> by A2, A6, Th24; thus (<:g,Y,Z:> * <:f,X,Y:>) . x = <:g,Y,Z:> . (<:f,X,Y:> . x) by A2, FUNCT_1:12 .= <:g,Y,Z:> . (f . x) by A3, Th26 .= g . (f . x) by A5, Th26 .= (g * f) . x by A4, FUNCT_1:13 .= <:(g * f),X,Z:> . x by A7, Th26 ; ::_thesis: verum end; dom (<:g,Y,Z:> * <:f,X,Y:>) c= dom <:(g * f),X,Z:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (<:g,Y,Z:> * <:f,X,Y:>) or x in dom <:(g * f),X,Z:> ) assume A8: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; ::_thesis: x in dom <:(g * f),X,Z:> then A9: x in dom <:f,X,Y:> by FUNCT_1:11; then A10: x in dom f by Th24; <:f,X,Y:> . x in dom <:g,Y,Z:> by A8, FUNCT_1:11; then A11: f . x in dom <:g,Y,Z:> by A9, Th26; then g . (f . x) in Z by Th24; then A12: (g * f) . x in Z by A10, FUNCT_1:13; f . x in dom g by A11, Th24; then x in dom (g * f) by A10, FUNCT_1:11; hence x in dom <:(g * f),X,Z:> by A8, A12, Th24; ::_thesis: verum end; hence <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> by A1, GRFUNC_1:2; ::_thesis: verum end; theorem :: PARTFUN1:36 for Y, Z, X being set for f, g being Function st (rng f) /\ (dom g) c= Y holds <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> proof let Y, Z, X be set ; ::_thesis: for f, g being Function st (rng f) /\ (dom g) c= Y holds <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> let f, g be Function; ::_thesis: ( (rng f) /\ (dom g) c= Y implies <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> ) assume A1: (rng f) /\ (dom g) c= Y ; ::_thesis: <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> A2: dom <:(g * f),X,Z:> c= dom (<:g,Y,Z:> * <:f,X,Y:>) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:(g * f),X,Z:> or x in dom (<:g,Y,Z:> * <:f,X,Y:>) ) assume A3: x in dom <:(g * f),X,Z:> ; ::_thesis: x in dom (<:g,Y,Z:> * <:f,X,Y:>) then A4: x in dom (g * f) by Th24; then A5: f . x in dom g by FUNCT_1:11; A6: x in dom f by A4, FUNCT_1:11; then f . x in rng f by FUNCT_1:def_3; then A7: f . x in (rng f) /\ (dom g) by A5, XBOOLE_0:def_4; (g * f) . x in Z by A3, Th24; then g . (f . x) in Z by A4, FUNCT_1:12; then A8: f . x in dom <:g,Y,Z:> by A1, A5, A7, Th24; ( x in dom <:f,X,Y:> & <:f,X,Y:> . x = f . x ) by A1, A3, A6, A7, Th24, Th25; hence x in dom (<:g,Y,Z:> * <:f,X,Y:>) by A8, FUNCT_1:11; ::_thesis: verum end; for x being set st x in dom <:(g * f),X,Z:> holds <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x proof let x be set ; ::_thesis: ( x in dom <:(g * f),X,Z:> implies <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x ) assume A9: x in dom <:(g * f),X,Z:> ; ::_thesis: <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x then A10: x in dom (g * f) by Th24; then A11: f . x in dom g by FUNCT_1:11; x in dom f by A10, FUNCT_1:11; then f . x in rng f by FUNCT_1:def_3; then A12: f . x in (rng f) /\ (dom g) by A11, XBOOLE_0:def_4; (g * f) . x in Z by A9, Th24; then g . (f . x) in Z by A10, FUNCT_1:12; then A13: f . x in dom <:g,Y,Z:> by A1, A11, A12, Th24; x in dom f by A10, FUNCT_1:11; then A14: x in dom <:f,X,Y:> by A1, A9, A12, Th24; thus <:(g * f),X,Z:> . x = (g * f) . x by A9, Th26 .= g . (f . x) by A10, FUNCT_1:12 .= <:g,Y,Z:> . (f . x) by A13, Th26 .= <:g,Y,Z:> . (<:f,X,Y:> . x) by A14, Th26 .= (<:g,Y,Z:> * <:f,X,Y:>) . x by A2, A9, FUNCT_1:12 ; ::_thesis: verum end; then A15: <:(g * f),X,Z:> c= <:g,Y,Z:> * <:f,X,Y:> by A2, GRFUNC_1:2; <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> by Th35; hence <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> by A15, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th37: :: PARTFUN1:37 for X, Y being set for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one proof let X, Y be set ; ::_thesis: for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one let f be Function; ::_thesis: ( f is one-to-one implies <:f,X,Y:> is one-to-one ) assume f is one-to-one ; ::_thesis: <:f,X,Y:> is one-to-one then Y |` f is one-to-one by FUNCT_1:58; hence <:f,X,Y:> is one-to-one by FUNCT_1:52; ::_thesis: verum end; theorem :: PARTFUN1:38 for X, Y being set for f being Function st f is one-to-one holds <:f,X,Y:> " = <:(f "),Y,X:> proof let X, Y be set ; ::_thesis: for f being Function st f is one-to-one holds <:f,X,Y:> " = <:(f "),Y,X:> let f be Function; ::_thesis: ( f is one-to-one implies <:f,X,Y:> " = <:(f "),Y,X:> ) assume A1: f is one-to-one ; ::_thesis: <:f,X,Y:> " = <:(f "),Y,X:> then A2: <:f,X,Y:> is one-to-one by Th37; for y being set holds ( y in dom (<:f,X,Y:> ") iff y in dom <:(f "),Y,X:> ) proof let y be set ; ::_thesis: ( y in dom (<:f,X,Y:> ") iff y in dom <:(f "),Y,X:> ) thus ( y in dom (<:f,X,Y:> ") implies y in dom <:(f "),Y,X:> ) ::_thesis: ( y in dom <:(f "),Y,X:> implies y in dom (<:f,X,Y:> ") ) proof assume y in dom (<:f,X,Y:> ") ; ::_thesis: y in dom <:(f "),Y,X:> then A3: y in rng <:f,X,Y:> by A2, FUNCT_1:33; then consider x being set such that A4: x in dom <:f,X,Y:> and A5: y = <:f,X,Y:> . x by FUNCT_1:def_3; A6: f . x = y by A4, A5, Th26; then A7: y in Y by A4, Th24; rng <:f,X,Y:> c= rng f by Th23; then y in rng f by A3; then A8: y in dom (f ") by A1, FUNCT_1:32; dom <:f,X,Y:> c= dom f by Th23; then (f ") . y = x by A1, A4, A6, FUNCT_1:32; hence y in dom <:(f "),Y,X:> by A4, A8, A7, Th24; ::_thesis: verum end; assume A9: y in dom <:(f "),Y,X:> ; ::_thesis: y in dom (<:f,X,Y:> ") dom <:(f "),Y,X:> c= dom (f ") by Th23; then y in dom (f ") by A9; then y in rng f by A1, FUNCT_1:33; then consider x being set such that A10: x in dom f and A11: y = f . x by FUNCT_1:def_3; x = (f ") . (f . x) by A1, A10, FUNCT_1:34; then x in X by A9, A11, Th24; then x in dom <:f,X,Y:> by A9, A10, A11, Th24; then ( <:f,X,Y:> . x in rng <:f,X,Y:> & <:f,X,Y:> . x = f . x ) by Th26, FUNCT_1:def_3; hence y in dom (<:f,X,Y:> ") by A2, A11, FUNCT_1:33; ::_thesis: verum end; then A12: dom (<:f,X,Y:> ") = dom <:(f "),Y,X:> by TARSKI:1; for y being set st y in dom <:(f "),Y,X:> holds <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y proof let y be set ; ::_thesis: ( y in dom <:(f "),Y,X:> implies <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y ) A13: rng <:f,X,Y:> c= rng f by Th23; assume A14: y in dom <:(f "),Y,X:> ; ::_thesis: <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y then y in rng <:f,X,Y:> by A2, A12, FUNCT_1:33; then consider x being set such that A15: x in dom f and A16: y = f . x by A13, FUNCT_1:def_3; A17: x = (f ") . (f . x) by A1, A15, FUNCT_1:34; then x in X by A14, A16, Th24; then x in dom <:f,X,Y:> by A14, A15, A16, Th24; then ( (<:f,X,Y:> ") . (<:f,X,Y:> . x) = x & <:f,X,Y:> . x = f . x ) by A2, Th26, FUNCT_1:34; hence <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y by A14, A16, A17, Th26; ::_thesis: verum end; hence <:f,X,Y:> " = <:(f "),Y,X:> by A12, FUNCT_1:2; ::_thesis: verum end; theorem :: PARTFUN1:39 for Z, X, Y being set for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):> proof let Z, X, Y be set ; ::_thesis: for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):> let f be Function; ::_thesis: Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):> thus Z |` <:f,X,Y:> = Z |` (Y |` (f | X)) by RELAT_1:109 .= (Z /\ Y) |` (f | X) by RELAT_1:96 .= <:f,X,(Z /\ Y):> by RELAT_1:109 ; ::_thesis: verum end; definition let X be set ; let f be X -defined Relation; attrf is total means :Def2: :: PARTFUN1:def 2 dom f = X; end; :: deftheorem Def2 defines total PARTFUN1:def_2_:_ for X being set for f being b1 -defined Relation holds ( f is total iff dom f = X ); registration let X be empty set ; let Y be set ; cluster -> total for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds b1 is total proof let R be Relation of X,Y; ::_thesis: R is total thus dom R = X ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; registration let X be non empty set ; let Y be empty set ; cluster -> non total for Element of bool [:X,Y:]; coherence for b1 being Relation of X,Y holds not b1 is total proof let f be Relation of X,Y; ::_thesis: not f is total assume f is total ; ::_thesis: contradiction then dom f = X by Def2; hence contradiction ; ::_thesis: verum end; end; theorem Th40: :: PARTFUN1:40 for X, Y being set for f being Function st <:f,X,Y:> is total holds X c= dom f proof let X, Y be set ; ::_thesis: for f being Function st <:f,X,Y:> is total holds X c= dom f let f be Function; ::_thesis: ( <:f,X,Y:> is total implies X c= dom f ) assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def_2 ::_thesis: X c= dom f A2: dom <:f,X,Y:> c= dom f by Th23; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom f ) assume x in X ; ::_thesis: x in dom f hence x in dom f by A1, A2; ::_thesis: verum end; theorem :: PARTFUN1:41 for X, Y being set st <:{},X,Y:> is total holds X = {} proof let X, Y be set ; ::_thesis: ( <:{},X,Y:> is total implies X = {} ) dom {} = {} ; hence ( <:{},X,Y:> is total implies X = {} ) by Th40, XBOOLE_1:3; ::_thesis: verum end; theorem :: PARTFUN1:42 for X, Y being set for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total proof let X, Y be set ; ::_thesis: for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total let f be Function; ::_thesis: ( X c= dom f & rng f c= Y implies <:f,X,Y:> is total ) assume that A1: X c= dom f and A2: rng f c= Y ; ::_thesis: <:f,X,Y:> is total X c= dom <:f,X,Y:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom <:f,X,Y:> ) assume A3: x in X ; ::_thesis: x in dom <:f,X,Y:> then f . x in rng f by A1, FUNCT_1:def_3; hence x in dom <:f,X,Y:> by A1, A2, A3, Th24; ::_thesis: verum end; hence dom <:f,X,Y:> = X by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem :: PARTFUN1:43 for X, Y being set for f being Function st <:f,X,Y:> is total holds f .: X c= Y proof let X, Y be set ; ::_thesis: for f being Function st <:f,X,Y:> is total holds f .: X c= Y let f be Function; ::_thesis: ( <:f,X,Y:> is total implies f .: X c= Y ) assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def_2 ::_thesis: f .: X c= Y let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in Y ) A2: rng <:f,X,Y:> c= Y by RELAT_1:def_19; assume y in f .: X ; ::_thesis: y in Y then consider x being set such that x in dom f and A3: ( x in X & y = f . x ) by FUNCT_1:def_6; ( <:f,X,Y:> . x = y & <:f,X,Y:> . x in rng <:f,X,Y:> ) by A1, A3, Th26, FUNCT_1:def_3; hence y in Y by A2; ::_thesis: verum end; theorem :: PARTFUN1:44 for X, Y being set for f being Function st X c= dom f & f .: X c= Y holds <:f,X,Y:> is total proof let X, Y be set ; ::_thesis: for f being Function st X c= dom f & f .: X c= Y holds <:f,X,Y:> is total let f be Function; ::_thesis: ( X c= dom f & f .: X c= Y implies <:f,X,Y:> is total ) assume that A1: X c= dom f and A2: f .: X c= Y ; ::_thesis: <:f,X,Y:> is total X c= dom <:f,X,Y:> proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom <:f,X,Y:> ) assume A3: x in X ; ::_thesis: x in dom <:f,X,Y:> then f . x in f .: X by A1, FUNCT_1:def_6; hence x in dom <:f,X,Y:> by A1, A2, A3, Th24; ::_thesis: verum end; hence dom <:f,X,Y:> = X by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; definition let X, Y be set ; func PFuncs (X,Y) -> set means :Def3: :: PARTFUN1:def 3 for x being set holds ( x in it iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) proof defpred S1[ set ] means ex f being Function st ( \$1 = f & dom f c= X & rng f c= Y ); consider F being set such that A1: for z being set holds ( z in F iff ( z in bool [:X,Y:] & S1[z] ) ) from XBOOLE_0:sch_1(); take F ; ::_thesis: for x being set holds ( x in F iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) let z be set ; ::_thesis: ( z in F iff ex f being Function st ( z = f & dom f c= X & rng f c= Y ) ) thus ( z in F implies ex f being Function st ( z = f & dom f c= X & rng f c= Y ) ) by A1; ::_thesis: ( ex f being Function st ( z = f & dom f c= X & rng f c= Y ) implies z in F ) given f being Function such that A2: z = f and A3: ( dom f c= X & rng f c= Y ) ; ::_thesis: z in F f c= [:X,Y:] proof let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds ( not [x,b1] in f or [x,b1] in [:X,Y:] ) let y be set ; ::_thesis: ( not [x,y] in f or [x,y] in [:X,Y:] ) assume A4: [x,y] in f ; ::_thesis: [x,y] in [:X,Y:] then A5: x in dom f by XTUPLE_0:def_12; then y = f . x by A4, FUNCT_1:def_2; then y in rng f by A5, FUNCT_1:def_3; hence [x,y] in [:X,Y:] by A3, A5, ZFMISC_1:def_2; ::_thesis: verum end; hence z in F by A1, A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds ( x in b2 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ) holds b1 = b2 proof let F1, F2 be set ; ::_thesis: ( ( for x being set holds ( x in F1 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds ( x in F2 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ) implies F1 = F2 ) assume that A6: for x being set holds ( x in F1 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) and A7: for x being set holds ( x in F2 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ; ::_thesis: F1 = F2 for x being set holds ( x in F1 iff x in F2 ) proof let x be set ; ::_thesis: ( x in F1 iff x in F2 ) ( x in F1 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) by A6; hence ( x in F1 iff x in F2 ) by A7; ::_thesis: verum end; hence F1 = F2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def3 defines PFuncs PARTFUN1:def_3_:_ for X, Y, b3 being set holds ( b3 = PFuncs (X,Y) iff for x being set holds ( x in b3 iff ex f being Function st ( x = f & dom f c= X & rng f c= Y ) ) ); registration let X, Y be set ; cluster PFuncs (X,Y) -> non empty ; coherence not PFuncs (X,Y) is empty proof ex f being Function st ( dom f c= X & rng f c= Y ) by Lm1; hence not PFuncs (X,Y) is empty by Def3; ::_thesis: verum end; end; theorem Th45: :: PARTFUN1:45 for X, Y being set for f being PartFunc of X,Y holds f in PFuncs (X,Y) proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds f in PFuncs (X,Y) let f be PartFunc of X,Y; ::_thesis: f in PFuncs (X,Y) ( dom f c= X & rng f c= Y ) by RELAT_1:def_19; hence f in PFuncs (X,Y) by Def3; ::_thesis: verum end; theorem Th46: :: PARTFUN1:46 for X, Y, f being set st f in PFuncs (X,Y) holds f is PartFunc of X,Y proof let X, Y, f be set ; ::_thesis: ( f in PFuncs (X,Y) implies f is PartFunc of X,Y ) assume f in PFuncs (X,Y) ; ::_thesis: f is PartFunc of X,Y then ex F being Function st ( f = F & dom F c= X & rng F c= Y ) by Def3; hence f is PartFunc of X,Y by RELSET_1:4; ::_thesis: verum end; theorem :: PARTFUN1:47 for X, Y being set for f being Element of PFuncs (X,Y) holds f is PartFunc of X,Y by Th46; theorem :: PARTFUN1:48 for Y being set holds PFuncs ({},Y) = {{}} proof let Y be set ; ::_thesis: PFuncs ({},Y) = {{}} for x being set holds ( x in PFuncs ({},Y) iff x = {} ) proof let x be set ; ::_thesis: ( x in PFuncs ({},Y) iff x = {} ) thus ( x in PFuncs ({},Y) implies x = {} ) ::_thesis: ( x = {} implies x in PFuncs ({},Y) ) proof assume x in PFuncs ({},Y) ; ::_thesis: x = {} then x is PartFunc of {},Y by Th46; hence x = {} ; ::_thesis: verum end; {} is PartFunc of {},Y by RELSET_1:12; hence ( x = {} implies x in PFuncs ({},Y) ) by Th45; ::_thesis: verum end; hence PFuncs ({},Y) = {{}} by TARSKI:def_1; ::_thesis: verum end; theorem :: PARTFUN1:49 for X being set holds PFuncs (X,{}) = {{}} proof let X be set ; ::_thesis: PFuncs (X,{}) = {{}} for x being set holds ( x in PFuncs (X,{}) iff x = {} ) proof let x be set ; ::_thesis: ( x in PFuncs (X,{}) iff x = {} ) thus ( x in PFuncs (X,{}) implies x = {} ) ::_thesis: ( x = {} implies x in PFuncs (X,{}) ) proof assume x in PFuncs (X,{}) ; ::_thesis: x = {} then x is PartFunc of X,{} by Th46; hence x = {} ; ::_thesis: verum end; {} is PartFunc of X,{} by RELSET_1:12; hence ( x = {} implies x in PFuncs (X,{}) ) by Th45; ::_thesis: verum end; hence PFuncs (X,{}) = {{}} by TARSKI:def_1; ::_thesis: verum end; theorem :: PARTFUN1:50 for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds PFuncs (X1,Y1) c= PFuncs (X2,Y2) proof let X1, X2, Y1, Y2 be set ; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies PFuncs (X1,Y1) c= PFuncs (X2,Y2) ) assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: PFuncs (X1,Y1) c= PFuncs (X2,Y2) let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in PFuncs (X1,Y1) or f in PFuncs (X2,Y2) ) assume f in PFuncs (X1,Y1) ; ::_thesis: f in PFuncs (X2,Y2) then f is PartFunc of X1,Y1 by Th46; then f is PartFunc of X2,Y2 by A1, RELSET_1:7; hence f in PFuncs (X2,Y2) by Th45; ::_thesis: verum end; definition let f, g be Function; predf tolerates g means :Def4: :: PARTFUN1:def 4 for x being set st x in (dom f) /\ (dom g) holds f . x = g . x; reflexivity for f being Function for x being set st x in (dom f) /\ (dom f) holds f . x = f . x ; symmetry for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ) holds for x being set st x in (dom g) /\ (dom f) holds g . x = f . x ; end; :: deftheorem Def4 defines tolerates PARTFUN1:def_4_:_ for f, g being Function holds ( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ); theorem Th51: :: PARTFUN1:51 for f, g being Function holds ( f tolerates g iff ex h being Function st f \/ g = h ) proof let f, g be Function; ::_thesis: ( f tolerates g iff ex h being Function st f \/ g = h ) ( ( for x being set st x in (dom f) /\ (dom g) holds f . x = g . x ) iff ex h being Function st f \/ g = h ) by Th1, Th2; hence ( f tolerates g iff ex h being Function st f \/ g = h ) by Def4; ::_thesis: verum end; theorem Th52: :: PARTFUN1:52 for f, g being Function holds ( f tolerates g iff ex h being Function st ( f c= h & g c= h ) ) proof let f, g be Function; ::_thesis: ( f tolerates g iff ex h being Function st ( f c= h & g c= h ) ) now__::_thesis:_(_(_ex_h_being_Function_st_ (_f_c=_h_&_g_c=_h_)_implies_ex_h_being_Function_st_f_\/_g_=_h_)_&_(_ex_h_being_Function_st_f_\/_g_=_h_implies_ex_h_being_Function_st_ (_f_c=_h_&_g_c=_h_)_)_) thus ( ex h being Function st ( f c= h & g c= h ) implies ex h being Function st f \/ g = h ) ::_thesis: ( ex h being Function st f \/ g = h implies ex h being Function st ( f c= h & g c= h ) ) proof given h being Function such that A1: ( f c= h & g c= h ) ; ::_thesis: ex h being Function st f \/ g = h f \/ g is Function by A1, GRFUNC_1:1, XBOOLE_1:8; hence ex h being Function st f \/ g = h ; ::_thesis: verum end; given h being Function such that A2: f \/ g = h ; ::_thesis: ex h being Function st ( f c= h & g c= h ) ( f c= h & g c= h ) by A2, XBOOLE_1:7; hence ex h being Function st ( f c= h & g c= h ) ; ::_thesis: verum end; hence ( f tolerates g iff ex h being Function st ( f c= h & g c= h ) ) by Th51; ::_thesis: verum end; theorem Th53: :: PARTFUN1:53 for f, g being Function st dom f c= dom g holds ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) proof let f, g be Function; ::_thesis: ( dom f c= dom g implies ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) ) assume dom f c= dom g ; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) then (dom f) /\ (dom g) = dom f by XBOOLE_1:28; hence ( f tolerates g iff for x being set st x in dom f holds f . x = g . x ) by Def4; ::_thesis: verum end; theorem :: PARTFUN1:54 for f, g being Function st f c= g holds f tolerates g by Th52; theorem Th55: :: PARTFUN1:55 for f, g being Function st dom f = dom g & f tolerates g holds f = g proof let f, g be Function; ::_thesis: ( dom f = dom g & f tolerates g implies f = g ) assume that A1: dom f = dom g and A2: f tolerates g ; ::_thesis: f = g for x being set st x in dom f holds f . x = g . x by A1, A2, Th53; hence f = g by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: PARTFUN1:56 for f, g being Function st dom f misses dom g holds f tolerates g proof let f, g be Function; ::_thesis: ( dom f misses dom g implies f tolerates g ) assume dom f misses dom g ; ::_thesis: f tolerates g then f \/ g is Function by GRFUNC_1:13; hence f tolerates g by Th51; ::_thesis: verum end; theorem :: PARTFUN1:57 for f, g, h being Function st f c= h & g c= h holds f tolerates g by Th52; theorem :: PARTFUN1:58 for X, Y being set for f, g being PartFunc of X,Y for h being Function st f tolerates h & g c= f holds g tolerates h proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y for h being Function st f tolerates h & g c= f holds g tolerates h let f, g be PartFunc of X,Y; ::_thesis: for h being Function st f tolerates h & g c= f holds g tolerates h let h be Function; ::_thesis: ( f tolerates h & g c= f implies g tolerates h ) assume that A1: f tolerates h and A2: g c= f ; ::_thesis: g tolerates h A3: dom g c= dom f by A2, RELAT_1:11; let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x ) assume A4: x in (dom g) /\ (dom h) ; ::_thesis: g . x = h . x then A5: x in dom g by XBOOLE_0:def_4; then A6: f . x = g . x by A2, GRFUNC_1:2; x in dom h by A4, XBOOLE_0:def_4; then x in (dom f) /\ (dom h) by A5, A3, XBOOLE_0:def_4; hence g . x = h . x by A1, A6, Def4; ::_thesis: verum end; theorem Th59: :: PARTFUN1:59 for f being Function holds {} tolerates f proof let f be Function; ::_thesis: {} tolerates f {} \/ f = f ; hence {} tolerates f by Th51; ::_thesis: verum end; theorem :: PARTFUN1:60 for X, Y being set for f being Function holds <:{},X,Y:> tolerates f proof let X, Y be set ; ::_thesis: for f being Function holds <:{},X,Y:> tolerates f let f be Function; ::_thesis: <:{},X,Y:> tolerates f <:{},X,Y:> = {} by Th34; hence <:{},X,Y:> tolerates f by Th59; ::_thesis: verum end; theorem :: PARTFUN1:61 for X, y being set for f, g being PartFunc of X,{y} holds f tolerates g proof let X, y be set ; ::_thesis: for f, g being PartFunc of X,{y} holds f tolerates g let f, g be PartFunc of X,{y}; ::_thesis: f tolerates g let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x ) assume A1: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x then x in dom f by XBOOLE_0:def_4; then A2: f . x = y by Th20; x in dom g by A1, XBOOLE_0:def_4; hence f . x = g . x by A2, Th20; ::_thesis: verum end; theorem :: PARTFUN1:62 for X being set for f being Function holds f | X tolerates f proof let X be set ; ::_thesis: for f being Function holds f | X tolerates f let f be Function; ::_thesis: f | X tolerates f f | X c= f by RELAT_1:59; hence f | X tolerates f by Th52; ::_thesis: verum end; theorem :: PARTFUN1:63 for Y being set for f being Function holds Y |` f tolerates f proof let Y be set ; ::_thesis: for f being Function holds Y |` f tolerates f let f be Function; ::_thesis: Y |` f tolerates f Y |` f c= f by RELAT_1:86; hence Y |` f tolerates f by Th52; ::_thesis: verum end; theorem Th64: :: PARTFUN1:64 for Y, X being set for f being Function holds (Y |` f) | X tolerates f proof let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X tolerates f let f be Function; ::_thesis: (Y |` f) | X tolerates f ( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86; then (Y |` f) | X c= f by XBOOLE_1:1; hence (Y |` f) | X tolerates f by Th52; ::_thesis: verum end; theorem :: PARTFUN1:65 for X, Y being set for f being Function holds <:f,X,Y:> tolerates f by Th64; theorem Th66: :: PARTFUN1:66 for X, Y being set for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds f = g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds f = g let f, g be PartFunc of X,Y; ::_thesis: ( f is total & g is total & f tolerates g implies f = g ) assume ( dom f = X & dom g = X ) ; :: according to PARTFUN1:def_2 ::_thesis: ( not f tolerates g or f = g ) hence ( not f tolerates g or f = g ) by Th55; ::_thesis: verum end; theorem Th67: :: PARTFUN1:67 for X, Y being set for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds f tolerates g proof let X, Y be set ; ::_thesis: for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds f tolerates g let f, g, h be PartFunc of X,Y; ::_thesis: ( f tolerates h & g tolerates h & h is total implies f tolerates g ) assume that A1: f tolerates h and A2: g tolerates h and A3: dom h = X ; :: according to PARTFUN1:def_2 ::_thesis: f tolerates g let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x ) assume A4: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x then x in dom f by XBOOLE_0:def_4; then x in (dom f) /\ (dom h) by A3, XBOOLE_0:def_4; then A5: f . x = h . x by A1, Def4; x in dom g by A4, XBOOLE_0:def_4; then x in (dom g) /\ (dom h) by A3, XBOOLE_0:def_4; hence f . x = g . x by A2, A5, Def4; ::_thesis: verum end; theorem Th68: :: PARTFUN1:68 for X, Y being set for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) ) assume that A1: ( Y = {} implies X = {} ) and A2: f tolerates g ; ::_thesis: ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) now__::_thesis:_ex_h_being_PartFunc_of_X,Y_st_ (_h_is_total_&_f_tolerates_h_&_g_tolerates_h_) percases ( Y = {} or Y <> {} ) ; supposeA3: Y = {} ; ::_thesis: ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) then ( f tolerates <:{},X,Y:> & g tolerates <:{},X,Y:> ) ; hence ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) by A1, A3; ::_thesis: verum end; supposeA4: Y <> {} ; ::_thesis: ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) set y = the Element of Y; defpred S1[ set , set ] means ( ( \$1 in dom f implies \$2 = f . \$1 ) & ( \$1 in dom g implies \$2 = g . \$1 ) & ( not \$1 in dom f & not \$1 in dom g implies \$2 = the Element of Y ) ); A5: for x being set st x in X holds ex y9 being set st S1[x,y9] proof let x be set ; ::_thesis: ( x in X implies ex y9 being set st S1[x,y9] ) assume x in X ; ::_thesis: ex y9 being set st S1[x,y9] now__::_thesis:_ex_y9_being_set_st_ (_(_x_in_dom_f_implies_y9_=_f_._x_)_&_(_x_in_dom_g_implies_y9_=_g_._x_)_&_(_not_x_in_dom_f_&_not_x_in_dom_g_implies_y9_=_the_Element_of_Y_)_) percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ; supposeA6: ( x in dom f & x in dom g ) ; ::_thesis: ex y9 being set st ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) take y9 = f . x; ::_thesis: ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) thus ( x in dom f implies y9 = f . x ) ; ::_thesis: ( ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4; hence ( x in dom g implies y9 = g . x ) by A2, Def4; ::_thesis: ( not x in dom f & not x in dom g implies y9 = the Element of Y ) thus ( not x in dom f & not x in dom g implies y9 = the Element of Y ) by A6; ::_thesis: verum end; supposeA7: ( x in dom f & not x in dom g ) ; ::_thesis: ex y9 being set st ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) take y9 = f . x; ::_thesis: ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) thus ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) by A7; ::_thesis: verum end; supposeA8: ( not x in dom f & x in dom g ) ; ::_thesis: ex y9 being set st ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) take y9 = g . x; ::_thesis: ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) thus ( ( x in dom f implies y9 = f . x ) & ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) ) by A8; ::_thesis: verum end; suppose ( not x in dom f & not x in dom g ) ; ::_thesis: ex y9 being set st S1[x,y9] hence ex y9 being set st S1[x,y9] ; ::_thesis: verum end; end; end; hence ex y9 being set st S1[x,y9] ; ::_thesis: verum end; A9: for x, y1, y2 being set st x in X & S1[x,y1] & S1[x,y2] holds y1 = y2 ; consider h being Function such that A10: dom h = X and A11: for x being set st x in X holds S1[x,h . x] from FUNCT_1:sch_2(A9, A5); rng h c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Y ) assume z in rng h ; ::_thesis: z in Y then consider x being set such that A12: x in dom h and A13: z = h . x by FUNCT_1:def_3; percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ; supposeA14: ( x in dom f & x in dom g ) ; ::_thesis: z in Y then z = f . x by A11, A13; hence z in Y by A14, Th4; ::_thesis: verum end; supposeA15: ( x in dom f & not x in dom g ) ; ::_thesis: z in Y then z = f . x by A11, A13; hence z in Y by A15, Th4; ::_thesis: verum end; supposeA16: ( not x in dom f & x in dom g ) ; ::_thesis: z in Y then z = g . x by A11, A13; hence z in Y by A16, Th4; ::_thesis: verum end; suppose ( not x in dom f & not x in dom g ) ; ::_thesis: z in Y then z = the Element of Y by A10, A11, A12, A13; hence z in Y by A4; ::_thesis: verum end; end; end; then reconsider h9 = h as PartFunc of X,Y by A10, RELSET_1:4; A17: f tolerates h proof let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom h) implies f . x = h . x ) assume x in (dom f) /\ (dom h) ; ::_thesis: f . x = h . x then x in dom f by XBOOLE_0:def_4; hence f . x = h . x by A11; ::_thesis: verum end; A18: g tolerates h proof let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x ) assume x in (dom g) /\ (dom h) ; ::_thesis: g . x = h . x then x in dom g by XBOOLE_0:def_4; hence g . x = h . x by A11; ::_thesis: verum end; h9 is total by A10, Def2; hence ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) by A17, A18; ::_thesis: verum end; end; end; hence ex h being PartFunc of X,Y st ( h is total & f tolerates h & g tolerates h ) ; ::_thesis: verum end; definition let X, Y be set ; let f be PartFunc of X,Y; func TotFuncs f -> set means :Def5: :: PARTFUN1:def 5 for x being set holds ( x in it iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) proof defpred S1[ set ] means ex g being PartFunc of X,Y st ( g = \$1 & g is total & f tolerates g ); now__::_thesis:_ex_F_being_set_st_ for_x_being_set_holds_ (_(_x_in_F_implies_ex_g_being_PartFunc_of_X,Y_st_ (_g_=_x_&_g_is_total_&_f_tolerates_g_)_)_&_(_ex_g_being_PartFunc_of_X,Y_st_ (_g_=_x_&_g_is_total_&_f_tolerates_g_)_implies_x_in_F_)_) consider F being set such that A1: for x being set holds ( x in F iff ( x in PFuncs (X,Y) & S1[x] ) ) from XBOOLE_0:sch_1(); take F = F; ::_thesis: for x being set holds ( ( x in F implies ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) implies x in F ) ) let x be set ; ::_thesis: ( ( x in F implies ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) implies x in F ) ) thus ( x in F implies ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) by A1; ::_thesis: ( ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) implies x in F ) given g being PartFunc of X,Y such that A2: ( g = x & g is total & f tolerates g ) ; ::_thesis: x in F g in PFuncs (X,Y) by Th45; hence x in F by A1, A2; ::_thesis: verum end; hence ex b1 being set st for x being set holds ( x in b1 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds ( x in b2 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex g being PartFunc of X,Y st ( g = \$1 & g is total & f tolerates g ); let F1, F2 be set ; ::_thesis: ( ( for x being set holds ( x in F1 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds ( x in F2 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ) implies F1 = F2 ) assume that A3: for x being set holds ( x in F1 iff S1[x] ) and A4: for x being set holds ( x in F2 iff S1[x] ) ; ::_thesis: F1 = F2 thus F1 = F2 from XBOOLE_0:sch_2(A3, A4); ::_thesis: verum end; end; :: deftheorem Def5 defines TotFuncs PARTFUN1:def_5_:_ for X, Y being set for f being PartFunc of X,Y for b4 being set holds ( b4 = TotFuncs f iff for x being set holds ( x in b4 iff ex g being PartFunc of X,Y st ( g = x & g is total & f tolerates g ) ) ); theorem Th69: :: PARTFUN1:69 for X, Y being set for f being PartFunc of X,Y for g being set st g in TotFuncs f holds g is PartFunc of X,Y proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y for g being set st g in TotFuncs f holds g is PartFunc of X,Y let f be PartFunc of X,Y; ::_thesis: for g being set st g in TotFuncs f holds g is PartFunc of X,Y let g be set ; ::_thesis: ( g in TotFuncs f implies g is PartFunc of X,Y ) assume g in TotFuncs f ; ::_thesis: g is PartFunc of X,Y then ex g9 being PartFunc of X,Y st ( g9 = g & g9 is total & f tolerates g9 ) by Def5; hence g is PartFunc of X,Y ; ::_thesis: verum end; theorem Th70: :: PARTFUN1:70 for X, Y being set for f, g being PartFunc of X,Y st g in TotFuncs f holds g is total proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g in TotFuncs f holds g is total let f, g be PartFunc of X,Y; ::_thesis: ( g in TotFuncs f implies g is total ) assume g in TotFuncs f ; ::_thesis: g is total then ex g9 being PartFunc of X,Y st ( g9 = g & g9 is total & f tolerates g9 ) by Def5; hence g is total ; ::_thesis: verum end; theorem Th71: :: PARTFUN1:71 for X, Y being set for f being PartFunc of X,Y for g being Function st g in TotFuncs f holds f tolerates g proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y for g being Function st g in TotFuncs f holds f tolerates g let f be PartFunc of X,Y; ::_thesis: for g being Function st g in TotFuncs f holds f tolerates g let g be Function; ::_thesis: ( g in TotFuncs f implies f tolerates g ) assume g in TotFuncs f ; ::_thesis: f tolerates g then ex g9 being PartFunc of X,Y st ( g9 = g & g9 is total & f tolerates g9 ) by Def5; hence f tolerates g ; ::_thesis: verum end; registration let X be non empty set ; let Y be empty set ; let f be PartFunc of X,Y; cluster TotFuncs f -> empty ; coherence TotFuncs f is empty proof set g = the Element of TotFuncs f; assume not TotFuncs f is empty ; ::_thesis: contradiction then ex g9 being PartFunc of X,{} st ( g9 = the Element of TotFuncs f & g9 is total & f tolerates g9 ) by Def5; hence contradiction ; ::_thesis: verum end; end; theorem Th72: :: PARTFUN1:72 for X, Y being set for f being PartFunc of X,Y holds ( f is total iff TotFuncs f = {f} ) proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds ( f is total iff TotFuncs f = {f} ) let f be PartFunc of X,Y; ::_thesis: ( f is total iff TotFuncs f = {f} ) thus ( f is total implies TotFuncs f = {f} ) ::_thesis: ( TotFuncs f = {f} implies f is total ) proof assume A1: f is total ; ::_thesis: TotFuncs f = {f} for g being set holds ( g in TotFuncs f iff f = g ) proof let g be set ; ::_thesis: ( g in TotFuncs f iff f = g ) thus ( g in TotFuncs f implies f = g ) ::_thesis: ( f = g implies g in TotFuncs f ) proof assume g in TotFuncs f ; ::_thesis: f = g then ex g9 being PartFunc of X,Y st ( g9 = g & g9 is total & f tolerates g9 ) by Def5; hence f = g by A1, Th66; ::_thesis: verum end; thus ( f = g implies g in TotFuncs f ) by A1, Def5; ::_thesis: verum end; hence TotFuncs f = {f} by TARSKI:def_1; ::_thesis: verum end; assume TotFuncs f = {f} ; ::_thesis: f is total then f in TotFuncs f by TARSKI:def_1; hence f is total by Th70; ::_thesis: verum end; theorem :: PARTFUN1:73 for Y being set for f being PartFunc of {},Y holds TotFuncs f = {f} by Th72; theorem :: PARTFUN1:74 for Y being set for f being PartFunc of {},Y holds TotFuncs f = {{}} by Th72; theorem :: PARTFUN1:75 for X, Y being set for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f tolerates g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f tolerates g let f, g be PartFunc of X,Y; ::_thesis: ( TotFuncs f meets TotFuncs g implies f tolerates g ) set h = the Element of (TotFuncs f) /\ (TotFuncs g); assume A1: (TotFuncs f) /\ (TotFuncs g) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: f tolerates g then A2: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs f by XBOOLE_0:def_4; A3: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs g by A1, XBOOLE_0:def_4; reconsider h = the Element of (TotFuncs f) /\ (TotFuncs g) as PartFunc of X,Y by A2, Th69; A4: g tolerates h by A3, Th71; f tolerates h by A2, Th71; hence f tolerates g by A2, A4, Th67, Th70; ::_thesis: verum end; theorem :: PARTFUN1:76 for X, Y being set for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds TotFuncs f meets TotFuncs g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds TotFuncs f meets TotFuncs g let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies TotFuncs f meets TotFuncs g ) assume ( ( Y = {} implies X = {} ) & f tolerates g ) ; ::_thesis: TotFuncs f meets TotFuncs g then consider h being PartFunc of X,Y such that A1: ( h is total & f tolerates h & g tolerates h ) by Th68; ( h in TotFuncs f & h in TotFuncs g ) by A1, Def5; hence (TotFuncs f) /\ (TotFuncs g) <> {} by XBOOLE_0:def_4; :: according to XBOOLE_0:def_7 ::_thesis: verum end; begin Lm2: for X being set for R being Relation of X st R = id X holds R is total proof let X be set ; ::_thesis: for R being Relation of X st R = id X holds R is total let R be Relation of X; ::_thesis: ( R = id X implies R is total ) assume R = id X ; ::_thesis: R is total hence dom R = X by RELAT_1:45; :: according to PARTFUN1:def_2 ::_thesis: verum end; Lm3: for X being set for R being Relation st R = id X holds ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) proof let X be set ; ::_thesis: for R being Relation st R = id X holds ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) let R be Relation; ::_thesis: ( R = id X implies ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) ) assume A1: R = id X ; ::_thesis: ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) then A2: ( dom R = X & rng R = X ) by RELAT_1:45; thus R is_reflexive_in field R :: according to RELAT_2:def_9 ::_thesis: ( R is symmetric & R is antisymmetric & R is transitive ) proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in field R or [x,x] in R ) thus ( not x in field R or [x,x] in R ) by A1, A2, RELAT_1:def_10; ::_thesis: verum end; thus R is_symmetric_in field R :: according to RELAT_2:def_11 ::_thesis: ( R is antisymmetric & R is transitive ) proof let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds ( not x in field R or not b1 in field R or not [x,b1] in R or [b1,x] in R ) let y be set ; ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R ) assume that x in field R and y in field R ; ::_thesis: ( not [x,y] in R or [y,x] in R ) assume [x,y] in R ; ::_thesis: [y,x] in R hence [y,x] in R by A1, RELAT_1:def_10; ::_thesis: verum end; thus R is_antisymmetric_in field R :: according to RELAT_2:def_12 ::_thesis: R is transitive proof let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds ( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 ) thus for b1 being set holds ( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 ) by A1, RELAT_1:def_10; ::_thesis: verum end; thus R is_transitive_in field R :: according to RELAT_2:def_16 ::_thesis: verum proof let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds ( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) thus for b1, b2 being set holds ( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) by A1, RELAT_1:def_10; ::_thesis: verum end; end; Lm4: for X being set holds id X is Relation of X proof let X be set ; ::_thesis: id X is Relation of X ( dom (id X) c= X & rng (id X) c= X ) ; hence id X is Relation of X by RELSET_1:4; ::_thesis: verum end; registration let X be set ; cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total for Element of bool [:X,X:]; existence ex b1 being Relation of X st ( b1 is total & b1 is reflexive & b1 is symmetric & b1 is antisymmetric & b1 is transitive ) proof reconsider R = id X as Relation of X by Lm4; take R ; ::_thesis: ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) thus ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) by Lm2, Lm3; ::_thesis: verum end; end; registration cluster Relation-like symmetric transitive -> reflexive for set ; coherence for b1 being Relation st b1 is symmetric & b1 is transitive holds b1 is reflexive proof let R be Relation; ::_thesis: ( R is symmetric & R is transitive implies R is reflexive ) assume that A1: R is_symmetric_in field R and A2: R is_transitive_in field R ; :: according to RELAT_2:def_11,RELAT_2:def_16 ::_thesis: R is reflexive let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field R or [x,x] in R ) assume A3: x in field R ; ::_thesis: [x,x] in R then ( x in dom R or x in rng R ) by XBOOLE_0:def_3; then consider y being set such that A4: ( [x,y] in R or [y,x] in R ) by XTUPLE_0:def_12, XTUPLE_0:def_13; ( y in rng R or y in dom R ) by A4, XTUPLE_0:def_12, XTUPLE_0:def_13; then A5: y in field R by XBOOLE_0:def_3; then ( [x,y] in R & [y,x] in R ) by A1, A3, A4, RELAT_2:def_3; hence [x,x] in R by A2, A3, A5, RELAT_2:def_8; ::_thesis: verum end; end; registration let X be set ; cluster id X -> symmetric antisymmetric transitive ; coherence ( id X is symmetric & id X is antisymmetric & id X is transitive ) by Lm3; end; definition let X be set ; :: original: id redefine func id X -> total Relation of X; coherence id X is total Relation of X by Lm2, Lm4; end; scheme :: PARTFUN1:sch 4 LambdaC9{ F1() -> non empty set , P1[ set ], F2( set ) -> set , F3( set ) -> set } : ex f being Function st ( dom f = F1() & ( for x being Element of F1() holds ( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) proof consider f being Function such that A1: ( dom f = F1() & ( for x being set st x in F1() holds ( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) from PARTFUN1:sch_1(); take f ; ::_thesis: ( dom f = F1() & ( for x being Element of F1() holds ( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) thus ( dom f = F1() & ( for x being Element of F1() holds ( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) by A1; ::_thesis: verum end; begin theorem Th77: :: PARTFUN1:77 for x, y, z being set for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds y = z proof let x, y, z be set ; ::_thesis: for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds y = z let f, g be Function; ::_thesis: ( f tolerates g & [x,y] in f & [x,z] in g implies y = z ) assume f tolerates g ; ::_thesis: ( not [x,y] in f or not [x,z] in g or y = z ) then consider h being Function such that A1: h = f \/ g by Th51; assume ( [x,y] in f & [x,z] in g ) ; ::_thesis: y = z then ( [x,y] in h & [x,z] in h ) by A1, XBOOLE_0:def_3; hence y = z by FUNCT_1:def_1; ::_thesis: verum end; theorem :: PARTFUN1:78 for A being set st A is functional & ( for f, g being Function st f in A & g in A holds f tolerates g ) holds union A is Function proof let A be set ; ::_thesis: ( A is functional & ( for f, g being Function st f in A & g in A holds f tolerates g ) implies union A is Function ) assume that A1: for x being set st x in A holds x is Function and A2: for f, g being Function st f in A & g in A holds f tolerates g ; :: according to FUNCT_1:def_13 ::_thesis: union A is Function A3: now__::_thesis:_for_x,_y,_z_being_set_st_[x,y]_in_union_A_&_[x,z]_in_union_A_holds_ y_=_z let x, y, z be set ; ::_thesis: ( [x,y] in union A & [x,z] in union A implies y = z ) assume that A4: [x,y] in union A and A5: [x,z] in union A ; ::_thesis: y = z consider p being set such that A6: [x,y] in p and A7: p in A by A4, TARSKI:def_4; consider q being set such that A8: [x,z] in q and A9: q in A by A5, TARSKI:def_4; reconsider p = p, q = q as Function by A1, A7, A9; p tolerates q by A2, A7, A9; hence y = z by A6, A8, Th77; ::_thesis: verum end; now__::_thesis:_for_z_being_set_st_z_in_union_A_holds_ ex_x,_y_being_set_st_[x,y]_=_z let z be set ; ::_thesis: ( z in union A implies ex x, y being set st [x,y] = z ) assume z in union A ; ::_thesis: ex x, y being set st [x,y] = z then consider p being set such that A10: z in p and A11: p in A by TARSKI:def_4; reconsider p = p as Function by A1, A11; p = p ; hence ex x, y being set st [x,y] = z by A10, RELAT_1:def_1; ::_thesis: verum end; hence union A is Function by A3, FUNCT_1:def_1, RELAT_1:def_1; ::_thesis: verum end; definition let D be set ; let p be D -valued Function; let i be set ; assume A1: i in dom p ; funcp /. i -> Element of D equals :Def6: :: PARTFUN1:def 6 p . i; coherence p . i is Element of D by A1, Th4; end; :: deftheorem Def6 defines /. PARTFUN1:def_6_:_ for D being set for p being b1 -valued Function for i being set st i in dom p holds p /. i = p . i; registration let X, Y be non empty set ; cluster Relation-like X -defined Y -valued Function-like non empty for Element of bool [:X,Y:]; existence not for b1 being PartFunc of X,Y holds b1 is empty proof reconsider p = {[(choose X),(choose Y)]} as PartFunc of X,Y by RELSET_1:3; take p ; ::_thesis: not p is empty thus not p is empty ; ::_thesis: verum end; end; registration let A, B be set ; cluster PFuncs (A,B) -> functional ; coherence PFuncs (A,B) is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in PFuncs (A,B) or x is set ) assume x in PFuncs (A,B) ; ::_thesis: x is set then ex f being Function st ( x = f & dom f c= A & rng f c= B ) by Def3; hence x is set ; ::_thesis: verum end; end; theorem :: PARTFUN1:79 for f1, f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds f1 * g = f2 * g proof let f1, f2, g be Function; ::_thesis: ( rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 implies f1 * g = f2 * g ) assume that A1: rng g c= dom f1 and A2: rng g c= dom f2 and A3: f1 tolerates f2 ; ::_thesis: f1 * g = f2 * g A4: dom (f2 * g) = dom g by A2, RELAT_1:27; A5: dom (f1 * g) = dom g by A1, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ (f1_*_g)_._x_=_(f2_*_g)_._x let x be set ; ::_thesis: ( x in dom g implies (f1 * g) . x = (f2 * g) . x ) assume A6: x in dom g ; ::_thesis: (f1 * g) . x = (f2 * g) . x then A7: (f2 * g) . x = f2 . (g . x) by A4, FUNCT_1:12; g . x in rng g by A6, FUNCT_1:def_3; then A8: g . x in (dom f1) /\ (dom f2) by A1, A2, XBOOLE_0:def_4; (f1 * g) . x = f1 . (g . x) by A5, A6, FUNCT_1:12; hence (f1 * g) . x = (f2 * g) . x by A3, A7, A8, Def4; ::_thesis: verum end; hence f1 * g = f2 * g by A5, A4, FUNCT_1:2; ::_thesis: verum end; theorem :: PARTFUN1:80 for Y, x, X being set for f being b1 -valued Function st x in dom (f | X) holds (f | X) /. x = f /. x proof let Y, x, X be set ; ::_thesis: for f being Y -valued Function st x in dom (f | X) holds (f | X) /. x = f /. x let f be Y -valued Function; ::_thesis: ( x in dom (f | X) implies (f | X) /. x = f /. x ) assume A1: x in dom (f | X) ; ::_thesis: (f | X) /. x = f /. x then A2: x in dom f by RELAT_1:57; thus (f | X) /. x = (f | X) . x by A1, Def6 .= f . x by A1, FUNCT_1:47 .= f /. x by A2, Def6 ; ::_thesis: verum end;