:: FUNCT_4 semantic presentation begin Lm1: for x, x9, y, y9, x1, x19, y1, y19 being set st [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] holds ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) proof let x, x9, y, y9, x1, x19, y1, y19 be set ; ::_thesis: ( [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] implies ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) ) assume [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] ; ::_thesis: ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) then ( [x,x9] = [x1,x19] & [y,y9] = [y1,y19] ) by XTUPLE_0:1; hence ( x = x1 & y = y1 & x9 = x19 & y9 = y19 ) by XTUPLE_0:1; ::_thesis: verum end; theorem Th1: :: FUNCT_4:1 for Z being set st ( for z being set st z in Z holds ex x, y being set st z = [x,y] ) holds ex X, Y being set st Z c= [:X,Y:] proof let Z be set ; ::_thesis: ( ( for z being set st z in Z holds ex x, y being set st z = [x,y] ) implies ex X, Y being set st Z c= [:X,Y:] ) assume A1: for z being set st z in Z holds ex x, y being set st z = [x,y] ; ::_thesis: ex X, Y being set st Z c= [:X,Y:] defpred S1[ set ] means ex y being set st [\$1,y] in Z; consider X being set such that A2: for x being set holds ( x in X iff ( x in union (union Z) & S1[x] ) ) from XBOOLE_0:sch_1(); defpred S2[ set ] means ex x being set st [x,\$1] in Z; consider Y being set such that A3: for y being set holds ( y in Y iff ( y in union (union Z) & S2[y] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: ex Y being set st Z c= [:X,Y:] take Y ; ::_thesis: Z c= [:X,Y:] let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in [:X,Y:] ) assume A4: z in Z ; ::_thesis: z in [:X,Y:] then consider x, y being set such that A5: z = [x,y] by A1; x in union (union Z) by A4, A5, ZFMISC_1:134; then A6: x in X by A2, A4, A5; y in union (union Z) by A4, A5, ZFMISC_1:134; then y in Y by A3, A4, A5; hence z in [:X,Y:] by A5, A6, ZFMISC_1:87; ::_thesis: verum end; theorem :: FUNCT_4:2 for g, f being Function holds g * f = (g | (rng f)) * f proof let g, f be Function; ::_thesis: g * f = (g | (rng f)) * f for x being set holds ( x in dom (g * f) iff x in dom ((g | (rng f)) * f) ) proof let x be set ; ::_thesis: ( x in dom (g * f) iff x in dom ((g | (rng f)) * f) ) A1: dom (g | (rng f)) = (dom g) /\ (rng f) by RELAT_1:61; thus ( x in dom (g * f) implies x in dom ((g | (rng f)) * f) ) ::_thesis: ( x in dom ((g | (rng f)) * f) implies x in dom (g * f) ) proof assume A2: x in dom (g * f) ; ::_thesis: x in dom ((g | (rng f)) * f) then A3: x in dom f by FUNCT_1:11; x in dom f by A2, FUNCT_1:11; then A4: f . x in rng f by FUNCT_1:def_3; f . x in dom g by A2, FUNCT_1:11; then f . x in dom (g | (rng f)) by A1, A4, XBOOLE_0:def_4; hence x in dom ((g | (rng f)) * f) by A3, FUNCT_1:11; ::_thesis: verum end; assume A5: x in dom ((g | (rng f)) * f) ; ::_thesis: x in dom (g * f) then f . x in dom (g | (rng f)) by FUNCT_1:11; then A6: f . x in dom g by A1, XBOOLE_0:def_4; x in dom f by A5, FUNCT_1:11; hence x in dom (g * f) by A6, FUNCT_1:11; ::_thesis: verum end; then A7: dom (g * f) = dom ((g | (rng f)) * f) by TARSKI:1; for x being set st x in dom (g * f) holds (g * f) . x = ((g | (rng f)) * f) . x proof let x be set ; ::_thesis: ( x in dom (g * f) implies (g * f) . x = ((g | (rng f)) * f) . x ) assume A8: x in dom (g * f) ; ::_thesis: (g * f) . x = ((g | (rng f)) * f) . x then A9: x in dom f by FUNCT_1:11; then A10: f . x in rng f by FUNCT_1:def_3; thus (g * f) . x = g . (f . x) by A8, FUNCT_1:12 .= (g | (rng f)) . (f . x) by A10, FUNCT_1:49 .= ((g | (rng f)) * f) . x by A9, FUNCT_1:13 ; ::_thesis: verum end; hence g * f = (g | (rng f)) * f by A7, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_4:3 for X, Y being set holds ( id X c= id Y iff X c= Y ) proof let X, Y be set ; ::_thesis: ( id X c= id Y iff X c= Y ) thus ( id X c= id Y implies X c= Y ) ::_thesis: ( X c= Y implies id X c= id Y ) proof assume A1: id X c= id Y ; ::_thesis: X c= Y let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y ) assume x in X ; ::_thesis: x in Y then [x,x] in id X by RELAT_1:def_10; hence x in Y by A1, RELAT_1:def_10; ::_thesis: verum end; assume A2: X c= Y ; ::_thesis: id X c= id Y let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in id X or z in id Y ) assume A3: z in id X ; ::_thesis: z in id Y then consider x, x9 being set such that A4: x in X and x9 in X and A5: z = [x,x9] by ZFMISC_1:84; x = x9 by A3, A5, RELAT_1:def_10; hence z in id Y by A2, A4, A5, RELAT_1:def_10; ::_thesis: verum end; theorem :: FUNCT_4:4 for X, Y, a being set st X c= Y holds X --> a c= Y --> a proof let X, Y, a be set ; ::_thesis: ( X c= Y implies X --> a c= Y --> a ) A1: dom (X --> a) = X by FUNCOP_1:13; assume A2: X c= Y ; ::_thesis: X --> a c= Y --> a A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(X_-->_a)_holds_ (X_-->_a)_._x_=_(Y_-->_a)_._x let x be set ; ::_thesis: ( x in dom (X --> a) implies (X --> a) . x = (Y --> a) . x ) assume A4: x in dom (X --> a) ; ::_thesis: (X --> a) . x = (Y --> a) . x then (X --> a) . x = a by FUNCOP_1:7; hence (X --> a) . x = (Y --> a) . x by A2, A1, A4, FUNCOP_1:7; ::_thesis: verum end; dom (Y --> a) = Y by FUNCOP_1:13; hence X --> a c= Y --> a by A2, A1, A3, GRFUNC_1:2; ::_thesis: verum end; theorem Th5: :: FUNCT_4:5 for X, a, Y, b being set st X --> a c= Y --> b holds X c= Y proof let X, a, Y, b be set ; ::_thesis: ( X --> a c= Y --> b implies X c= Y ) assume X --> a c= Y --> b ; ::_thesis: X c= Y then A1: dom (X --> a) c= dom (Y --> b) by RELAT_1:11; dom (X --> a) = X by FUNCOP_1:13; hence X c= Y by A1, FUNCOP_1:13; ::_thesis: verum end; theorem :: FUNCT_4:6 for X, a, Y, b being set st X <> {} & X --> a c= Y --> b holds a = b proof let X, a, Y, b be set ; ::_thesis: ( X <> {} & X --> a c= Y --> b implies a = b ) assume A1: X <> {} ; ::_thesis: ( not X --> a c= Y --> b or a = b ) set x = the Element of X; assume A2: X --> a c= Y --> b ; ::_thesis: a = b then X c= Y by Th5; then the Element of X in Y by A1, TARSKI:def_3; then A3: (Y --> b) . the Element of X = b by FUNCOP_1:7; ( dom (X --> a) = X & (X --> a) . the Element of X = a ) by A1, FUNCOP_1:7, FUNCOP_1:13; hence a = b by A1, A2, A3, GRFUNC_1:2; ::_thesis: verum end; theorem :: FUNCT_4:7 for x being set for f being Function st x in dom f holds x .--> (f . x) c= f proof let x be set ; ::_thesis: for f being Function st x in dom f holds x .--> (f . x) c= f let f be Function; ::_thesis: ( x in dom f implies x .--> (f . x) c= f ) A1: now__::_thesis:_for_y_being_set_st_y_in_dom_(x_.-->_(f_._x))_holds_ (x_.-->_(f_._x))_._y_=_f_._y let y be set ; ::_thesis: ( y in dom (x .--> (f . x)) implies (x .--> (f . x)) . y = f . y ) assume y in dom (x .--> (f . x)) ; ::_thesis: (x .--> (f . x)) . y = f . y then x = y by FUNCOP_1:75; hence (x .--> (f . x)) . y = f . y by FUNCOP_1:72; ::_thesis: verum end; assume A2: x in dom f ; ::_thesis: x .--> (f . x) c= f dom (x .--> (f . x)) c= dom f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (x .--> (f . x)) or y in dom f ) thus ( not y in dom (x .--> (f . x)) or y in dom f ) by A2, FUNCOP_1:75; ::_thesis: verum end; hence x .--> (f . x) c= f by A1, GRFUNC_1:2; ::_thesis: verum end; theorem :: FUNCT_4:8 for Y, X being set for f being Function holds (Y |` f) | X c= f proof let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X c= f let f be Function; ::_thesis: (Y |` f) | X c= f ( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86; hence (Y |` f) | X c= f by XBOOLE_1:1; ::_thesis: verum end; theorem :: FUNCT_4:9 for Y, X being set for f, g being Function st f c= g holds (Y |` f) | X c= (Y |` g) | X proof let Y, X be set ; ::_thesis: for f, g being Function st f c= g holds (Y |` f) | X c= (Y |` g) | X let f, g be Function; ::_thesis: ( f c= g implies (Y |` f) | X c= (Y |` g) | X ) assume f c= g ; ::_thesis: (Y |` f) | X c= (Y |` g) | X then Y |` f c= Y |` g by RELAT_1:101; hence (Y |` f) | X c= (Y |` g) | X by RELAT_1:76; ::_thesis: verum end; definition let f, g be Function; funcf +* g -> Function means :Def1: :: FUNCT_4:def 1 ( dom it = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies it . x = g . x ) & ( not x in dom g implies it . x = f . x ) ) ) ); existence ex b1 being Function st ( dom b1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies b1 . x = g . x ) & ( not x in dom g implies b1 . x = f . x ) ) ) ) proof deffunc H1( set ) -> set = f . \$1; deffunc H2( set ) -> set = g . \$1; defpred S1[ set ] means \$1 in dom g; thus ex F being Function st ( dom F = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies b1 . x = g . x ) & ( not x in dom g implies b1 . x = f . x ) ) ) & dom b2 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies b2 . x = g . x ) & ( not x in dom g implies b2 . x = f . x ) ) ) holds b1 = b2 proof let h1, h2 be Function; ::_thesis: ( dom h1 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) ) & dom h2 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ) implies h1 = h2 ) assume that A1: dom h1 = (dom f) \/ (dom g) and A2: for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies h1 . x = g . x ) & ( not x in dom g implies h1 . x = f . x ) ) and A3: dom h2 = (dom f) \/ (dom g) and A4: for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies h2 . x = g . x ) & ( not x in dom g implies h2 . x = f . x ) ) ; ::_thesis: h1 = h2 for x being set st x in (dom f) \/ (dom g) holds h1 . x = h2 . x proof let x be set ; ::_thesis: ( x in (dom f) \/ (dom g) implies h1 . x = h2 . x ) assume A5: x in (dom f) \/ (dom g) ; ::_thesis: h1 . x = h2 . x then A6: ( not x in dom g implies ( h1 . x = f . x & h2 . x = f . x ) ) by A2, A4; ( x in dom g implies ( h1 . x = g . x & h2 . x = g . x ) ) by A2, A4, A5; hence h1 . x = h2 . x by A6; ::_thesis: verum end; hence h1 = h2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; idempotence for f being Function holds ( dom f = (dom f) \/ (dom f) & ( for x being set st x in (dom f) \/ (dom f) holds ( ( x in dom f implies f . x = f . x ) & ( not x in dom f implies f . x = f . x ) ) ) ) ; end; :: deftheorem Def1 defines +* FUNCT_4:def_1_:_ for f, g, b3 being Function holds ( b3 = f +* g iff ( dom b3 = (dom f) \/ (dom g) & ( for x being set st x in (dom f) \/ (dom g) holds ( ( x in dom g implies b3 . x = g . x ) & ( not x in dom g implies b3 . x = f . x ) ) ) ) ); theorem Th10: :: FUNCT_4:10 for f, g being Function holds ( dom f c= dom (f +* g) & dom g c= dom (f +* g) ) proof let f, g be Function; ::_thesis: ( dom f c= dom (f +* g) & dom g c= dom (f +* g) ) dom (f +* g) = (dom f) \/ (dom g) by Def1; hence ( dom f c= dom (f +* g) & dom g c= dom (f +* g) ) by XBOOLE_1:7; ::_thesis: verum end; theorem Th11: :: FUNCT_4:11 for x being set for g, f being Function st not x in dom g holds (f +* g) . x = f . x proof let x be set ; ::_thesis: for g, f being Function st not x in dom g holds (f +* g) . x = f . x let g, f be Function; ::_thesis: ( not x in dom g implies (f +* g) . x = f . x ) assume A1: not x in dom g ; ::_thesis: (f +* g) . x = f . x percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: (f +* g) . x = f . x then x in (dom f) \/ (dom g) by XBOOLE_0:def_3; hence (f +* g) . x = f . x by A1, Def1; ::_thesis: verum end; supposeA2: not x in dom f ; ::_thesis: (f +* g) . x = f . x then not x in (dom f) \/ (dom g) by A1, XBOOLE_0:def_3; then not x in dom (f +* g) by Def1; hence (f +* g) . x = {} by FUNCT_1:def_2 .= f . x by A2, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; theorem Th12: :: FUNCT_4:12 for x being set for f, g being Function holds ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) proof let x be set ; ::_thesis: for f, g being Function holds ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) let f, g be Function; ::_thesis: ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) ( x in dom (f +* g) iff x in (dom f) \/ (dom g) ) by Def1; hence ( x in dom (f +* g) iff ( x in dom f or x in dom g ) ) by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th13: :: FUNCT_4:13 for x being set for g, f being Function st x in dom g holds (f +* g) . x = g . x proof let x be set ; ::_thesis: for g, f being Function st x in dom g holds (f +* g) . x = g . x let g, f be Function; ::_thesis: ( x in dom g implies (f +* g) . x = g . x ) ( x in dom g implies x in (dom f) \/ (dom g) ) by XBOOLE_0:def_3; hence ( x in dom g implies (f +* g) . x = g . x ) by Def1; ::_thesis: verum end; theorem Th14: :: FUNCT_4:14 for f, g, h being Function holds (f +* g) +* h = f +* (g +* h) proof let f, g, h be Function; ::_thesis: (f +* g) +* h = f +* (g +* h) A1: now__::_thesis:_for_x_being_set_st_x_in_(dom_f)_\/_(dom_(g_+*_h))_holds_ (_(_x_in_dom_(g_+*_h)_implies_((f_+*_g)_+*_h)_._x_=_(g_+*_h)_._x_)_&_(_not_x_in_dom_(g_+*_h)_implies_((f_+*_g)_+*_h)_._x_=_f_._x_)_) let x be set ; ::_thesis: ( x in (dom f) \/ (dom (g +* h)) implies ( ( x in dom (g +* h) implies ((f +* g) +* h) . x = (g +* h) . x ) & ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x ) ) ) assume x in (dom f) \/ (dom (g +* h)) ; ::_thesis: ( ( x in dom (g +* h) implies ((f +* g) +* h) . x = (g +* h) . x ) & ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x ) ) hereby ::_thesis: ( not x in dom (g +* h) implies ((f +* g) +* h) . x = f . x ) assume A2: x in dom (g +* h) ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x percases ( ( x in dom g & not x in dom h ) or x in dom h ) by A2, Th12; supposeA3: ( x in dom g & not x in dom h ) ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x hence ((f +* g) +* h) . x = (f +* g) . x by Th11 .= g . x by A3, Th13 .= (g +* h) . x by A3, Th11 ; ::_thesis: verum end; supposeA4: x in dom h ; ::_thesis: ((f +* g) +* h) . x = (g +* h) . x hence ((f +* g) +* h) . x = h . x by Th13 .= (g +* h) . x by A4, Th13 ; ::_thesis: verum end; end; end; assume A5: not x in dom (g +* h) ; ::_thesis: ((f +* g) +* h) . x = f . x then A6: not x in dom g by Th12; not x in dom h by A5, Th12; hence ((f +* g) +* h) . x = (f +* g) . x by Th11 .= f . x by A6, Th11 ; ::_thesis: verum end; dom ((f +* g) +* h) = (dom (f +* g)) \/ (dom h) by Def1 .= ((dom f) \/ (dom g)) \/ (dom h) by Def1 .= (dom f) \/ ((dom g) \/ (dom h)) by XBOOLE_1:4 .= (dom f) \/ (dom (g +* h)) by Def1 ; hence (f +* g) +* h = f +* (g +* h) by A1, Def1; ::_thesis: verum end; theorem Th15: :: FUNCT_4:15 for x being set for f, g being Function st f tolerates g & x in dom f holds (f +* g) . x = f . x proof let x be set ; ::_thesis: for f, g being Function st f tolerates g & x in dom f holds (f +* g) . x = f . x let f, g be Function; ::_thesis: ( f tolerates g & x in dom f implies (f +* g) . x = f . x ) assume that A1: f tolerates g and A2: x in dom f ; ::_thesis: (f +* g) . x = f . x now__::_thesis:_(f_+*_g)_._x_=_f_._x percases ( x in dom g or not x in dom g ) ; suppose x in dom g ; ::_thesis: (f +* g) . x = f . x then ( x in (dom f) /\ (dom g) & (f +* g) . x = g . x ) by A2, Th13, XBOOLE_0:def_4; hence (f +* g) . x = f . x by A1, PARTFUN1:def_4; ::_thesis: verum end; suppose not x in dom g ; ::_thesis: (f +* g) . x = f . x hence (f +* g) . x = f . x by Th11; ::_thesis: verum end; end; end; hence (f +* g) . x = f . x ; ::_thesis: verum end; theorem :: FUNCT_4:16 for x being set for f, g being Function st dom f misses dom g & x in dom f holds (f +* g) . x = f . x proof let x be set ; ::_thesis: for f, g being Function st dom f misses dom g & x in dom f holds (f +* g) . x = f . x let f, g be Function; ::_thesis: ( dom f misses dom g & x in dom f implies (f +* g) . x = f . x ) assume ( (dom f) /\ (dom g) = {} & x in dom f ) ; :: according to XBOOLE_0:def_7 ::_thesis: (f +* g) . x = f . x then not x in dom g by XBOOLE_0:def_4; hence (f +* g) . x = f . x by Th11; ::_thesis: verum end; theorem Th17: :: FUNCT_4:17 for f, g being Function holds rng (f +* g) c= (rng f) \/ (rng g) proof let f, g be Function; ::_thesis: rng (f +* g) c= (rng f) \/ (rng g) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f +* g) or y in (rng f) \/ (rng g) ) assume y in rng (f +* g) ; ::_thesis: y in (rng f) \/ (rng g) then consider x being set such that A1: x in dom (f +* g) and A2: y = (f +* g) . x by FUNCT_1:def_3; ( ( x in dom f & not x in dom g ) or x in dom g ) by A1, Th12; then ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th11, Th13; then ( y in rng f or y in rng g ) by A2, FUNCT_1:def_3; hence y in (rng f) \/ (rng g) by XBOOLE_0:def_3; ::_thesis: verum end; theorem :: FUNCT_4:18 for g, f being Function holds rng g c= rng (f +* g) proof let g, f be Function; ::_thesis: rng g c= rng (f +* g) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (f +* g) ) assume y in rng g ; ::_thesis: y in rng (f +* g) then consider x being set such that A1: ( x in dom g & y = g . x ) by FUNCT_1:def_3; ( x in dom (f +* g) & (f +* g) . x = y ) by A1, Th12, Th13; hence y in rng (f +* g) by FUNCT_1:def_3; ::_thesis: verum end; theorem Th19: :: FUNCT_4:19 for f, g being Function st dom f c= dom g holds f +* g = g proof let f, g be Function; ::_thesis: ( dom f c= dom g implies f +* g = g ) assume dom f c= dom g ; ::_thesis: f +* g = g then (dom f) \/ (dom g) = dom g by XBOOLE_1:12; then ( dom (f +* g) = dom g & ( for x being set st x in dom g holds (f +* g) . x = g . x ) ) by Def1; hence f +* g = g by FUNCT_1:2; ::_thesis: verum end; registration let f be Function; let g be empty Function; reduceg +* f to f; reducibility g +* f = f proof dom g c= dom f by XBOOLE_1:2; hence g +* f = f by Th19; ::_thesis: verum end; reducef +* g to f; reducibility f +* g = f proof A1: for x being set st x in dom f holds (f +* g) . x = f . x proof let x be set ; ::_thesis: ( x in dom f implies (f +* g) . x = f . x ) assume x in dom f ; ::_thesis: (f +* g) . x = f . x then x in (dom f) \ (dom g) ; hence (f +* g) . x = f . x by Th11; ::_thesis: verum end; (dom f) \/ (dom g) = dom f ; then dom (f +* g) = dom f by Def1; hence f +* g = f by A1, FUNCT_1:2; ::_thesis: verum end; end; theorem Th20: :: FUNCT_4:20 for f being Function holds {} +* f = f ; theorem Th21: :: FUNCT_4:21 for f being Function holds f +* {} = f ; theorem :: FUNCT_4:22 for X, Y being set holds (id X) +* (id Y) = id (X \/ Y) proof let X, Y be set ; ::_thesis: (id X) +* (id Y) = id (X \/ Y) A1: for x being set st x in dom (id (X \/ Y)) holds ((id X) +* (id Y)) . x = (id (X \/ Y)) . x proof let x be set ; ::_thesis: ( x in dom (id (X \/ Y)) implies ((id X) +* (id Y)) . x = (id (X \/ Y)) . x ) assume A2: x in dom (id (X \/ Y)) ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x now__::_thesis:_((id_X)_+*_(id_Y))_._x_=_(id_(X_\/_Y))_._x percases ( x in Y or not x in Y ) ; supposeA3: x in Y ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x dom (id Y) = Y ; hence ((id X) +* (id Y)) . x = (id Y) . x by A3, Th13 .= x by A3, FUNCT_1:18 .= (id (X \/ Y)) . x by A2, FUNCT_1:18 ; ::_thesis: verum end; supposeA4: not x in Y ; ::_thesis: ((id X) +* (id Y)) . x = (id (X \/ Y)) . x then A5: x in X by A2, XBOOLE_0:def_3; not x in dom (id Y) by A4; hence ((id X) +* (id Y)) . x = (id X) . x by Th11 .= x by A5, FUNCT_1:18 .= (id (X \/ Y)) . x by A2, FUNCT_1:18 ; ::_thesis: verum end; end; end; hence ((id X) +* (id Y)) . x = (id (X \/ Y)) . x ; ::_thesis: verum end; dom ((id X) +* (id Y)) = (dom (id X)) \/ (dom (id Y)) by Def1 .= X \/ (dom (id Y)) .= X \/ Y .= dom (id (X \/ Y)) ; hence (id X) +* (id Y) = id (X \/ Y) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_4:23 for f, g being Function holds (f +* g) | (dom g) = g proof let f, g be Function; ::_thesis: (f +* g) | (dom g) = g (dom f) \/ (dom g) = dom (f +* g) by Def1; then A1: dom ((f +* g) | (dom g)) = dom g by RELAT_1:62, XBOOLE_1:7; for x being set st x in dom g holds ((f +* g) | (dom g)) . x = g . x proof let x be set ; ::_thesis: ( x in dom g implies ((f +* g) | (dom g)) . x = g . x ) ( x in dom g implies (f +* g) . x = g . x ) by Th13; hence ( x in dom g implies ((f +* g) | (dom g)) . x = g . x ) by A1, FUNCT_1:47; ::_thesis: verum end; hence (f +* g) | (dom g) = g by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th24: :: FUNCT_4:24 for f, g being Function holds (f +* g) | ((dom f) \ (dom g)) c= f proof let f, g be Function; ::_thesis: (f +* g) | ((dom f) \ (dom g)) c= f A1: for x being set st x in dom ((f +* g) | ((dom f) \ (dom g))) holds ((f +* g) | ((dom f) \ (dom g))) . x = f . x proof let x be set ; ::_thesis: ( x in dom ((f +* g) | ((dom f) \ (dom g))) implies ((f +* g) | ((dom f) \ (dom g))) . x = f . x ) assume A2: x in dom ((f +* g) | ((dom f) \ (dom g))) ; ::_thesis: ((f +* g) | ((dom f) \ (dom g))) . x = f . x dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58; then not x in dom g by A2, XBOOLE_0:def_5; then (f +* g) . x = f . x by Th11; hence ((f +* g) | ((dom f) \ (dom g))) . x = f . x by A2, FUNCT_1:47; ::_thesis: verum end; dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58; then dom ((f +* g) | ((dom f) \ (dom g))) c= dom f by XBOOLE_1:1; hence (f +* g) | ((dom f) \ (dom g)) c= f by A1, GRFUNC_1:2; ::_thesis: verum end; theorem Th25: :: FUNCT_4:25 for g, f being Function holds g c= f +* g proof let g, f be Function; ::_thesis: g c= f +* g dom (f +* g) = (dom f) \/ (dom g) by Def1; then A1: dom g c= dom (f +* g) by XBOOLE_1:7; for x being set st x in dom g holds (f +* g) . x = g . x by Th13; hence g c= f +* g by A1, GRFUNC_1:2; ::_thesis: verum end; theorem :: FUNCT_4:26 for f, g, h being Function st f tolerates g +* h holds f | ((dom f) \ (dom h)) tolerates g proof let f, g, h be Function; ::_thesis: ( f tolerates g +* h implies f | ((dom f) \ (dom h)) tolerates g ) assume A1: f tolerates g +* h ; ::_thesis: f | ((dom f) \ (dom h)) tolerates g let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) or (f | ((dom f) \ (dom h))) . x = g . x ) assume A2: x in (dom (f | ((dom f) \ (dom h)))) /\ (dom g) ; ::_thesis: (f | ((dom f) \ (dom h))) . x = g . x then A3: x in dom (f | ((dom f) \ (dom h))) by XBOOLE_0:def_4; x in dom g by A2, XBOOLE_0:def_4; then A4: x in dom (g +* h) by Th12; A5: dom (f | ((dom f) \ (dom h))) c= (dom f) \ (dom h) by RELAT_1:58; then x in dom f by A3, XBOOLE_0:def_5; then A6: x in (dom f) /\ (dom (g +* h)) by A4, XBOOLE_0:def_4; not x in dom h by A3, A5, XBOOLE_0:def_5; then (g +* h) . x = g . x by Th11; then f . x = g . x by A1, A6, PARTFUN1:def_4; hence (f | ((dom f) \ (dom h))) . x = g . x by A3, A5, FUNCT_1:49; ::_thesis: verum end; theorem Th27: :: FUNCT_4:27 for f, g, h being Function st f tolerates g +* h holds f tolerates h proof let f, g, h be Function; ::_thesis: ( f tolerates g +* h implies f tolerates h ) assume A1: f tolerates g +* h ; ::_thesis: f tolerates h let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f) /\ (dom h) or f . x = h . x ) assume A2: x in (dom f) /\ (dom h) ; ::_thesis: f . x = h . x then A3: x in dom f by XBOOLE_0:def_4; A4: x in dom h by A2, XBOOLE_0:def_4; then x in dom (g +* h) by Th12; then A5: x in (dom f) /\ (dom (g +* h)) by A3, XBOOLE_0:def_4; (g +* h) . x = h . x by A4, Th13; hence f . x = h . x by A1, A5, PARTFUN1:def_4; ::_thesis: verum end; theorem Th28: :: FUNCT_4:28 for f, g being Function holds ( f tolerates g iff f c= f +* g ) proof let f, g be Function; ::_thesis: ( f tolerates g iff f c= f +* g ) thus ( f tolerates g implies f c= f +* g ) ::_thesis: ( f c= f +* g implies f tolerates g ) proof (dom f) \/ (dom g) = dom (f +* g) by Def1; then A1: dom f c= dom (f +* g) by XBOOLE_1:7; assume f tolerates g ; ::_thesis: f c= f +* g then for x being set st x in dom f holds (f +* g) . x = f . x by Th15; hence f c= f +* g by A1, GRFUNC_1:2; ::_thesis: verum end; thus ( f c= f +* g implies f tolerates g ) by Th27, PARTFUN1:54; ::_thesis: verum end; theorem Th29: :: FUNCT_4:29 for f, g being Function holds f +* g c= f \/ g proof let f, g be Function; ::_thesis: f +* g c= f \/ g let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f +* g or p in f \/ g ) assume A1: p in f +* g ; ::_thesis: p in f \/ g then consider x, y being set such that A2: p = [x,y] by RELAT_1:def_1; x in dom (f +* g) by A1, A2, FUNCT_1:1; then ( ( x in dom f & not x in dom g ) or x in dom g ) by Th12; then A3: ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by Th11, Th13; y = (f +* g) . x by A1, A2, FUNCT_1:1; then ( p in f or p in g ) by A2, A3, FUNCT_1:1; hence p in f \/ g by XBOOLE_0:def_3; ::_thesis: verum end; theorem Th30: :: FUNCT_4:30 for f, g being Function holds ( f tolerates g iff f \/ g = f +* g ) proof let f, g be Function; ::_thesis: ( f tolerates g iff f \/ g = f +* g ) thus ( f tolerates g implies f \/ g = f +* g ) ::_thesis: ( f \/ g = f +* g implies f tolerates g ) proof assume f tolerates g ; ::_thesis: f \/ g = f +* g then A1: f c= f +* g by Th28; A2: f +* g c= f \/ g by Th29; g c= f +* g by Th25; then f \/ g c= f +* g by A1, XBOOLE_1:8; hence f \/ g = f +* g by A2, XBOOLE_0:def_10; ::_thesis: verum end; thus ( f \/ g = f +* g implies f tolerates g ) by PARTFUN1:51; ::_thesis: verum end; theorem Th31: :: FUNCT_4:31 for f, g being Function st dom f misses dom g holds f \/ g = f +* g proof let f, g be Function; ::_thesis: ( dom f misses dom g implies f \/ g = f +* g ) assume dom f misses dom g ; ::_thesis: f \/ g = f +* g then f tolerates g by PARTFUN1:56; hence f \/ g = f +* g by Th30; ::_thesis: verum end; theorem Th32: :: FUNCT_4:32 for f, g being Function st dom f misses dom g holds f c= f +* g proof let f, g be Function; ::_thesis: ( dom f misses dom g implies f c= f +* g ) assume dom f misses dom g ; ::_thesis: f c= f +* g then f \/ g = f +* g by Th31; hence f c= f +* g by XBOOLE_1:7; ::_thesis: verum end; theorem :: FUNCT_4:33 for f, g being Function st dom f misses dom g holds (f +* g) | (dom f) = f proof let f, g be Function; ::_thesis: ( dom f misses dom g implies (f +* g) | (dom f) = f ) assume dom f misses dom g ; ::_thesis: (f +* g) | (dom f) = f then A1: (dom f) \ (dom g) = dom f by XBOOLE_1:83; dom ((f +* g) | (dom f)) = (dom (f +* g)) /\ (dom f) by RELAT_1:61 .= ((dom f) \/ (dom g)) /\ (dom f) by Def1 .= dom f by XBOOLE_1:21 ; hence (f +* g) | (dom f) = f by A1, Th24, GRFUNC_1:3; ::_thesis: verum end; theorem Th34: :: FUNCT_4:34 for f, g being Function holds ( f tolerates g iff f +* g = g +* f ) proof let f, g be Function; ::_thesis: ( f tolerates g iff f +* g = g +* f ) thus ( f tolerates g implies f +* g = g +* f ) ::_thesis: ( f +* g = g +* f implies f tolerates g ) proof assume A1: f tolerates g ; ::_thesis: f +* g = g +* f A2: for x being set st x in dom (f +* g) holds (f +* g) . x = (g +* f) . x proof let x be set ; ::_thesis: ( x in dom (f +* g) implies (f +* g) . x = (g +* f) . x ) assume A3: x in dom (f +* g) ; ::_thesis: (f +* g) . x = (g +* f) . x now__::_thesis:_(f_+*_g)_._x_=_(g_+*_f)_._x A4: dom (f +* g) = (dom f) \/ (dom g) by Def1; 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 A3, A4, XBOOLE_0:def_3; supposeA5: ( x in dom f & x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x then A6: (g +* f) . x = f . x by Th13; ( x in (dom f) /\ (dom g) & (f +* g) . x = g . x ) by A5, Th13, XBOOLE_0:def_4; hence (f +* g) . x = (g +* f) . x by A1, A6, PARTFUN1:def_4; ::_thesis: verum end; supposeA7: ( x in dom f & not x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x then (f +* g) . x = f . x by Th11; hence (f +* g) . x = (g +* f) . x by A7, Th13; ::_thesis: verum end; supposeA8: ( not x in dom f & x in dom g ) ; ::_thesis: (f +* g) . x = (g +* f) . x then (f +* g) . x = g . x by Th13; hence (f +* g) . x = (g +* f) . x by A8, Th11; ::_thesis: verum end; end; end; hence (f +* g) . x = (g +* f) . x ; ::_thesis: verum end; dom (f +* g) = (dom g) \/ (dom f) by Def1 .= dom (g +* f) by Def1 ; hence f +* g = g +* f by A2, FUNCT_1:2; ::_thesis: verum end; assume A9: f +* g = g +* f ; ::_thesis: f tolerates g let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x ) assume A10: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x then x in dom g by XBOOLE_0:def_4; then A11: (f +* g) . x = g . x by Th13; x in dom f by A10, XBOOLE_0:def_4; hence f . x = g . x by A9, A11, Th13; ::_thesis: verum end; theorem Th35: :: FUNCT_4:35 for f, g being Function st dom f misses dom g holds f +* g = g +* f proof let f, g be Function; ::_thesis: ( dom f misses dom g implies f +* g = g +* f ) assume dom f misses dom g ; ::_thesis: f +* g = g +* f then f tolerates g by PARTFUN1:56; hence f +* g = g +* f by Th34; ::_thesis: verum end; theorem :: FUNCT_4:36 for X, Y being set for f, g being PartFunc of X,Y st g is total holds f +* g = g proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g is total holds f +* g = g let f, g be PartFunc of X,Y; ::_thesis: ( g is total implies f +* g = g ) assume dom g = X ; :: according to PARTFUN1:def_2 ::_thesis: f +* g = g then dom f c= dom g ; hence f +* g = g by Th19; ::_thesis: verum end; theorem Th37: :: FUNCT_4:37 for X, Y being set for f, g being Function of X,Y st ( Y = {} implies X = {} ) holds f +* g = g proof let X, Y be set ; ::_thesis: for f, g being Function of X,Y st ( Y = {} implies X = {} ) holds f +* g = g let f, g be Function of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) implies f +* g = g ) assume ( Y = {} implies X = {} ) ; ::_thesis: f +* g = g then ( dom f = X & dom g = X ) by FUNCT_2:def_1; hence f +* g = g by Th19; ::_thesis: verum end; theorem :: FUNCT_4:38 for X being set for f, g being Function of X,X holds f +* g = g by Th37; theorem :: FUNCT_4:39 for X being set for D being non empty set for f, g being Function of X,D holds f +* g = g by Th37; theorem :: FUNCT_4:40 for X, Y being set for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y proof let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y let f, g be PartFunc of X,Y; ::_thesis: f +* g is PartFunc of X,Y rng (f +* g) c= (rng f) \/ (rng g) by Th17; then A1: rng (f +* g) c= Y by XBOOLE_1:1; dom (f +* g) = (dom f) \/ (dom g) by Def1; hence f +* g is PartFunc of X,Y by A1, RELSET_1:4; ::_thesis: verum end; definition let f be Function; func ~ f -> Function means :Def2: :: FUNCT_4:def 2 ( ( for x being set holds ( x in dom it iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds it . (z,y) = f . (y,z) ) ); existence ex b1 being Function st ( ( for x being set holds ( x in dom b1 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds b1 . (z,y) = f . (y,z) ) ) proof defpred S1[ set , set ] means ex y, z being set st ( \$1 = [z,y] & \$2 = f . [y,z] ); defpred S2[ set ] means ex y being set st [\$1,y] in dom f; consider D1 being set such that A1: for x being set holds ( x in D1 iff ( x in union (union (dom f)) & S2[x] ) ) from XBOOLE_0:sch_1(); defpred S3[ set ] means ex y being set st [y,\$1] in dom f; consider D2 being set such that A2: for y being set holds ( y in D2 iff ( y in union (union (dom f)) & S3[y] ) ) from XBOOLE_0:sch_1(); defpred S4[ set ] means ex y, z being set st ( \$1 = [z,y] & [y,z] in dom f ); consider D being set such that A3: for x being set holds ( x in D iff ( x in [:D2,D1:] & S4[x] ) ) from XBOOLE_0:sch_1(); A4: for x, y1, y2 being set st x in D & S1[x,y1] & S1[x,y2] holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( x in D & S1[x,y1] & S1[x,y2] implies y1 = y2 ) assume x in D ; ::_thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 ) given y, z being set such that A5: x = [z,y] and A6: y1 = f . [y,z] ; ::_thesis: ( not S1[x,y2] or y1 = y2 ) given y9, z9 being set such that A7: x = [z9,y9] and A8: y2 = f . [y9,z9] ; ::_thesis: y1 = y2 z = z9 by A5, A7, XTUPLE_0:1; hence y1 = y2 by A5, A6, A7, A8, XTUPLE_0:1; ::_thesis: verum end; A9: for x being set st x in D holds ex y1 being set st S1[x,y1] proof let x be set ; ::_thesis: ( x in D implies ex y1 being set st S1[x,y1] ) assume x in D ; ::_thesis: ex y1 being set st S1[x,y1] then consider y, z being set such that A10: x = [z,y] and [y,z] in dom f by A3; take f . [y,z] ; ::_thesis: S1[x,f . [y,z]] thus S1[x,f . [y,z]] by A10; ::_thesis: verum end; consider h being Function such that A11: dom h = D and A12: for x being set st x in D holds S1[x,h . x] from FUNCT_1:sch_2(A4, A9); take h ; ::_thesis: ( ( for x being set holds ( x in dom h iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds h . (z,y) = f . (y,z) ) ) thus A13: for x being set holds ( x in dom h iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ::_thesis: for y, z being set st [y,z] in dom f holds h . (z,y) = f . (y,z) proof let x be set ; ::_thesis: ( x in dom h iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) thus ( x in dom h implies ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) by A3, A11; ::_thesis: ( ex y, z being set st ( x = [z,y] & [y,z] in dom f ) implies x in dom h ) given y, z being set such that A14: x = [z,y] and A15: [y,z] in dom f ; ::_thesis: x in dom h y in union (union (dom f)) by A15, ZFMISC_1:134; then A16: y in D1 by A1, A15; z in union (union (dom f)) by A15, ZFMISC_1:134; then z in D2 by A2, A15; then [z,y] in [:D2,D1:] by A16, ZFMISC_1:87; hence x in dom h by A3, A11, A14, A15; ::_thesis: verum end; let y, z be set ; ::_thesis: ( [y,z] in dom f implies h . (z,y) = f . (y,z) ) assume [y,z] in dom f ; ::_thesis: h . (z,y) = f . (y,z) then [z,y] in D by A11, A13; then consider y9, z9 being set such that A17: [z,y] = [z9,y9] and A18: h . (z,y) = f . [y9,z9] by A12; z = z9 by A17, XTUPLE_0:1; hence h . (z,y) = f . (y,z) by A17, A18, XTUPLE_0:1; ::_thesis: verum end; uniqueness for b1, b2 being Function st ( for x being set holds ( x in dom b1 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds b1 . (z,y) = f . (y,z) ) & ( for x being set holds ( x in dom b2 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds b2 . (z,y) = f . (y,z) ) holds b1 = b2 proof let h1, h2 be Function; ::_thesis: ( ( for x being set holds ( x in dom h1 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds h1 . (z,y) = f . (y,z) ) & ( for x being set holds ( x in dom h2 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds h2 . (z,y) = f . (y,z) ) implies h1 = h2 ) assume that A19: for x being set holds ( x in dom h1 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) and A20: for y, z being set st [y,z] in dom f holds h1 . (z,y) = f . (y,z) and A21: for x being set holds ( x in dom h2 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) and A22: for y, z being set st [y,z] in dom f holds h2 . (z,y) = f . (y,z) ; ::_thesis: h1 = h2 A23: for x being set st x in dom h1 holds h1 . x = h2 . x proof let x be set ; ::_thesis: ( x in dom h1 implies h1 . x = h2 . x ) assume x in dom h1 ; ::_thesis: h1 . x = h2 . x then consider x1, x2 being set such that A24: x = [x2,x1] and A25: [x1,x2] in dom f by A19; h1 . (x2,x1) = f . (x1,x2) by A20, A25 .= h2 . (x2,x1) by A22, A25 ; hence h1 . x = h2 . x by A24; ::_thesis: verum end; for x being set holds ( x in dom h1 iff x in dom h2 ) proof let x be set ; ::_thesis: ( x in dom h1 iff x in dom h2 ) ( x in dom h1 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) by A19; hence ( x in dom h1 iff x in dom h2 ) by A21; ::_thesis: verum end; then dom h1 = dom h2 by TARSKI:1; hence h1 = h2 by A23, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines ~ FUNCT_4:def_2_:_ for f, b2 being Function holds ( b2 = ~ f iff ( ( for x being set holds ( x in dom b2 iff ex y, z being set st ( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds b2 . (z,y) = f . (y,z) ) ) ); theorem Th41: :: FUNCT_4:41 for f being Function holds rng (~ f) c= rng f proof let f be Function; ::_thesis: rng (~ f) c= rng f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (~ f) or y in rng f ) assume y in rng (~ f) ; ::_thesis: y in rng f then consider x being set such that A1: x in dom (~ f) and A2: y = (~ f) . x by FUNCT_1:def_3; consider x1, x2 being set such that A3: x = [x2,x1] and A4: [x1,x2] in dom f by A1, Def2; y = (~ f) . (x2,x1) by A2, A3 .= f . (x1,x2) by A4, Def2 ; hence y in rng f by A4, FUNCT_1:def_3; ::_thesis: verum end; theorem Th42: :: FUNCT_4:42 for x, y being set for f being Function holds ( [x,y] in dom f iff [y,x] in dom (~ f) ) proof let x, y be set ; ::_thesis: for f being Function holds ( [x,y] in dom f iff [y,x] in dom (~ f) ) let f be Function; ::_thesis: ( [x,y] in dom f iff [y,x] in dom (~ f) ) thus ( [x,y] in dom f implies [y,x] in dom (~ f) ) by Def2; ::_thesis: ( [y,x] in dom (~ f) implies [x,y] in dom f ) assume [y,x] in dom (~ f) ; ::_thesis: [x,y] in dom f then consider x1, y1 being set such that A1: [y,x] = [y1,x1] and A2: [x1,y1] in dom f by Def2; x1 = x by A1, XTUPLE_0:1; hence [x,y] in dom f by A1, A2, XTUPLE_0:1; ::_thesis: verum end; theorem :: FUNCT_4:43 for y, x being set for f being Function st [y,x] in dom (~ f) holds (~ f) . (y,x) = f . (x,y) proof let y, x be set ; ::_thesis: for f being Function st [y,x] in dom (~ f) holds (~ f) . (y,x) = f . (x,y) let f be Function; ::_thesis: ( [y,x] in dom (~ f) implies (~ f) . (y,x) = f . (x,y) ) assume [y,x] in dom (~ f) ; ::_thesis: (~ f) . (y,x) = f . (x,y) then [x,y] in dom f by Th42; hence (~ f) . (y,x) = f . (x,y) by Def2; ::_thesis: verum end; theorem :: FUNCT_4:44 for f being Function ex X, Y being set st dom (~ f) c= [:X,Y:] proof let f be Function; ::_thesis: ex X, Y being set st dom (~ f) c= [:X,Y:] now__::_thesis:_for_z_being_set_st_z_in_dom_(~_f)_holds_ ex_x,_y_being_set_st_z_=_[x,y] let z be set ; ::_thesis: ( z in dom (~ f) implies ex x, y being set st z = [x,y] ) assume z in dom (~ f) ; ::_thesis: ex x, y being set st z = [x,y] then ex x, y being set st ( z = [y,x] & [x,y] in dom f ) by Def2; hence ex x, y being set st z = [x,y] ; ::_thesis: verum end; hence ex X, Y being set st dom (~ f) c= [:X,Y:] by Th1; ::_thesis: verum end; theorem Th45: :: FUNCT_4:45 for X, Y being set for f being Function st dom f c= [:X,Y:] holds dom (~ f) c= [:Y,X:] proof let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds dom (~ f) c= [:Y,X:] let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies dom (~ f) c= [:Y,X:] ) assume A1: dom f c= [:X,Y:] ; ::_thesis: dom (~ f) c= [:Y,X:] let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (~ f) or z in [:Y,X:] ) assume z in dom (~ f) ; ::_thesis: z in [:Y,X:] then ex x, y being set st ( z = [y,x] & [x,y] in dom f ) by Def2; hence z in [:Y,X:] by A1, ZFMISC_1:88; ::_thesis: verum end; theorem Th46: :: FUNCT_4:46 for X, Y being set for f being Function st dom f = [:X,Y:] holds dom (~ f) = [:Y,X:] proof let X, Y be set ; ::_thesis: for f being Function st dom f = [:X,Y:] holds dom (~ f) = [:Y,X:] let f be Function; ::_thesis: ( dom f = [:X,Y:] implies dom (~ f) = [:Y,X:] ) assume A1: dom f = [:X,Y:] ; ::_thesis: dom (~ f) = [:Y,X:] hence dom (~ f) c= [:Y,X:] by Th45; :: according to XBOOLE_0:def_10 ::_thesis: [:Y,X:] c= dom (~ f) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:Y,X:] or z in dom (~ f) ) assume z in [:Y,X:] ; ::_thesis: z in dom (~ f) then consider y, x being set such that A2: ( y in Y & x in X ) and A3: z = [y,x] by ZFMISC_1:def_2; [x,y] in dom f by A1, A2, ZFMISC_1:def_2; hence z in dom (~ f) by A3, Def2; ::_thesis: verum end; theorem Th47: :: FUNCT_4:47 for X, Y being set for f being Function st dom f c= [:X,Y:] holds rng (~ f) = rng f proof let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds rng (~ f) = rng f let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies rng (~ f) = rng f ) assume A1: dom f c= [:X,Y:] ; ::_thesis: rng (~ f) = rng f thus rng (~ f) c= rng f by Th41; :: according to XBOOLE_0:def_10 ::_thesis: rng f c= rng (~ f) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in rng (~ f) ) assume y in rng f ; ::_thesis: y in rng (~ f) then consider x being set such that A2: x in dom f and A3: y = f . x by FUNCT_1:def_3; consider x1, y1 being set such that x1 in X and y1 in Y and A4: x = [x1,y1] by A1, A2, ZFMISC_1:84; A5: [y1,x1] in dom (~ f) by A2, A4, Th42; y = f . (x1,y1) by A3, A4 .= (~ f) . (y1,x1) by A2, A4, Def2 ; hence y in rng (~ f) by A5, FUNCT_1:def_3; ::_thesis: verum end; theorem :: FUNCT_4:48 for X, Y, Z being set for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z proof let X, Y, Z be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z holds ~ f is PartFunc of [:Y,X:],Z let f be PartFunc of [:X,Y:],Z; ::_thesis: ~ f is PartFunc of [:Y,X:],Z A1: dom f c= [:X,Y:] ; then A2: dom (~ f) c= [:Y,X:] by Th45; rng f c= Z ; then rng (~ f) c= Z by A1, Th47; hence ~ f is PartFunc of [:Y,X:],Z by A2, RELSET_1:4; ::_thesis: verum end; theorem Th49: :: FUNCT_4:49 for X, Y, Z being set for f being Function of [:X,Y:],Z st Z <> {} holds ~ f is Function of [:Y,X:],Z proof let X, Y, Z be set ; ::_thesis: for f being Function of [:X,Y:],Z st Z <> {} holds ~ f is Function of [:Y,X:],Z let f be Function of [:X,Y:],Z; ::_thesis: ( Z <> {} implies ~ f is Function of [:Y,X:],Z ) assume A1: Z <> {} ; ::_thesis: ~ f is Function of [:Y,X:],Z then A2: dom f = [:X,Y:] by FUNCT_2:def_1; then A3: [:Y,X:] = dom (~ f) by Th46; rng f c= Z ; then rng (~ f) c= Z by A2, Th47; then reconsider R = ~ f as Relation of [:Y,X:],Z by A3, RELSET_1:4; R is quasi_total proof percases ( Z <> {} or Z = {} ) ; :: according to FUNCT_2:def_1 case Z <> {} ; ::_thesis: [:Y,X:] = dom R dom f = [:X,Y:] by A1, FUNCT_2:def_1; hence [:Y,X:] = dom R by Th46; ::_thesis: verum end; case Z = {} ; ::_thesis: R = {} hence R = {} ; ::_thesis: verum end; end; end; hence ~ f is Function of [:Y,X:],Z ; ::_thesis: verum end; theorem :: FUNCT_4:50 for X, Y being set for D being non empty set for f being Function of [:X,Y:],D holds ~ f is Function of [:Y,X:],D by Th49; theorem Th51: :: FUNCT_4:51 for f being Function holds ~ (~ f) c= f proof let f be Function; ::_thesis: ~ (~ f) c= f A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(~_(~_f))_holds_ ex_y2,_z2_being_set_st_ (_x_=_[z2,y2]_&_[y2,z2]_in_dom_(~_f)_&_[z2,y2]_in_dom_f_) let x be set ; ::_thesis: ( x in dom (~ (~ f)) implies ex y2, z2 being set st ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) ) assume x in dom (~ (~ f)) ; ::_thesis: ex y2, z2 being set st ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) then consider y2, z2 being set such that A2: ( x = [z2,y2] & [y2,z2] in dom (~ f) ) by Def2; take y2 = y2; ::_thesis: ex z2 being set st ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) take z2 = z2; ::_thesis: ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) thus ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A2, Th42; ::_thesis: verum end; A3: for x being set st x in dom (~ (~ f)) holds (~ (~ f)) . x = f . x proof let x be set ; ::_thesis: ( x in dom (~ (~ f)) implies (~ (~ f)) . x = f . x ) assume x in dom (~ (~ f)) ; ::_thesis: (~ (~ f)) . x = f . x then consider y2, z2 being set such that A4: x = [z2,y2] and A5: [y2,z2] in dom (~ f) and A6: [z2,y2] in dom f by A1; (~ (~ f)) . (z2,y2) = (~ f) . (y2,z2) by A5, Def2 .= f . (z2,y2) by A6, Def2 ; hence (~ (~ f)) . x = f . x by A4; ::_thesis: verum end; dom (~ (~ f)) c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (~ (~ f)) or x in dom f ) assume x in dom (~ (~ f)) ; ::_thesis: x in dom f then ex y2, z2 being set st ( x = [z2,y2] & [y2,z2] in dom (~ f) & [z2,y2] in dom f ) by A1; hence x in dom f ; ::_thesis: verum end; hence ~ (~ f) c= f by A3, GRFUNC_1:2; ::_thesis: verum end; theorem Th52: :: FUNCT_4:52 for X, Y being set for f being Function st dom f c= [:X,Y:] holds ~ (~ f) = f proof let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds ~ (~ f) = f let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies ~ (~ f) = f ) assume A1: dom f c= [:X,Y:] ; ::_thesis: ~ (~ f) = f A2: ~ (~ f) c= f by Th51; dom (~ (~ f)) = dom f proof thus dom (~ (~ f)) c= dom f by A2, RELAT_1:11; :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (~ (~ f)) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in dom (~ (~ f)) ) assume A3: z in dom f ; ::_thesis: z in dom (~ (~ f)) then consider x, y being set such that x in X and y in Y and A4: z = [x,y] by A1, ZFMISC_1:84; [y,x] in dom (~ f) by A3, A4, Th42; hence z in dom (~ (~ f)) by A4, Th42; ::_thesis: verum end; hence ~ (~ f) = f by Th51, GRFUNC_1:3; ::_thesis: verum end; theorem :: FUNCT_4:53 for X, Y, Z being set for f being PartFunc of [:X,Y:],Z holds ~ (~ f) = f proof let X, Y, Z be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z holds ~ (~ f) = f let f be PartFunc of [:X,Y:],Z; ::_thesis: ~ (~ f) = f dom f c= [:X,Y:] ; hence ~ (~ f) = f by Th52; ::_thesis: verum end; definition let f, g be Function; func|:f,g:| -> Function means :Def3: :: FUNCT_4:def 3 ( ( for z being set holds ( z in dom it iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds it . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ); existence ex b1 being Function st ( ( for z being set holds ( z in dom b1 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds b1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) proof defpred S1[ set , set ] means ex x, y, x9, y9 being set st ( \$1 = [[x,x9],[y,y9]] & \$2 = [(f . [x,y]),(g . [x9,y9])] ); defpred S2[ set ] means ex y being set st [\$1,y] in dom f; consider D1 being set such that A1: for x being set holds ( x in D1 iff ( x in union (union (dom f)) & S2[x] ) ) from XBOOLE_0:sch_1(); defpred S3[ set ] means ex x being set st [x,\$1] in dom f; consider D2 being set such that A2: for y being set holds ( y in D2 iff ( y in union (union (dom f)) & S3[y] ) ) from XBOOLE_0:sch_1(); defpred S4[ set ] means ex y being set st [\$1,y] in dom g; consider D19 being set such that A3: for x being set holds ( x in D19 iff ( x in union (union (dom g)) & S4[x] ) ) from XBOOLE_0:sch_1(); defpred S5[ set ] means ex x being set st [x,\$1] in dom g; consider D29 being set such that A4: for y being set holds ( y in D29 iff ( y in union (union (dom g)) & S5[y] ) ) from XBOOLE_0:sch_1(); defpred S6[ set ] means ex x, y, x9, y9 being set st ( \$1 = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ); consider D being set such that A5: for z being set holds ( z in D iff ( z in [:[:D1,D19:],[:D2,D29:]:] & S6[z] ) ) from XBOOLE_0:sch_1(); A6: for z, z1, z2 being set st z in D & S1[z,z1] & S1[z,z2] holds z1 = z2 proof let z, z1, z2 be set ; ::_thesis: ( z in D & S1[z,z1] & S1[z,z2] implies z1 = z2 ) assume z in D ; ::_thesis: ( not S1[z,z1] or not S1[z,z2] or z1 = z2 ) given x, y, x9, y9 being set such that A7: z = [[x,x9],[y,y9]] and A8: z1 = [(f . [x,y]),(g . [x9,y9])] ; ::_thesis: ( not S1[z,z2] or z1 = z2 ) given x1, y1, x19, y19 being set such that A9: z = [[x1,x19],[y1,y19]] and A10: z2 = [(f . [x1,y1]),(g . [x19,y19])] ; ::_thesis: z1 = z2 A11: x9 = x19 by A7, A9, Lm1; ( x = x1 & y = y1 ) by A7, A9, Lm1; hence z1 = z2 by A7, A8, A9, A10, A11, Lm1; ::_thesis: verum end; A12: for z being set st z in D holds ex z1 being set st S1[z,z1] proof let z be set ; ::_thesis: ( z in D implies ex z1 being set st S1[z,z1] ) assume z in D ; ::_thesis: ex z1 being set st S1[z,z1] then consider x, y, x9, y9 being set such that A13: z = [[x,x9],[y,y9]] and [x,y] in dom f and [x9,y9] in dom g by A5; take [(f . [x,y]),(g . [x9,y9])] ; ::_thesis: S1[z,[(f . [x,y]),(g . [x9,y9])]] thus S1[z,[(f . [x,y]),(g . [x9,y9])]] by A13; ::_thesis: verum end; consider h being Function such that A14: dom h = D and A15: for z being set st z in D holds S1[z,h . z] from FUNCT_1:sch_2(A6, A12); take h ; ::_thesis: ( ( for z being set holds ( z in dom h iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) thus A16: for z being set holds ( z in dom h iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ::_thesis: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] proof let z be set ; ::_thesis: ( z in dom h iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) thus ( z in dom h implies ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) by A5, A14; ::_thesis: ( ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) implies z in dom h ) given x, y, x9, y9 being set such that A17: z = [[x,x9],[y,y9]] and A18: [x,y] in dom f and A19: [x9,y9] in dom g ; ::_thesis: z in dom h y9 in union (union (dom g)) by A19, ZFMISC_1:134; then A20: y9 in D29 by A4, A19; y in union (union (dom f)) by A18, ZFMISC_1:134; then y in D2 by A2, A18; then A21: [y,y9] in [:D2,D29:] by A20, ZFMISC_1:87; x9 in union (union (dom g)) by A19, ZFMISC_1:134; then A22: x9 in D19 by A3, A19; x in union (union (dom f)) by A18, ZFMISC_1:134; then x in D1 by A1, A18; then [x,x9] in [:D1,D19:] by A22, ZFMISC_1:87; then z in [:[:D1,D19:],[:D2,D29:]:] by A17, A21, ZFMISC_1:87; hence z in dom h by A5, A14, A17, A18, A19; ::_thesis: verum end; let x, y, x9, y9 be set ; ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g implies h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) assume ( [x,y] in dom f & [x9,y9] in dom g ) ; ::_thesis: h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] then [[x,x9],[y,y9]] in D by A14, A16; then consider x1, y1, x19, y19 being set such that A23: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and A24: h . [[x,x9],[y,y9]] = [(f . [x1,y1]),(g . [x19,y19])] by A15; A25: x9 = x19 by A23, Lm1; ( x = x1 & y = y1 ) by A23, Lm1; hence h . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by A23, A24, A25, Lm1; ::_thesis: verum end; uniqueness for b1, b2 being Function st ( for z being set holds ( z in dom b1 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds b1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being set holds ( z in dom b2 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds b2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) holds b1 = b2 proof let h1, h2 be Function; ::_thesis: ( ( for z being set holds ( z in dom h1 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) & ( for z being set holds ( z in dom h2 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) implies h1 = h2 ) assume that A26: for z being set holds ( z in dom h1 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and A27: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] and A28: for z being set holds ( z in dom h2 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) and A29: for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds h2 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ; ::_thesis: h1 = h2 A30: for z being set st z in dom h1 holds h1 . z = h2 . z proof let z be set ; ::_thesis: ( z in dom h1 implies h1 . z = h2 . z ) assume z in dom h1 ; ::_thesis: h1 . z = h2 . z then consider x, y, x9, y9 being set such that A31: z = [[x,x9],[y,y9]] and A32: ( [x,y] in dom f & [x9,y9] in dom g ) by A26; h1 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by A27, A32 .= h2 . ([x,x9],[y,y9]) by A29, A32 ; hence h1 . z = h2 . z by A31; ::_thesis: verum end; for z being set holds ( z in dom h1 iff z in dom h2 ) proof let z be set ; ::_thesis: ( z in dom h1 iff z in dom h2 ) ( z in dom h1 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) by A26; hence ( z in dom h1 iff z in dom h2 ) by A28; ::_thesis: verum end; then dom h1 = dom h2 by TARSKI:1; hence h1 = h2 by A30, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines |: FUNCT_4:def_3_:_ for f, g, b3 being Function holds ( b3 = |:f,g:| iff ( ( for z being set holds ( z in dom b3 iff ex x, y, x9, y9 being set st ( z = [[x,x9],[y,y9]] & [x,y] in dom f & [x9,y9] in dom g ) ) ) & ( for x, y, x9, y9 being set st [x,y] in dom f & [x9,y9] in dom g holds b3 . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) ) ); theorem Th54: :: FUNCT_4:54 for x, x9, y, y9 being set for f, g being Function holds ( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) ) proof let x, x9, y, y9 be set ; ::_thesis: for f, g being Function holds ( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) ) let f, g be Function; ::_thesis: ( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) ) thus ( [[x,x9],[y,y9]] in dom |:f,g:| implies ( [x,y] in dom f & [x9,y9] in dom g ) ) ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| ) proof assume [[x,x9],[y,y9]] in dom |:f,g:| ; ::_thesis: ( [x,y] in dom f & [x9,y9] in dom g ) then consider x1, y1, x19, y19 being set such that A1: [[x,x9],[y,y9]] = [[x1,x19],[y1,y19]] and A2: ( [x1,y1] in dom f & [x19,y19] in dom g ) by Def3; ( x = x1 & x9 = x19 ) by A1, Lm1; hence ( [x,y] in dom f & [x9,y9] in dom g ) by A1, A2, Lm1; ::_thesis: verum end; thus ( [x,y] in dom f & [x9,y9] in dom g implies [[x,x9],[y,y9]] in dom |:f,g:| ) by Def3; ::_thesis: verum end; theorem :: FUNCT_4:55 for x, x9, y, y9 being set for f, g being Function st [[x,x9],[y,y9]] in dom |:f,g:| holds |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] proof let x, x9, y, y9 be set ; ::_thesis: for f, g being Function st [[x,x9],[y,y9]] in dom |:f,g:| holds |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] let f, g be Function; ::_thesis: ( [[x,x9],[y,y9]] in dom |:f,g:| implies |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] ) assume [[x,x9],[y,y9]] in dom |:f,g:| ; ::_thesis: |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] then ( [x,y] in dom f & [x9,y9] in dom g ) by Th54; hence |:f,g:| . ([x,x9],[y,y9]) = [(f . (x,y)),(g . (x9,y9))] by Def3; ::_thesis: verum end; theorem Th56: :: FUNCT_4:56 for f, g being Function holds rng |:f,g:| c= [:(rng f),(rng g):] proof let f, g be Function; ::_thesis: rng |:f,g:| c= [:(rng f),(rng g):] let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng |:f,g:| or z in [:(rng f),(rng g):] ) assume z in rng |:f,g:| ; ::_thesis: z in [:(rng f),(rng g):] then consider p being set such that A1: p in dom |:f,g:| and A2: z = |:f,g:| . p by FUNCT_1:def_3; consider x, y, x9, y9 being set such that A3: p = [[x,x9],[y,y9]] and A4: ( [x,y] in dom f & [x9,y9] in dom g ) by A1, Def3; A5: ( f . [x,y] in rng f & g . [x9,y9] in rng g ) by A4, FUNCT_1:def_3; z = |:f,g:| . ([x,x9],[y,y9]) by A2, A3 .= [(f . (x,y)),(g . (x9,y9))] by A4, Def3 ; hence z in [:(rng f),(rng g):] by A5, ZFMISC_1:87; ::_thesis: verum end; theorem Th57: :: FUNCT_4:57 for X, Y, X9, Y9 being set for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] proof let X, Y, X9, Y9 be set ; ::_thesis: for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] let f, g be Function; ::_thesis: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] implies dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] ) assume A1: ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ; ::_thesis: dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] let xy be set ; :: according to TARSKI:def_3 ::_thesis: ( not xy in dom |:f,g:| or xy in [:[:X,X9:],[:Y,Y9:]:] ) assume xy in dom |:f,g:| ; ::_thesis: xy in [:[:X,X9:],[:Y,Y9:]:] then consider x, y, x9, y9 being set such that A2: xy = [[x,x9],[y,y9]] and A3: ( [x,y] in dom f & [x9,y9] in dom g ) by Def3; ( y in Y & y9 in Y9 ) by A1, A3, ZFMISC_1:87; then A4: [y,y9] in [:Y,Y9:] by ZFMISC_1:87; ( x in X & x9 in X9 ) by A1, A3, ZFMISC_1:87; then [x,x9] in [:X,X9:] by ZFMISC_1:87; hence xy in [:[:X,X9:],[:Y,Y9:]:] by A2, A4, ZFMISC_1:87; ::_thesis: verum end; theorem Th58: :: FUNCT_4:58 for X, Y, X9, Y9 being set for f, g being Function st dom f = [:X,Y:] & dom g = [:X9,Y9:] holds dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:] proof let X, Y, X9, Y9 be set ; ::_thesis: for f, g being Function st dom f = [:X,Y:] & dom g = [:X9,Y9:] holds dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:] let f, g be Function; ::_thesis: ( dom f = [:X,Y:] & dom g = [:X9,Y9:] implies dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:] ) assume A1: ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) ; ::_thesis: dom |:f,g:| = [:[:X,X9:],[:Y,Y9:]:] hence dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57; :: according to XBOOLE_0:def_10 ::_thesis: [:[:X,X9:],[:Y,Y9:]:] c= dom |:f,g:| let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:[:X,X9:],[:Y,Y9:]:] or z in dom |:f,g:| ) assume z in [:[:X,X9:],[:Y,Y9:]:] ; ::_thesis: z in dom |:f,g:| then consider xx, yy being set such that A2: xx in [:X,X9:] and A3: yy in [:Y,Y9:] and A4: z = [xx,yy] by ZFMISC_1:def_2; consider y, y9 being set such that A5: ( y in Y & y9 in Y9 ) and A6: yy = [y,y9] by A3, ZFMISC_1:def_2; consider x, x9 being set such that A7: ( x in X & x9 in X9 ) and A8: xx = [x,x9] by A2, ZFMISC_1:def_2; ( [x,y] in dom f & [x9,y9] in dom g ) by A1, A7, A5, ZFMISC_1:87; hence z in dom |:f,g:| by A4, A8, A6, Def3; ::_thesis: verum end; theorem :: FUNCT_4:59 for X, Y, Z, X9, Y9, Z9 being set for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] proof let X, Y, Z, X9, Y9, Z9 be set ; ::_thesis: for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] let f be PartFunc of [:X,Y:],Z; ::_thesis: for g being PartFunc of [:X9,Y9:],Z9 holds |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] let g be PartFunc of [:X9,Y9:],Z9; ::_thesis: |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] ( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z9:] ) by Th56, ZFMISC_1:96; then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1; ( dom f c= [:X,Y:] & dom g c= [:X9,Y9:] ) ; then dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:] by Th57; hence |:f,g:| is PartFunc of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4; ::_thesis: verum end; theorem Th60: :: FUNCT_4:60 for X, Y, Z, X9, Y9, Z9 being set for f being Function of [:X,Y:],Z for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] proof let X, Y, Z, X9, Y9, Z9 be set ; ::_thesis: for f being Function of [:X,Y:],Z for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] let f be Function of [:X,Y:],Z; ::_thesis: for g being Function of [:X9,Y9:],Z9 st Z <> {} & Z9 <> {} holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] let g be Function of [:X9,Y9:],Z9; ::_thesis: ( Z <> {} & Z9 <> {} implies |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] ) ( rng |:f,g:| c= [:(rng f),(rng g):] & [:(rng f),(rng g):] c= [:Z,Z9:] ) by Th56, ZFMISC_1:96; then A1: rng |:f,g:| c= [:Z,Z9:] by XBOOLE_1:1; assume A2: ( Z <> {} & Z9 <> {} ) ; ::_thesis: |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] then ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by FUNCT_2:def_1; then [:[:X,X9:],[:Y,Y9:]:] = dom |:f,g:| by Th58; then reconsider R = |:f,g:| as Relation of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] by A1, RELSET_1:4; R is quasi_total proof percases ( [:Z,Z9:] <> {} or [:Z,Z9:] = {} ) ; :: according to FUNCT_2:def_1 case [:Z,Z9:] <> {} ; ::_thesis: [:[:X,X9:],[:Y,Y9:]:] = dom R ( dom f = [:X,Y:] & dom g = [:X9,Y9:] ) by A2, FUNCT_2:def_1; hence [:[:X,X9:],[:Y,Y9:]:] = dom R by Th58; ::_thesis: verum end; case [:Z,Z9:] = {} ; ::_thesis: R = {} hence R = {} ; ::_thesis: verum end; end; end; hence |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:Z,Z9:] ; ::_thesis: verum end; theorem :: FUNCT_4:61 for X, Y, X9, Y9 being set for D, D9 being non empty set for f being Function of [:X,Y:],D for g being Function of [:X9,Y9:],D9 holds |:f,g:| is Function of [:[:X,X9:],[:Y,Y9:]:],[:D,D9:] by Th60; definition let x, y, a, b be set ; func(x,y) --> (a,b) -> set equals :: FUNCT_4:def 4 (x .--> a) +* (y .--> b); correctness coherence (x .--> a) +* (y .--> b) is set ; ; end; :: deftheorem defines --> FUNCT_4:def_4_:_ for x, y, a, b being set holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b); registration let x, y, a, b be set ; cluster(x,y) --> (a,b) -> Relation-like Function-like ; coherence ( (x,y) --> (a,b) is Function-like & (x,y) --> (a,b) is Relation-like ) ; end; theorem Th62: :: FUNCT_4:62 for x1, x2, y1, y2 being set holds ( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} ) proof let x1, x2, y1, y2 be set ; ::_thesis: ( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} ) set f = {x1} --> y1; set g = {x2} --> y2; set h = (x1,x2) --> (y1,y2); (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1} \/ {y2} by XBOOLE_1:13; then A1: (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1,y2} by ENUMSET1:1; ( dom ({x1} --> y1) = {x1} & dom ({x2} --> y2) = {x2} ) by FUNCOP_1:13; then (dom ({x1} --> y1)) \/ (dom ({x2} --> y2)) = {x1,x2} by ENUMSET1:1; hence dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Def1; ::_thesis: rng ((x1,x2) --> (y1,y2)) c= {y1,y2} rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th17; hence rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th63: :: FUNCT_4:63 for x1, x2, y1, y2 being set holds ( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 ) proof let x1, x2, y1, y2 be set ; ::_thesis: ( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 ) set f = {x1} --> y1; set g = {x2} --> y2; set h = (x1,x2) --> (y1,y2); A1: x2 in {x2} by TARSKI:def_1; A2: x1 in {x1} by TARSKI:def_1; hereby ::_thesis: ((x1,x2) --> (y1,y2)) . x2 = y2 assume x1 <> x2 ; ::_thesis: ((x1,x2) --> (y1,y2)) . x1 = y1 then not x1 in dom ({x2} --> y2) by TARSKI:def_1; then ((x1,x2) --> (y1,y2)) . x1 = ({x1} --> y1) . x1 by Th11; hence ((x1,x2) --> (y1,y2)) . x1 = y1 by A2, FUNCOP_1:7; ::_thesis: verum end; {x2} = dom ({x2} --> y2) by FUNCOP_1:13; then ((x1,x2) --> (y1,y2)) . x2 = ({x2} --> y2) . x2 by A1, Th13; hence ((x1,x2) --> (y1,y2)) . x2 = y2 by A1, FUNCOP_1:7; ::_thesis: verum end; theorem :: FUNCT_4:64 for x1, x2, y1, y2 being set st x1 <> x2 holds rng ((x1,x2) --> (y1,y2)) = {y1,y2} proof let x1, x2, y1, y2 be set ; ::_thesis: ( x1 <> x2 implies rng ((x1,x2) --> (y1,y2)) = {y1,y2} ) set h = (x1,x2) --> (y1,y2); assume A1: x1 <> x2 ; ::_thesis: rng ((x1,x2) --> (y1,y2)) = {y1,y2} thus rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by Th62; :: according to XBOOLE_0:def_10 ::_thesis: {y1,y2} c= rng ((x1,x2) --> (y1,y2)) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {y1,y2} or y in rng ((x1,x2) --> (y1,y2)) ) assume y in {y1,y2} ; ::_thesis: y in rng ((x1,x2) --> (y1,y2)) then ( y = y1 or y = y2 ) by TARSKI:def_2; then A2: ( ((x1,x2) --> (y1,y2)) . x1 = y or ((x1,x2) --> (y1,y2)) . x2 = y ) by A1, Th63; dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62; then ( x1 in dom ((x1,x2) --> (y1,y2)) & x2 in dom ((x1,x2) --> (y1,y2)) ) by TARSKI:def_2; hence y in rng ((x1,x2) --> (y1,y2)) by A2, FUNCT_1:def_3; ::_thesis: verum end; theorem :: FUNCT_4:65 for x1, x2, y being set holds (x1,x2) --> (y,y) = {x1,x2} --> y proof let x1, x2, y be set ; ::_thesis: (x1,x2) --> (y,y) = {x1,x2} --> y set F = (x1,x2) --> (y,y); set f = {x1} --> y; set g = {x2} --> y; set F9 = {x1,x2} --> y; now__::_thesis:_(_dom_((x1,x2)_-->_(y,y))_=_{x1,x2}_&_dom_({x1,x2}_-->_y)_=_{x1,x2}_&_(_for_x_being_set_st_x_in_{x1,x2}_holds_ ((x1,x2)_-->_(y,y))_._x_=_({x1,x2}_-->_y)_._x_)_) thus A1: ( dom ((x1,x2) --> (y,y)) = {x1,x2} & dom ({x1,x2} --> y) = {x1,x2} ) by Th62, FUNCOP_1:13; ::_thesis: for x being set st x in {x1,x2} holds ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x let x be set ; ::_thesis: ( x in {x1,x2} implies ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x ) assume A2: x in {x1,x2} ; ::_thesis: ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x now__::_thesis:_(_((x1,x2)_-->_(y,y))_._x_=_y_&_({x1,x2}_-->_y)_._x_=_y_) percases ( ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) or x in dom ({x2} --> y) ) by A1, A2, Th12; supposeA3: ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) ; ::_thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) then ((x1,x2) --> (y,y)) . x = ({x1} --> y) . x by Th11; hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A3, FUNCOP_1:7; ::_thesis: verum end; supposeA4: x in dom ({x2} --> y) ; ::_thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) then ((x1,x2) --> (y,y)) . x = ({x2} --> y) . x by Th13; hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A4, FUNCOP_1:7; ::_thesis: verum end; end; end; hence ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x ; ::_thesis: verum end; hence (x1,x2) --> (y,y) = {x1,x2} --> y by FUNCT_1:2; ::_thesis: verum end; definition let A be non empty set ; let x1, x2 be set ; let y1, y2 be Element of A; :: original: --> redefine func(x1,x2) --> (y1,y2) -> Function of {x1,x2},A; coherence (x1,x2) --> (y1,y2) is Function of {x1,x2},A proof set f = {x1} --> y1; set g = {x2} --> y2; set h = (x1,x2) --> (y1,y2); rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th17; then A1: rng ((x1,x2) --> (y1,y2)) c= A by XBOOLE_1:1; dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62; hence (x1,x2) --> (y1,y2) is Function of {x1,x2},A by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; theorem :: FUNCT_4:66 for a, b, c, d being set for g being Function st dom g = {a,b} & g . a = c & g . b = d holds g = (a,b) --> (c,d) proof let a, b, c, d be set ; ::_thesis: for g being Function st dom g = {a,b} & g . a = c & g . b = d holds g = (a,b) --> (c,d) let h be Function; ::_thesis: ( dom h = {a,b} & h . a = c & h . b = d implies h = (a,b) --> (c,d) ) assume that A1: dom h = {a,b} and A2: h . a = c and A3: h . b = d ; ::_thesis: h = (a,b) --> (c,d) set f = {a} --> c; set g = {b} --> d; A4: b in {b} by TARSKI:def_1; A5: a in {a} by TARSKI:def_1; A6: now__::_thesis:_for_x_being_set_st_x_in_(dom_({a}_-->_c))_\/_(dom_({b}_-->_d))_holds_ (_(_x_in_dom_({b}_-->_d)_implies_h_._x_=_({b}_-->_d)_._x_)_&_(_not_x_in_dom_({b}_-->_d)_implies_h_._x_=_({a}_-->_c)_._x_)_) let x be set ; ::_thesis: ( x in (dom ({a} --> c)) \/ (dom ({b} --> d)) implies ( ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) & ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) ) ) assume A7: x in (dom ({a} --> c)) \/ (dom ({b} --> d)) ; ::_thesis: ( ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) & ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) ) thus ( x in dom ({b} --> d) implies h . x = ({b} --> d) . x ) ::_thesis: ( not x in dom ({b} --> d) implies h . x = ({a} --> c) . x ) proof assume x in dom ({b} --> d) ; ::_thesis: h . x = ({b} --> d) . x then x = b by TARSKI:def_1; hence h . x = ({b} --> d) . x by A3, A4, FUNCOP_1:7; ::_thesis: verum end; assume not x in dom ({b} --> d) ; ::_thesis: h . x = ({a} --> c) . x then x in dom ({a} --> c) by A7, XBOOLE_0:def_3; then x = a by TARSKI:def_1; hence h . x = ({a} --> c) . x by A2, A5, FUNCOP_1:7; ::_thesis: verum end; ( dom ({a} --> c) = {a} & dom ({b} --> d) = {b} ) by FUNCOP_1:13; then dom h = (dom ({a} --> c)) \/ (dom ({b} --> d)) by A1, ENUMSET1:1; hence h = (a,b) --> (c,d) by A6, Def1; ::_thesis: verum end; theorem Th67: :: FUNCT_4:67 for a, b, c, d being set st a <> c holds (a,c) --> (b,d) = {[a,b],[c,d]} proof let a, b, c, d be set ; ::_thesis: ( a <> c implies (a,c) --> (b,d) = {[a,b],[c,d]} ) assume A1: a <> c ; ::_thesis: (a,c) --> (b,d) = {[a,b],[c,d]} set f = {a} --> b; set g = {c} --> d; A2: ( dom ({a} --> b) = {a} & dom ({c} --> d) = {c} ) by FUNCOP_1:13; ( {a} --> b = {[a,b]} & {c} --> d = {[c,d]} ) by ZFMISC_1:29; hence (a,c) --> (b,d) = {[a,b]} \/ {[c,d]} by A1, A2, Th31, ZFMISC_1:11 .= {[a,b],[c,d]} by ENUMSET1:1 ; ::_thesis: verum end; theorem :: FUNCT_4:68 for a, b, x, y, x9, y9 being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) holds ( x = x9 & y = y9 ) proof let a, b, x, y, x9, y9 be set ; ::_thesis: ( a <> b & (a,b) --> (x,y) = (a,b) --> (x9,y9) implies ( x = x9 & y = y9 ) ) assume that A1: a <> b and A2: (a,b) --> (x,y) = (a,b) --> (x9,y9) ; ::_thesis: ( x = x9 & y = y9 ) thus x = ((a,b) --> (x,y)) . a by A1, Th63 .= x9 by A1, A2, Th63 ; ::_thesis: y = y9 thus y = ((a,b) --> (x,y)) . b by Th63 .= y9 by A2, Th63 ; ::_thesis: verum end; begin theorem :: FUNCT_4:69 for f1, f2, g1, g2 being Function st rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 holds (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) proof let f1, f2, g1, g2 be Function; ::_thesis: ( rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2 implies (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) ) assume that A1: ( rng g1 c= dom f1 & rng g2 c= dom f2 ) and A2: f1 tolerates f2 ; ::_thesis: (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) A3: ( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & dom (f1 +* f2) = (dom f1) \/ (dom f2) ) by Def1, Th17; (rng g1) \/ (rng g2) c= (dom f1) \/ (dom f2) by A1, XBOOLE_1:13; then A4: dom ((f1 +* f2) * (g1 +* g2)) = dom (g1 +* g2) by A3, RELAT_1:27, XBOOLE_1:1 .= (dom g1) \/ (dom g2) by Def1 ; A5: ( dom (f1 * g1) = dom g1 & dom (f2 * g2) = dom g2 ) by A1, RELAT_1:27; A6: now__::_thesis:_for_x_being_set_st_x_in_(dom_g1)_\/_(dom_g2)_holds_ ((f1_+*_f2)_*_(g1_+*_g2))_._x_=_((f1_*_g1)_+*_(f2_*_g2))_._x let x be set ; ::_thesis: ( x in (dom g1) \/ (dom g2) implies ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x ) A7: ( not x in dom g2 or x in dom g2 ) ; assume A8: x in (dom g1) \/ (dom g2) ; ::_thesis: ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x then A9: ((f1 +* f2) * (g1 +* g2)) . x = (f1 +* f2) . ((g1 +* g2) . x) by A4, FUNCT_1:12; ( x in dom g1 or x in dom g2 ) by A8, XBOOLE_0:def_3; then ( ( (g1 +* g2) . x = g1 . x & ((f1 * g1) +* (f2 * g2)) . x = (f1 * g1) . x & (f1 * g1) . x = f1 . (g1 . x) & g1 . x in rng g1 & ( g1 . x in rng g1 implies g1 . x in dom f1 ) ) or ( (g1 +* g2) . x = g2 . x & ((f1 * g1) +* (f2 * g2)) . x = (f2 * g2) . x & (f2 * g2) . x = f2 . (g2 . x) & g2 . x in rng g2 & ( g2 . x in rng g2 implies g2 . x in dom f2 ) ) ) by A1, A5, A8, A7, Def1, FUNCT_1:12, FUNCT_1:def_3; hence ((f1 +* f2) * (g1 +* g2)) . x = ((f1 * g1) +* (f2 * g2)) . x by A2, A9, Th13, Th15; ::_thesis: verum end; dom ((f1 * g1) +* (f2 * g2)) = (dom g1) \/ (dom g2) by A5, Def1; hence (f1 +* f2) * (g1 +* g2) = (f1 * g1) +* (f2 * g2) by A4, A6, FUNCT_1:2; ::_thesis: verum end; theorem Th70: :: FUNCT_4:70 for f being Function for A, B being set st dom f c= A \/ B holds (f | A) +* (f | B) = f proof let f be Function; ::_thesis: for A, B being set st dom f c= A \/ B holds (f | A) +* (f | B) = f let A, B be set ; ::_thesis: ( dom f c= A \/ B implies (f | A) +* (f | B) = f ) A1: ( dom (f | A) = (dom f) /\ A & dom (f | B) = (dom f) /\ B ) by RELAT_1:61; A2: for x being set st x in (dom (f | A)) \/ (dom (f | B)) holds ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) ) proof let x be set ; ::_thesis: ( x in (dom (f | A)) \/ (dom (f | B)) implies ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) ) ) assume A3: x in (dom (f | A)) \/ (dom (f | B)) ; ::_thesis: ( ( x in dom (f | B) implies f . x = (f | B) . x ) & ( not x in dom (f | B) implies f . x = (f | A) . x ) ) thus ( x in dom (f | B) implies f . x = (f | B) . x ) by FUNCT_1:47; ::_thesis: ( not x in dom (f | B) implies f . x = (f | A) . x ) assume not x in dom (f | B) ; ::_thesis: f . x = (f | A) . x then x in dom (f | A) by A3, XBOOLE_0:def_3; hence f . x = (f | A) . x by FUNCT_1:47; ::_thesis: verum end; assume dom f c= A \/ B ; ::_thesis: (f | A) +* (f | B) = f then dom f = (dom f) /\ (A \/ B) by XBOOLE_1:28 .= (dom (f | A)) \/ (dom (f | B)) by A1, XBOOLE_1:23 ; hence (f | A) +* (f | B) = f by A2, Def1; ::_thesis: verum end; theorem Th71: :: FUNCT_4:71 for p, q being Function for A being set holds (p +* q) | A = (p | A) +* (q | A) proof let p, q be Function; ::_thesis: for A being set holds (p +* q) | A = (p | A) +* (q | A) let A be set ; ::_thesis: (p +* q) | A = (p | A) +* (q | A) A1: dom ((p +* q) | A) = (dom (p +* q)) /\ A by RELAT_1:61 .= ((dom p) \/ (dom q)) /\ A by Def1 .= ((dom p) /\ A) \/ ((dom q) /\ A) by XBOOLE_1:23 .= (dom (p | A)) \/ ((dom q) /\ A) by RELAT_1:61 .= (dom (p | A)) \/ (dom (q | A)) by RELAT_1:61 ; for x being set st x in (dom (p | A)) \/ (dom (q | A)) holds ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) ) proof let x be set ; ::_thesis: ( x in (dom (p | A)) \/ (dom (q | A)) implies ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) ) ) assume A2: x in (dom (p | A)) \/ (dom (q | A)) ; ::_thesis: ( ( x in dom (q | A) implies ((p +* q) | A) . x = (q | A) . x ) & ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) ) then ( x in dom (p | A) or x in dom (q | A) ) by XBOOLE_0:def_3; then ( x in (dom p) /\ A or x in (dom q) /\ A ) by RELAT_1:61; then A3: x in A by XBOOLE_0:def_4; hereby ::_thesis: ( not x in dom (q | A) implies ((p +* q) | A) . x = (p | A) . x ) assume A4: x in dom (q | A) ; ::_thesis: ((p +* q) | A) . x = (q | A) . x then x in (dom q) /\ A by RELAT_1:61; then A5: x in dom q by XBOOLE_0:def_4; thus ((p +* q) | A) . x = (p +* q) . x by A1, A2, FUNCT_1:47 .= q . x by A5, Th13 .= (q | A) . x by A4, FUNCT_1:47 ; ::_thesis: verum end; assume A6: not x in dom (q | A) ; ::_thesis: ((p +* q) | A) . x = (p | A) . x then not x in (dom q) /\ A by RELAT_1:61; then A7: not x in dom q by A3, XBOOLE_0:def_4; A8: x in dom (p | A) by A2, A6, XBOOLE_0:def_3; then x in (dom p) /\ A by RELAT_1:61; then x in dom p by XBOOLE_0:def_4; then x in dom (p +* q) by Th12; then x in (dom (p +* q)) /\ A by A3, XBOOLE_0:def_4; then x in dom ((p +* q) | A) by RELAT_1:61; hence ((p +* q) | A) . x = (p +* q) . x by FUNCT_1:47 .= p . x by A7, Th11 .= (p | A) . x by A8, FUNCT_1:47 ; ::_thesis: verum end; hence (p +* q) | A = (p | A) +* (q | A) by A1, Def1; ::_thesis: verum end; theorem Th72: :: FUNCT_4:72 for f, g being Function for A being set st A misses dom g holds (f +* g) | A = f | A proof let f, g be Function; ::_thesis: for A being set st A misses dom g holds (f +* g) | A = f | A let A be set ; ::_thesis: ( A misses dom g implies (f +* g) | A = f | A ) assume A misses dom g ; ::_thesis: (f +* g) | A = f | A then (dom g) /\ A = {} by XBOOLE_0:def_7; then dom (g | A) = {} by RELAT_1:61; then g | A = {} ; hence (f +* g) | A = (f | A) +* {} by Th71 .= f | A ; ::_thesis: verum end; theorem :: FUNCT_4:73 for f, g being Function for A being set st dom f misses A holds (f +* g) | A = g | A proof let f, g be Function; ::_thesis: for A being set st dom f misses A holds (f +* g) | A = g | A let A be set ; ::_thesis: ( dom f misses A implies (f +* g) | A = g | A ) assume dom f misses A ; ::_thesis: (f +* g) | A = g | A then (dom f) /\ A = {} by XBOOLE_0:def_7; then dom (f | A) = {} by RELAT_1:61; then f | A = {} ; hence (f +* g) | A = {} +* (g | A) by Th71 .= g | A ; ::_thesis: verum end; theorem :: FUNCT_4:74 for f, g, h being Function st dom g = dom h holds (f +* g) +* h = f +* h proof let f, g, h be Function; ::_thesis: ( dom g = dom h implies (f +* g) +* h = f +* h ) assume A1: dom g = dom h ; ::_thesis: (f +* g) +* h = f +* h thus (f +* g) +* h = f +* (g +* h) by Th14 .= f +* h by A1, Th19 ; ::_thesis: verum end; Lm2: for f, g being Function st f c= g holds g +* f = g proof let f, g be Function; ::_thesis: ( f c= g implies g +* f = g ) assume A1: f c= g ; ::_thesis: g +* f = g then f tolerates g by PARTFUN1:54; hence g +* f = f \/ g by Th30 .= g by A1, XBOOLE_1:12 ; ::_thesis: verum end; theorem :: FUNCT_4:75 for f being Function for A being set holds f +* (f | A) = f by Lm2, RELAT_1:59; theorem :: FUNCT_4:76 for f, g being Function for B, C being set st dom f c= B & dom g c= C & B misses C holds ( (f +* g) | B = f & (f +* g) | C = g ) proof let f, g be Function; ::_thesis: for B, C being set st dom f c= B & dom g c= C & B misses C holds ( (f +* g) | B = f & (f +* g) | C = g ) let B, C be set ; ::_thesis: ( dom f c= B & dom g c= C & B misses C implies ( (f +* g) | B = f & (f +* g) | C = g ) ) assume that A1: dom f c= B and A2: dom g c= C and A3: B misses C ; ::_thesis: ( (f +* g) | B = f & (f +* g) | C = g ) dom f misses C by A1, A3, XBOOLE_1:63; then (dom f) /\ C = {} by XBOOLE_0:def_7; then dom (f | C) = {} by RELAT_1:61; then A4: f | C = {} ; dom g misses B by A2, A3, XBOOLE_1:63; then (dom g) /\ B = {} by XBOOLE_0:def_7; then dom (g | B) = {} by RELAT_1:61; then A5: g | B = {} ; thus (f +* g) | B = (f | B) +* (g | B) by Th71 .= f | B by A5, Th21 .= f by A1, RELAT_1:68 ; ::_thesis: (f +* g) | C = g thus (f +* g) | C = (f | C) +* (g | C) by Th71 .= g | C by A4, Th20 .= g by A2, RELAT_1:68 ; ::_thesis: verum end; theorem :: FUNCT_4:77 for p, q being Function for A being set st dom p c= A & dom q misses A holds (p +* q) | A = p proof let p, q be Function; ::_thesis: for A being set st dom p c= A & dom q misses A holds (p +* q) | A = p let A be set ; ::_thesis: ( dom p c= A & dom q misses A implies (p +* q) | A = p ) assume that A1: dom p c= A and A2: dom q misses A ; ::_thesis: (p +* q) | A = p thus (p +* q) | A = p | A by A2, Th72 .= p by A1, RELAT_1:68 ; ::_thesis: verum end; theorem :: FUNCT_4:78 for f being Function for A, B being set holds f | (A \/ B) = (f | A) +* (f | B) proof let f be Function; ::_thesis: for A, B being set holds f | (A \/ B) = (f | A) +* (f | B) let A, B be set ; ::_thesis: f | (A \/ B) = (f | A) +* (f | B) A1: (f | (A \/ B)) | B = f | ((A \/ B) /\ B) by RELAT_1:71 .= f | B by XBOOLE_1:21 ; A2: dom (f | (A \/ B)) c= A \/ B by RELAT_1:58; (f | (A \/ B)) | A = f | ((A \/ B) /\ A) by RELAT_1:71 .= f | A by XBOOLE_1:21 ; hence f | (A \/ B) = (f | A) +* (f | B) by A1, A2, Th70; ::_thesis: verum end; theorem :: FUNCT_4:79 for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ; theorem :: FUNCT_4:80 for i, j, k being set holds ((i,j) :-> k) . (i,j) = k by FUNCOP_1:71; theorem :: FUNCT_4:81 for a, b, c being set holds (a,a) --> (b,c) = a .--> c proof let a, b, c be set ; ::_thesis: (a,a) --> (b,c) = a .--> c dom (a .--> c) = {a} by FUNCOP_1:13 .= dom ({a} --> b) by FUNCOP_1:13 ; hence (a,a) --> (b,c) = a .--> c by Th19; ::_thesis: verum end; theorem :: FUNCT_4:82 for x, y being set holds x .--> y = {[x,y]} by ZFMISC_1:29; theorem :: FUNCT_4:83 for f being Function for a, b, c being set st a <> c holds (f +* (a .--> b)) . c = f . c proof let f be Function; ::_thesis: for a, b, c being set st a <> c holds (f +* (a .--> b)) . c = f . c let a, b, c be set ; ::_thesis: ( a <> c implies (f +* (a .--> b)) . c = f . c ) assume A1: a <> c ; ::_thesis: (f +* (a .--> b)) . c = f . c set g = a .--> b; not c in dom (a .--> b) by A1, TARSKI:def_1; hence (f +* (a .--> b)) . c = f . c by Th11; ::_thesis: verum end; theorem :: FUNCT_4:84 for f being Function for a, b, c, d being set st a <> b holds ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) proof let f be Function; ::_thesis: for a, b, c, d being set st a <> b holds ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) let a, b, c, d be set ; ::_thesis: ( a <> b implies ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) ) assume A1: a <> b ; ::_thesis: ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) set g = (a,b) --> (c,d); A2: dom ((a,b) --> (c,d)) = {a,b} by Th62; then a in dom ((a,b) --> (c,d)) by TARSKI:def_2; hence (f +* ((a,b) --> (c,d))) . a = ((a,b) --> (c,d)) . a by Th13 .= c by A1, Th63 ; ::_thesis: (f +* ((a,b) --> (c,d))) . b = d b in dom ((a,b) --> (c,d)) by A2, TARSKI:def_2; hence (f +* ((a,b) --> (c,d))) . b = ((a,b) --> (c,d)) . b by Th13 .= d by Th63 ; ::_thesis: verum end; theorem Th85: :: FUNCT_4:85 for a, b being set for f being Function st a in dom f & f . a = b holds a .--> b c= f proof let a, b be set ; ::_thesis: for f being Function st a in dom f & f . a = b holds a .--> b c= f let f be Function; ::_thesis: ( a in dom f & f . a = b implies a .--> b c= f ) assume ( a in dom f & f . a = b ) ; ::_thesis: a .--> b c= f then [a,b] in f by FUNCT_1:1; then {[a,b]} c= f by ZFMISC_1:31; hence a .--> b c= f by ZFMISC_1:29; ::_thesis: verum end; theorem :: FUNCT_4:86 for a, b, c, d being set for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds (a,c) --> (b,d) c= f proof let a, b, c, d be set ; ::_thesis: for f being Function st a in dom f & c in dom f & f . a = b & f . c = d holds (a,c) --> (b,d) c= f let f be Function; ::_thesis: ( a in dom f & c in dom f & f . a = b & f . c = d implies (a,c) --> (b,d) c= f ) assume that A1: a in dom f and A2: c in dom f and A3: ( f . a = b & f . c = d ) ; ::_thesis: (a,c) --> (b,d) c= f percases ( a <> c or a = c ) ; supposeA4: a <> c ; ::_thesis: (a,c) --> (b,d) c= f ( [a,b] in f & [c,d] in f ) by A1, A2, A3, FUNCT_1:1; then {[a,b],[c,d]} c= f by ZFMISC_1:32; hence (a,c) --> (b,d) c= f by A4, Th67; ::_thesis: verum end; suppose a = c ; ::_thesis: (a,c) --> (b,d) c= f hence (a,c) --> (b,d) c= f by A1, A3, Th85; ::_thesis: verum end; end; end; theorem Th87: :: FUNCT_4:87 for f, g, h being Function st f c= h & g c= h holds f +* g c= h proof let f, g, h be Function; ::_thesis: ( f c= h & g c= h implies f +* g c= h ) assume ( f c= h & g c= h ) ; ::_thesis: f +* g c= h then A1: f \/ g c= h by XBOOLE_1:8; f +* g c= f \/ g by Th29; hence f +* g c= h by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: FUNCT_4:88 for f, g being Function for A being set st A /\ (dom f) c= A /\ (dom g) holds (f +* (g | A)) | A = g | A proof let f, g be Function; ::_thesis: for A being set st A /\ (dom f) c= A /\ (dom g) holds (f +* (g | A)) | A = g | A let A be set ; ::_thesis: ( A /\ (dom f) c= A /\ (dom g) implies (f +* (g | A)) | A = g | A ) assume A1: A /\ (dom f) c= A /\ (dom g) ; ::_thesis: (f +* (g | A)) | A = g | A A2: ( dom (f | A) = A /\ (dom f) & dom (g | A) = A /\ (dom g) ) by RELAT_1:61; thus (f +* (g | A)) | A = (f | A) +* ((g | A) | A) by Th71 .= (f | A) +* (g | A) .= g | A by A1, A2, Th19 ; ::_thesis: verum end; theorem :: FUNCT_4:89 for f being Function for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n proof let f be Function; ::_thesis: for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n let a, b, n, m be set ; ::_thesis: ((f +* (a .--> b)) +* (m .--> n)) . m = n set mn = m .--> n; dom (m .--> n) = {m} by FUNCOP_1:13; then m in dom (m .--> n) by TARSKI:def_1; hence ((f +* (a .--> b)) +* (m .--> n)) . m = (m .--> n) . m by Th13 .= n by FUNCOP_1:72 ; ::_thesis: verum end; theorem :: FUNCT_4:90 for f being Function for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m proof let f be Function; ::_thesis: for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m let n, m be set ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m set mn = m .--> n; set nm = n .--> m; dom (m .--> n) = {m} by FUNCOP_1:13; then A1: m in dom (m .--> n) by TARSKI:def_1; percases ( n = m or n <> m ) ; supposeA2: n = m ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m hence ((f +* (n .--> m)) +* (m .--> n)) . n = (m .--> n) . m by A1, Th13 .= m by A2, FUNCOP_1:72 ; ::_thesis: verum end; supposeA3: n <> m ; ::_thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m dom (n .--> m) = {n} by FUNCOP_1:13; then A4: n in dom (n .--> m) by TARSKI:def_1; not n in dom (m .--> n) by A3, TARSKI:def_1; hence ((f +* (n .--> m)) +* (m .--> n)) . n = (f +* (n .--> m)) . n by Th11 .= (n .--> m) . n by A4, Th13 .= m by FUNCOP_1:72 ; ::_thesis: verum end; end; end; theorem :: FUNCT_4:91 for f being Function for a, b, n, m, x being set st x <> m & x <> a holds ((f +* (a .--> b)) +* (m .--> n)) . x = f . x proof let f be Function; ::_thesis: for a, b, n, m, x being set st x <> m & x <> a holds ((f +* (a .--> b)) +* (m .--> n)) . x = f . x let a, b, n, m, x be set ; ::_thesis: ( x <> m & x <> a implies ((f +* (a .--> b)) +* (m .--> n)) . x = f . x ) assume that A1: x <> m and A2: x <> a ; ::_thesis: ((f +* (a .--> b)) +* (m .--> n)) . x = f . x set mn = m .--> n; set nm = a .--> b; A3: not x in dom (a .--> b) by A2, TARSKI:def_1; not x in dom (m .--> n) by A1, TARSKI:def_1; hence ((f +* (a .--> b)) +* (m .--> n)) . x = (f +* (a .--> b)) . x by Th11 .= f . x by A3, Th11 ; ::_thesis: verum end; theorem :: FUNCT_4:92 for f, g being Function st f is one-to-one & g is one-to-one & rng f misses rng g holds f +* g is one-to-one proof let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g implies f +* g is one-to-one ) assume that A1: f is one-to-one and A2: g is one-to-one and A3: rng f misses rng g ; ::_thesis: f +* g is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (f +* g) or not x2 in dom (f +* g) or not (f +* g) . x1 = (f +* g) . x2 or x1 = x2 ) set fg = f +* g; assume that A4: x1 in dom (f +* g) and A5: x2 in dom (f +* g) and A6: (f +* g) . x1 = (f +* g) . x2 ; ::_thesis: x1 = x2 A7: ( x1 in dom f or x1 in dom g ) by A4, Th12; A8: ( x2 in dom f or x2 in dom g ) by A5, Th12; percases ( ( x1 in dom g & x2 in dom g ) or ( x1 in dom g & not x2 in dom g ) or ( not x1 in dom g & x2 in dom g ) or ( not x1 in dom g & not x2 in dom g ) ) ; supposeA9: ( x1 in dom g & x2 in dom g ) ; ::_thesis: x1 = x2 then ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = g . x2 ) by Th13; hence x1 = x2 by A2, A6, A9, FUNCT_1:def_4; ::_thesis: verum end; supposeA10: ( x1 in dom g & not x2 in dom g ) ; ::_thesis: x1 = x2 then x2 in dom f by A5, Th12; then A11: f . x2 in rng f by FUNCT_1:def_3; A12: g . x1 in rng g by A10, FUNCT_1:def_3; ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = f . x2 ) by A10, Th11, Th13; hence x1 = x2 by A3, A6, A12, A11, XBOOLE_0:3; ::_thesis: verum end; supposeA13: ( not x1 in dom g & x2 in dom g ) ; ::_thesis: x1 = x2 then x1 in dom f by A4, Th12; then A14: f . x1 in rng f by FUNCT_1:def_3; A15: g . x2 in rng g by A13, FUNCT_1:def_3; ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = g . x2 ) by A13, Th11, Th13; hence x1 = x2 by A3, A6, A15, A14, XBOOLE_0:3; ::_thesis: verum end; supposeA16: ( not x1 in dom g & not x2 in dom g ) ; ::_thesis: x1 = x2 then ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = f . x2 ) by Th11; hence x1 = x2 by A1, A6, A7, A8, A16, FUNCT_1:def_4; ::_thesis: verum end; end; end; registration let f, g be Function; reduce(f +* g) +* g to f +* g; reducibility (f +* g) +* g = f +* g proof thus (f +* g) +* g = f +* (g +* g) by Th14 .= f +* g ; ::_thesis: verum end; end; theorem :: FUNCT_4:93 for f, g being Function holds (f +* g) +* g = f +* g ; theorem :: FUNCT_4:94 for f, g, h being Function for D being set st (f +* g) | D = h | D holds (h +* g) | D = (f +* g) | D proof let f, g, h be Function; ::_thesis: for D being set st (f +* g) | D = h | D holds (h +* g) | D = (f +* g) | D let D be set ; ::_thesis: ( (f +* g) | D = h | D implies (h +* g) | D = (f +* g) | D ) assume A1: (f +* g) | D = h | D ; ::_thesis: (h +* g) | D = (f +* g) | D A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61 .= ((dom f) \/ (dom g)) /\ D by Def1 ; A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61 .= ((dom h) \/ (dom g)) /\ D by Def1 ; then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23 .= (((dom f) \/ (dom g)) /\ D) \/ ((dom g) /\ D) by A1, A2, RELAT_1:61 .= (((dom f) \/ (dom g)) \/ (dom g)) /\ D by XBOOLE_1:23 .= ((dom f) \/ ((dom g) \/ (dom g))) /\ D by XBOOLE_1:4 .= ((dom f) \/ (dom g)) /\ D ; now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+*_g)_|_D)_holds_ ((h_+*_g)_|_D)_._x_=_((f_+*_g)_|_D)_._x let x be set ; ::_thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b1 = ((f +* g) | D) . b1 ) assume A5: x in dom ((f +* g) | D) ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1 then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def_4; A7: x in D by A2, A5, XBOOLE_0:def_4; A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def_4; percases ( x in dom g or not x in dom g ) ; supposeA9: x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1 ((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47 .= g . x by A6, A9, Def1 ; hence ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; ::_thesis: verum end; suppose not x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1 hence ((h +* g) | D) . x = h . x by A8, Def1 .= ((f +* g) | D) . x by A1, A7, FUNCT_1:49 ; ::_thesis: verum end; end; end; hence (h +* g) | D = (f +* g) | D by A2, A4, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_4:95 for f, g, h being Function for D being set st f | D = h | D holds (h +* g) | D = (f +* g) | D proof let f, g, h be Function; ::_thesis: for D being set st f | D = h | D holds (h +* g) | D = (f +* g) | D let D be set ; ::_thesis: ( f | D = h | D implies (h +* g) | D = (f +* g) | D ) assume A1: f | D = h | D ; ::_thesis: (h +* g) | D = (f +* g) | D A2: dom ((f +* g) | D) = (dom (f +* g)) /\ D by RELAT_1:61 .= ((dom f) \/ (dom g)) /\ D by Def1 ; A3: dom ((h +* g) | D) = (dom (h +* g)) /\ D by RELAT_1:61 .= ((dom h) \/ (dom g)) /\ D by Def1 ; then A4: dom ((h +* g) | D) = ((dom h) /\ D) \/ ((dom g) /\ D) by XBOOLE_1:23 .= (dom (f | D)) \/ ((dom g) /\ D) by A1, RELAT_1:61 .= ((dom f) /\ D) \/ ((dom g) /\ D) by RELAT_1:61 .= ((dom f) \/ (dom g)) /\ D by XBOOLE_1:23 ; now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+*_g)_|_D)_holds_ ((h_+*_g)_|_D)_._x_=_((f_+*_g)_|_D)_._x let x be set ; ::_thesis: ( x in dom ((f +* g) | D) implies ((h +* g) | D) . b1 = ((f +* g) | D) . b1 ) assume A5: x in dom ((f +* g) | D) ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1 then A6: x in (dom f) \/ (dom g) by A2, XBOOLE_0:def_4; A7: x in D by A2, A5, XBOOLE_0:def_4; A8: ( x in (dom h) \/ (dom g) & ((h +* g) | D) . x = (h +* g) . x ) by A2, A3, A4, A5, FUNCT_1:47, XBOOLE_0:def_4; percases ( x in dom g or not x in dom g ) ; supposeA9: x in dom g ; ::_thesis: ((h +* g) | D) . b1 = ((f +* g) | D) . b1 ((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47 .= g . x by A6, A9, Def1 ; hence ((h +* g) | D) . x = ((f +* g) | D) . x by A8, A9, Def1; ::_thesis: verum end; supposeA10: not x in dom g ; ::_thesis: ((f +* g) | D) . b1 = ((h +* g) | D) . b1 then A11: ((h +* g) | D) . x = h . x by A8, Def1 .= (h | D) . x by A7, FUNCT_1:49 ; thus ((f +* g) | D) . x = (f +* g) . x by A5, FUNCT_1:47 .= f . x by A6, A10, Def1 .= ((h +* g) | D) . x by A1, A7, A11, FUNCT_1:49 ; ::_thesis: verum end; end; end; hence (h +* g) | D = (f +* g) | D by A2, A4, FUNCT_1:2; ::_thesis: verum end; theorem Th96: :: FUNCT_4:96 for x being set holds x .--> x = id {x} proof let x be set ; ::_thesis: x .--> x = id {x} for y, z being set holds ( [y,z] in x .--> x iff ( y in {x} & y = z ) ) proof let y, z be set ; ::_thesis: ( [y,z] in x .--> x iff ( y in {x} & y = z ) ) A1: x .--> x = {[x,x]} by ZFMISC_1:29; thus ( [y,z] in x .--> x implies ( y in {x} & y = z ) ) ::_thesis: ( y in {x} & y = z implies [y,z] in x .--> x ) proof assume [y,z] in x .--> x ; ::_thesis: ( y in {x} & y = z ) then A2: [y,z] = [x,x] by A1, TARSKI:def_1; then y = x by XTUPLE_0:1; hence ( y in {x} & y = z ) by A2, TARSKI:def_1, XTUPLE_0:1; ::_thesis: verum end; assume y in {x} ; ::_thesis: ( not y = z or [y,z] in x .--> x ) then y = x by TARSKI:def_1; hence ( not y = z or [y,z] in x .--> x ) by A1, TARSKI:def_1; ::_thesis: verum end; hence x .--> x = id {x} by RELAT_1:def_10; ::_thesis: verum end; theorem Th97: :: FUNCT_4:97 for f, g being Function st f c= g holds f +* g = g proof let f, g be Function; ::_thesis: ( f c= g implies f +* g = g ) assume A1: f c= g ; ::_thesis: f +* g = g then f tolerates g by PARTFUN1:54; hence f +* g = f \/ g by Th30 .= g by A1, XBOOLE_1:12 ; ::_thesis: verum end; theorem Th98: :: FUNCT_4:98 for f, g being Function st f c= g holds g +* f = g proof let f, g be Function; ::_thesis: ( f c= g implies g +* f = g ) assume A1: f c= g ; ::_thesis: g +* f = g then f tolerates g by PARTFUN1:54; hence g +* f = f \/ g by Th30 .= g by A1, XBOOLE_1:12 ; ::_thesis: verum end; begin definition let f be Function; let x, y be set ; funcf +~ (x,y) -> set equals :: FUNCT_4:def 5 f +* ((x .--> y) * f); coherence f +* ((x .--> y) * f) is set ; end; :: deftheorem defines +~ FUNCT_4:def_5_:_ for f being Function for x, y being set holds f +~ (x,y) = f +* ((x .--> y) * f); registration let f be Function; let x, y be set ; clusterf +~ (x,y) -> Relation-like Function-like ; coherence ( f +~ (x,y) is Relation-like & f +~ (x,y) is Function-like ) ; end; theorem Th99: :: FUNCT_4:99 for f being Function for x, y being set holds dom (f +~ (x,y)) = dom f proof let f be Function; ::_thesis: for x, y being set holds dom (f +~ (x,y)) = dom f let x, y be set ; ::_thesis: dom (f +~ (x,y)) = dom f thus dom (f +~ (x,y)) = (dom f) \/ (dom ((x .--> y) * f)) by Def1 .= dom f by RELAT_1:25, XBOOLE_1:12 ; ::_thesis: verum end; theorem Th100: :: FUNCT_4:100 for f being Function for x, y being set st x <> y holds not x in rng (f +~ (x,y)) proof let f be Function; ::_thesis: for x, y being set st x <> y holds not x in rng (f +~ (x,y)) let x, y be set ; ::_thesis: ( x <> y implies not x in rng (f +~ (x,y)) ) assume A1: x <> y ; ::_thesis: not x in rng (f +~ (x,y)) assume x in rng (f +~ (x,y)) ; ::_thesis: contradiction then consider z being set such that A2: z in dom (f +~ (x,y)) and A3: (f +~ (x,y)) . z = x by FUNCT_1:def_3; A4: z in dom f by A2, Th99; A5: now__::_thesis:_z_in_dom_((x_.-->_y)_*_f) assume A6: not z in dom ((x .--> y) * f) ; ::_thesis: contradiction then f . z = x by A3, Th11; then f . z in dom (x .--> y) by FUNCOP_1:74; hence contradiction by A4, A6, FUNCT_1:11; ::_thesis: verum end; (x .--> y) . (f . z) = ((x .--> y) * f) . z by A4, FUNCT_1:13 .= x by A3, A5, Th13 ; then f . z <> x by A1, FUNCOP_1:72; then not f . z in dom (x .--> y) by FUNCOP_1:75; hence contradiction by A5, FUNCT_1:11; ::_thesis: verum end; theorem :: FUNCT_4:101 for f being Function for x, y being set st x in rng f holds y in rng (f +~ (x,y)) proof let f be Function; ::_thesis: for x, y being set st x in rng f holds y in rng (f +~ (x,y)) let x, y be set ; ::_thesis: ( x in rng f implies y in rng (f +~ (x,y)) ) assume x in rng f ; ::_thesis: y in rng (f +~ (x,y)) then consider z being set such that A1: z in dom f and A2: f . z = x by FUNCT_1:def_3; A3: dom ((x .--> y) * f) c= dom (f +~ (x,y)) by Th10; x in dom (x .--> y) by FUNCOP_1:74; then A4: z in dom ((x .--> y) * f) by A1, A2, FUNCT_1:11; then (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th13 .= (x .--> y) . (f . z) by A1, FUNCT_1:13 .= y by A2, FUNCOP_1:72 ; hence y in rng (f +~ (x,y)) by A4, A3, FUNCT_1:3; ::_thesis: verum end; theorem Th102: :: FUNCT_4:102 for f being Function for x being set holds f +~ (x,x) = f proof let f be Function; ::_thesis: for x being set holds f +~ (x,x) = f let x be set ; ::_thesis: f +~ (x,x) = f thus f +~ (x,x) = f +* ((id {x}) * f) by Th96 .= f by Th98, RELAT_1:50 ; ::_thesis: verum end; theorem Th103: :: FUNCT_4:103 for f being Function for x, y being set st not x in rng f holds f +~ (x,y) = f proof let f be Function; ::_thesis: for x, y being set st not x in rng f holds f +~ (x,y) = f let x, y be set ; ::_thesis: ( not x in rng f implies f +~ (x,y) = f ) A1: dom (x .--> y) = {x} by FUNCOP_1:13; assume not x in rng f ; ::_thesis: f +~ (x,y) = f then dom (x .--> y) misses rng f by A1, ZFMISC_1:50; then (x .--> y) * f = {} by RELAT_1:44; hence f +~ (x,y) = f by Th21; ::_thesis: verum end; theorem :: FUNCT_4:104 for f being Function for x, y being set holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} proof let f be Function; ::_thesis: for x, y being set holds rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} let x, y be set ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} percases ( not x in rng f or ( x in rng f & x = y ) or x <> y ) ; supposeA1: not x in rng f ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} then f +~ (x,y) = f by Th103; then rng (f +~ (x,y)) = (rng f) \ {x} by A1, ZFMISC_1:57; hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by XBOOLE_1:7; ::_thesis: verum end; supposethat A2: x in rng f and A3: x = y ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} f +~ (x,y) = f by A3, Th102; hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A2, A3, ZFMISC_1:116; ::_thesis: verum end; supposeA4: x <> y ; ::_thesis: rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} not x in rng (f +~ (x,y)) by A4, Th100; then A5: (rng (f +~ (x,y))) \ {x} = rng (f +~ (x,y)) by ZFMISC_1:57; rng (x .--> y) = {y} by FUNCOP_1:8; then A6: (rng f) \/ (rng ((x .--> y) * f)) c= (rng f) \/ {y} by RELAT_1:26, XBOOLE_1:9; rng (f +~ (x,y)) c= (rng f) \/ (rng ((x .--> y) * f)) by Th17; then rng (f +~ (x,y)) c= (rng f) \/ {y} by A6, XBOOLE_1:1; then rng (f +~ (x,y)) c= ((rng f) \/ {y}) \ {x} by A5, XBOOLE_1:33; hence rng (f +~ (x,y)) c= ((rng f) \ {x}) \/ {y} by A4, ZFMISC_1:123; ::_thesis: verum end; end; end; theorem :: FUNCT_4:105 for z being set for f being Function for x, y being set st f . z <> x holds (f +~ (x,y)) . z = f . z proof let z be set ; ::_thesis: for f being Function for x, y being set st f . z <> x holds (f +~ (x,y)) . z = f . z let f be Function; ::_thesis: for x, y being set st f . z <> x holds (f +~ (x,y)) . z = f . z let x, y be set ; ::_thesis: ( f . z <> x implies (f +~ (x,y)) . z = f . z ) assume f . z <> x ; ::_thesis: (f +~ (x,y)) . z = f . z then not f . z in dom (x .--> y) by FUNCOP_1:75; then not z in dom ((x .--> y) * f) by FUNCT_1:11; hence (f +~ (x,y)) . z = f . z by Th11; ::_thesis: verum end; theorem :: FUNCT_4:106 for z being set for f being Function for x, y being set st z in dom f & f . z = x holds (f +~ (x,y)) . z = y proof let z be set ; ::_thesis: for f being Function for x, y being set st z in dom f & f . z = x holds (f +~ (x,y)) . z = y let f be Function; ::_thesis: for x, y being set st z in dom f & f . z = x holds (f +~ (x,y)) . z = y let x, y be set ; ::_thesis: ( z in dom f & f . z = x implies (f +~ (x,y)) . z = y ) assume that A1: z in dom f and A2: f . z = x ; ::_thesis: (f +~ (x,y)) . z = y f . z in dom (x .--> y) by A2, FUNCOP_1:74; then A3: z in dom ((x .--> y) * f) by A1, FUNCT_1:11; hence (f +~ (x,y)) . z = ((x .--> y) * f) . z by Th13 .= (x .--> y) . x by A2, A3, FUNCT_1:12 .= y by FUNCOP_1:72 ; ::_thesis: verum end; theorem :: FUNCT_4:107 for f being Function for x, y being set st not x in dom f holds f c= f +* (x .--> y) proof let f be Function; ::_thesis: for x, y being set st not x in dom f holds f c= f +* (x .--> y) let x, y be set ; ::_thesis: ( not x in dom f implies f c= f +* (x .--> y) ) assume not x in dom f ; ::_thesis: f c= f +* (x .--> y) then dom f misses {x} by ZFMISC_1:50; then dom f misses dom (x .--> y) by FUNCOP_1:13; hence f c= f +* (x .--> y) by Th32; ::_thesis: verum end; theorem :: FUNCT_4:108 for X, Y being set for f being PartFunc of X,Y for x, y being set st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y proof let X, Y be set ; ::_thesis: for f being PartFunc of X,Y for x, y being set st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y let f be PartFunc of X,Y; ::_thesis: for x, y being set st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y let x, y be set ; ::_thesis: ( x in X & y in Y implies f +* (x .--> y) is PartFunc of X,Y ) assume that A1: x in X and A2: y in Y ; ::_thesis: f +* (x .--> y) is PartFunc of X,Y A3: {x} c= X by A1, ZFMISC_1:31; {y} c= Y by A2, ZFMISC_1:31; then rng (x .--> y) c= Y by FUNCOP_1:8; then A4: (rng f) \/ (rng (x .--> y)) c= Y by XBOOLE_1:8; rng (f +* (x .--> y)) c= (rng f) \/ (rng (x .--> y)) by Th17; then A5: rng (f +* (x .--> y)) c= Y by A4, XBOOLE_1:1; dom (f +* (x .--> y)) = (dom f) \/ (dom (x .--> y)) by Def1 .= (dom f) \/ {x} by FUNCOP_1:13 ; hence f +* (x .--> y) is PartFunc of X,Y by A3, A5, RELSET_1:4, XBOOLE_1:8; ::_thesis: verum end; registration let f be Function; let g be non empty Function; clusterf +* g -> non empty ; coherence not f +* g is empty proof dom (f +* g) = (dom f) \/ (dom g) by Def1; hence not f +* g is empty ; ::_thesis: verum end; clusterg +* f -> non empty ; coherence not g +* f is empty proof dom (g +* f) = (dom g) \/ (dom f) by Def1; hence not g +* f is empty ; ::_thesis: verum end; end; registration let f, g be non-empty Function; clusterf +* g -> non-empty ; coherence f +* g is non-empty proof set h = f +* g; A1: dom (f +* g) = (dom f) \/ (dom g) by Def1; not {} in rng (f +* g) proof assume {} in rng (f +* g) ; ::_thesis: contradiction then consider x being set such that A2: ( x in dom (f +* g) & {} = (f +* g) . x ) by FUNCT_1:def_3; ( not x in dom g or x in dom g ) ; then ( ( {} = f . x & x in dom f ) or ( {} = g . x & x in dom g ) ) by A1, A2, Def1, XBOOLE_0:def_3; then ( {} in rng f or {} in rng g ) by FUNCT_1:def_3; hence contradiction by RELAT_1:def_9; ::_thesis: verum end; hence f +* g is non-empty by RELAT_1:def_9; ::_thesis: verum end; end; definition let X, Y be set ; let f, g be PartFunc of X,Y; :: original: +* redefine funcf +* g -> PartFunc of X,Y; coherence f +* g is PartFunc of X,Y proof A1: dom (f +* g) c= (dom f) \/ (dom g) by Def1; A2: dom (f +* g) c= X by A1, XBOOLE_1:1; A3: rng (f +* g) c= (rng f) \/ (rng g) by Th17; rng (f +* g) c= Y by A3, XBOOLE_1:1; then f +* g is Relation of X,Y by A2, RELSET_1:4; hence f +* g is PartFunc of X,Y ; ::_thesis: verum end; end; theorem :: FUNCT_4:109 for z, x, y being set holds dom ((x --> y) +* (x .--> z)) = succ x proof let z, x, y be set ; ::_thesis: dom ((x --> y) +* (x .--> z)) = succ x thus dom ((x --> y) +* (x .--> z)) = (dom (x --> y)) \/ (dom (x .--> z)) by Def1 .= x \/ (dom (x .--> z)) by FUNCOP_1:13 .= x \/ {x} by FUNCOP_1:13 .= succ x by ORDINAL1:def_1 ; ::_thesis: verum end; theorem :: FUNCT_4:110 for z, x, y being set holds dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = succ (succ x) proof let z, x, y be set ; ::_thesis: dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = succ (succ x) thus dom (((x --> y) +* (x .--> z)) +* ((succ x) .--> z)) = (dom ((x --> y) +* (x .--> z))) \/ (dom ((succ x) .--> z)) by Def1 .= ((dom (x --> y)) \/ (dom (x .--> z))) \/ (dom ((succ x) .--> z)) by Def1 .= (x \/ (dom (x .--> z))) \/ (dom ((succ x) .--> z)) by FUNCOP_1:13 .= (x \/ {x}) \/ (dom ((succ x) .--> z)) by FUNCOP_1:13 .= (x \/ {x}) \/ {(succ x)} by FUNCOP_1:13 .= (succ x) \/ {(succ x)} by ORDINAL1:def_1 .= succ (succ x) by ORDINAL1:def_1 ; ::_thesis: verum end; registration let f, g be Function-yielding Function; clusterf +* g -> Function-yielding ; coherence f +* g is Function-yielding proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (f +* g) or (f +* g) . x is set ) assume x in dom (f +* g) ; ::_thesis: (f +* g) . x is set then A1: x in (dom f) \/ (dom g) by Def1; percases ( x in dom g or ( x in dom f & not x in dom g ) ) by A1, XBOOLE_0:def_3; suppose x in dom g ; ::_thesis: (f +* g) . x is set then (f +* g) . x = g . x by Th13; hence (f +* g) . x is Function ; ::_thesis: verum end; suppose ( x in dom f & not x in dom g ) ; ::_thesis: (f +* g) . x is set then (f +* g) . x = f . x by Th11; hence (f +* g) . x is Function ; ::_thesis: verum end; end; end; end; registration let I be set ; let f, g be I -defined Function; clusterf +* g -> I -defined ; coherence f +* g is I -defined proof dom (f +* g) = (dom f) \/ (dom g) by Def1; then dom (f +* g) c= I ; hence f +* g is I -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let I be set ; let f be I -defined total Function; let g be I -defined Function; clusterf +* g -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = f +* g holds b1 is total proof dom f = I by PARTFUN1:def_2; then dom (f +* g) = I \/ (dom g) by Def1 .= I by XBOOLE_1:12 ; hence for b1 being I -defined Function st b1 = f +* g holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; clusterg +* f -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = g +* f holds b1 is total proof dom f = I by PARTFUN1:def_2; then dom (g +* f) = I \/ (dom g) by Def1 .= I by XBOOLE_1:12 ; hence for b1 being I -defined Function st b1 = g +* f holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let I be set ; let g, h be I -valued Function; clusterg +* h -> I -valued ; coherence g +* h is I -valued proof A1: rng (g +* h) c= (rng g) \/ (rng h) by Th17; rng (g +* h) c= I by A1, XBOOLE_1:1; hence g +* h is I -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let f be Function; let g, h be f -compatible Function; clusterg +* h -> f -compatible ; coherence g +* h is f -compatible proof let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (g +* h) or (g +* h) . x in f . x ) assume A1: x in dom (g +* h) ; ::_thesis: (g +* h) . x in f . x A2: dom (g +* h) = (dom g) \/ (dom h) by Def1; percases ( ( x in dom g & not x in dom h ) or x in dom h ) by A1, A2, XBOOLE_0:def_3; supposeA3: ( x in dom g & not x in dom h ) ; ::_thesis: (g +* h) . x in f . x then g . x in f . x by FUNCT_1:def_14; hence (g +* h) . x in f . x by A3, Th11; ::_thesis: verum end; supposeA4: x in dom h ; ::_thesis: (g +* h) . x in f . x then h . x in f . x by FUNCT_1:def_14; hence (g +* h) . x in f . x by A4, Th13; ::_thesis: verum end; end; end; end; theorem :: FUNCT_4:111 for f being Function for A being set holds (f | A) +* f = f by Th97, RELAT_1:59; theorem :: FUNCT_4:112 for x, y being set for R being Relation st dom R = {x} & rng R = {y} holds R = x .--> y proof let x, y be set ; ::_thesis: for R being Relation st dom R = {x} & rng R = {y} holds R = x .--> y let R be Relation; ::_thesis: ( dom R = {x} & rng R = {y} implies R = x .--> y ) assume that A1: dom R = {x} and A2: rng R = {y} ; ::_thesis: R = x .--> y set g = x .--> y; A3: x .--> y = {[x,y]} by ZFMISC_1:29; for a, b being set holds ( [a,b] in R iff [a,b] in x .--> y ) proof let a, b be set ; ::_thesis: ( [a,b] in R iff [a,b] in x .--> y ) hereby ::_thesis: ( [a,b] in x .--> y implies [a,b] in R ) assume A4: [a,b] in R ; ::_thesis: [a,b] in x .--> y then b in rng R by XTUPLE_0:def_13; then A5: b = y by A2, TARSKI:def_1; a in dom R by A4, XTUPLE_0:def_12; then a = x by A1, TARSKI:def_1; hence [a,b] in x .--> y by A3, A5, TARSKI:def_1; ::_thesis: verum end; assume [a,b] in x .--> y ; ::_thesis: [a,b] in R then A6: [a,b] = [x,y] by A3, TARSKI:def_1; then A7: b = y by XTUPLE_0:1; a = x by A6, XTUPLE_0:1; then a in dom R by A1, TARSKI:def_1; then consider z being set such that A8: [a,z] in R by XTUPLE_0:def_12; z in rng R by A8, XTUPLE_0:def_13; hence [a,b] in R by A2, A7, A8, TARSKI:def_1; ::_thesis: verum end; hence R = x .--> y by RELAT_1:def_2; ::_thesis: verum end; theorem :: FUNCT_4:113 for f being Function for x, y being set holds (f +* (x .--> y)) . x = y proof let f be Function; ::_thesis: for x, y being set holds (f +* (x .--> y)) . x = y let x, y be set ; ::_thesis: (f +* (x .--> y)) . x = y A1: x in {x} by TARSKI:def_1; then ( dom (x .--> y) = {x} & x in (dom f) \/ {x} ) by FUNCOP_1:13, XBOOLE_0:def_3; hence (f +* (x .--> y)) . x = (x .--> y) . x by A1, Def1 .= y by FUNCOP_1:72 ; ::_thesis: verum end; theorem :: FUNCT_4:114 for z1, z2 being set for f being Function for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2) proof let z1, z2 be set ; ::_thesis: for f being Function for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2) let f be Function; ::_thesis: for x being set holds (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2) let x be set ; ::_thesis: (f +* (x .--> z1)) +* (x .--> z2) = f +* (x .--> z2) A1: dom (x .--> z1) = {x} by FUNCOP_1:13 .= dom (x .--> z2) by FUNCOP_1:13 ; thus (f +* (x .--> z1)) +* (x .--> z2) = f +* ((x .--> z1) +* (x .--> z2)) by Th14 .= f +* (x .--> z2) by A1, Th19 ; ::_thesis: verum end; registration let A be non empty set ; let a, b be Element of A; let x, y be set ; cluster(a,b) --> (x,y) -> A -defined ; coherence (a,b) --> (x,y) is A -defined ; end; theorem :: FUNCT_4:115 for g, h, f being Function st dom g misses dom h holds ((f +* g) +* h) +* g = (f +* g) +* h proof let g, h, f be Function; ::_thesis: ( dom g misses dom h implies ((f +* g) +* h) +* g = (f +* g) +* h ) assume A1: dom g misses dom h ; ::_thesis: ((f +* g) +* h) +* g = (f +* g) +* h thus ((f +* g) +* h) +* g = (f +* (g +* h)) +* g by Th14 .= f +* ((g +* h) +* g) by Th14 .= f +* ((h +* g) +* g) by A1, Th35 .= f +* (h +* g) .= f +* (g +* h) by A1, Th35 .= (f +* g) +* h by Th14 ; ::_thesis: verum end; theorem :: FUNCT_4:116 for f, h, g being Function st dom f misses dom h & f c= g +* h holds f c= g proof let f, h, g be Function; ::_thesis: ( dom f misses dom h & f c= g +* h implies f c= g ) assume that A1: dom f misses dom h and A2: f c= g +* h ; ::_thesis: f c= g A3: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th71 .= (g | (dom f)) +* {} by A1, RELAT_1:66 .= g | (dom f) ; f | (dom f) = f ; then f c= g | (dom f) by A2, A3, RELAT_1:76; hence f c= g by RELAT_1:184; ::_thesis: verum end; theorem Th117: :: FUNCT_4:117 for f, h, g being Function st dom f misses dom h & f c= g holds f c= g +* h proof let f, h, g be Function; ::_thesis: ( dom f misses dom h & f c= g implies f c= g +* h ) assume that A1: dom f misses dom h and A2: f c= g ; ::_thesis: f c= g +* h A3: (g +* h) | (dom f) = (g | (dom f)) +* (h | (dom f)) by Th71 .= (g | (dom f)) +* {} by A1, RELAT_1:66 .= g | (dom f) ; f | (dom f) = f ; then f c= (g +* h) | (dom f) by A2, A3, RELAT_1:76; hence f c= g +* h by RELAT_1:184; ::_thesis: verum end; theorem :: FUNCT_4:118 for g, h, f being Function st dom g misses dom h holds (f +* g) +* h = (f +* h) +* g proof let g, h, f be Function; ::_thesis: ( dom g misses dom h implies (f +* g) +* h = (f +* h) +* g ) assume A1: dom g misses dom h ; ::_thesis: (f +* g) +* h = (f +* h) +* g thus (f +* g) +* h = f +* (g +* h) by Th14 .= f +* (h +* g) by A1, Th35 .= (f +* h) +* g by Th14 ; ::_thesis: verum end; theorem :: FUNCT_4:119 for f, g being Function st dom f misses dom g holds (f +* g) \ g = f proof let f, g be Function; ::_thesis: ( dom f misses dom g implies (f +* g) \ g = f ) assume A1: dom f misses dom g ; ::_thesis: (f +* g) \ g = f then A2: f misses g by RELAT_1:179; thus (f +* g) \ g = (f \/ g) \ g by A1, Th31 .= f by A2, XBOOLE_1:88 ; ::_thesis: verum end; theorem :: FUNCT_4:120 for f, g being Function st dom f misses dom g holds f \ g = f proof let f, g be Function; ::_thesis: ( dom f misses dom g implies f \ g = f ) assume dom f misses dom g ; ::_thesis: f \ g = f then f misses g by RELAT_1:179; hence f \ g = f by XBOOLE_1:83; ::_thesis: verum end; theorem :: FUNCT_4:121 for g, h, f being Function st dom g misses dom h holds (f \ g) +* h = (f +* h) \ g proof let g, h, f be Function; ::_thesis: ( dom g misses dom h implies (f \ g) +* h = (f +* h) \ g ) assume A1: dom g misses dom h ; ::_thesis: (f \ g) +* h = (f +* h) \ g A2: dom (f +* h) = (dom f) \/ (dom h) by Def1; A3: dom ((f \ g) +* h) = (dom (f \ g)) \/ (dom h) by Def1; A4: dom ((f \ g) +* h) = dom ((f +* h) \ g) proof thus dom ((f \ g) +* h) c= dom ((f +* h) \ g) :: according to XBOOLE_0:def_10 ::_thesis: dom ((f +* h) \ g) c= dom ((f \ g) +* h) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f \ g) +* h) or x in dom ((f +* h) \ g) ) assume A5: x in dom ((f \ g) +* h) ; ::_thesis: x in dom ((f +* h) \ g) percases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A5, XBOOLE_0:def_3; supposethat A6: x in dom (f \ g) and A7: not x in dom h ; ::_thesis: x in dom ((f +* h) \ g) consider y being set such that A8: [x,y] in f \ g by A6, XTUPLE_0:def_12; A9: x in dom f by A8, XTUPLE_0:def_12; then A10: x in dom (f +* h) by A2, XBOOLE_0:def_3; A11: not [x,y] in g by A8, XBOOLE_0:def_5; A12: (f +* h) . x = f . x by A7, Th11; f . x = y by A8, A9, FUNCT_1:def_2; then [x,y] in f +* h by A12, A10, FUNCT_1:def_2; then [x,y] in (f +* h) \ g by A11, XBOOLE_0:def_5; hence x in dom ((f +* h) \ g) by XTUPLE_0:def_12; ::_thesis: verum end; supposeA13: x in dom h ; ::_thesis: x in dom ((f +* h) \ g) then A14: not x in dom g by A1, XBOOLE_0:3; x in dom (f +* h) by A2, A13, XBOOLE_0:def_3; then A15: x in (dom (f +* h)) \ (dom g) by A14, XBOOLE_0:def_5; (dom (f +* h)) \ (dom g) c= dom ((f +* h) \ g) by RELAT_1:3; hence x in dom ((f +* h) \ g) by A15; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f +* h) \ g) or x in dom ((f \ g) +* h) ) assume x in dom ((f +* h) \ g) ; ::_thesis: x in dom ((f \ g) +* h) then consider y being set such that A16: [x,y] in (f +* h) \ g by XTUPLE_0:def_12; A17: x in dom (f +* h) by A16, XTUPLE_0:def_12; then A18: y = (f +* h) . x by A16, FUNCT_1:def_2; percases ( ( x in dom f & not x in dom h ) or x in dom h ) by A2, A17, XBOOLE_0:def_3; supposethat A19: x in dom f and A20: not x in dom h ; ::_thesis: x in dom ((f \ g) +* h) A21: not [x,y] in g by A16, XBOOLE_0:def_5; (f +* h) . x = f . x by A20, Th11; then [x,y] in f by A19, A18, FUNCT_1:def_2; then [x,y] in f \ g by A21, XBOOLE_0:def_5; then x in dom (f \ g) by XTUPLE_0:def_12; hence x in dom ((f \ g) +* h) by A3, XBOOLE_0:def_3; ::_thesis: verum end; suppose x in dom h ; ::_thesis: x in dom ((f \ g) +* h) hence x in dom ((f \ g) +* h) by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; now__::_thesis:_for_x_being_set_st_x_in_dom_((f_\_g)_+*_h)_holds_ ((f_\_g)_+*_h)_._x_=_((f_+*_h)_\_g)_._x let x be set ; ::_thesis: ( x in dom ((f \ g) +* h) implies ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1 ) assume A22: x in dom ((f \ g) +* h) ; ::_thesis: ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1 percases ( ( x in dom (f \ g) & not x in dom h ) or x in dom h ) by A3, A22, XBOOLE_0:def_3; supposethat A23: x in dom (f \ g) and A24: not x in dom h ; ::_thesis: ((f \ g) +* h) . b1 = ((f +* h) \ g) . b1 thus ((f \ g) +* h) . x = (f \ g) . x by A24, Th11 .= f . x by A23, GRFUNC_1:2 .= (f +* h) . x by A24, Th11 .= ((f +* h) \ g) . x by A4, A22, GRFUNC_1:2 ; ::_thesis: verum end; supposeA25: x in dom h ; ::_thesis: ((f +* h) \ g) . b1 = ((f \ g) +* h) . b1 then A26: not x in dom g by A1, XBOOLE_0:3; x in dom (f +* h) by A25, A2, XBOOLE_0:def_3; then x in (dom (f +* h)) \ (dom g) by A26, XBOOLE_0:def_5; hence ((f +* h) \ g) . x = (f +* h) . x by GRFUNC_1:32 .= h . x by A25, Th13 .= ((f \ g) +* h) . x by A25, Th13 ; ::_thesis: verum end; end; end; hence (f \ g) +* h = (f +* h) \ g by A4, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_4:122 for f1, f2, g1, g2 being Function st f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 holds f1 +* f2 c= g1 +* g2 proof let f1, f2, g1, g2 be Function; ::_thesis: ( f1 c= g1 & f2 c= g2 & dom f1 misses dom g2 implies f1 +* f2 c= g1 +* g2 ) assume that A1: f1 c= g1 and A2: f2 c= g2 and A3: dom f1 misses dom g2 ; ::_thesis: f1 +* f2 c= g1 +* g2 A4: f1 c= g1 +* g2 by A1, A3, Th117; g2 c= g1 +* g2 by Th25; then f2 c= g1 +* g2 by A2, XBOOLE_1:1; hence f1 +* f2 c= g1 +* g2 by A4, Th87; ::_thesis: verum end; theorem Th123: :: FUNCT_4:123 for f, g, h being Function st f c= g holds f +* h c= g +* h proof let f, g, h be Function; ::_thesis: ( f c= g implies f +* h c= g +* h ) assume A1: f c= g ; ::_thesis: f +* h c= g +* h now__::_thesis:_(_dom_(f_+*_h)_c=_dom_(g_+*_h)_&_(_for_x_being_set_st_x_in_dom_(f_+*_h)_holds_ (f_+*_h)_._x_=_(g_+*_h)_._x_)_) ( dom (f +* h) = (dom f) \/ (dom h) & dom (g +* h) = (dom g) \/ (dom h) ) by Def1; hence dom (f +* h) c= dom (g +* h) by A1, RELAT_1:11, XBOOLE_1:9; ::_thesis: for x being set st x in dom (f +* h) holds (f +* h) . b2 = (g +* h) . b2 let x be set ; ::_thesis: ( x in dom (f +* h) implies (f +* h) . b1 = (g +* h) . b1 ) assume x in dom (f +* h) ; ::_thesis: (f +* h) . b1 = (g +* h) . b1 then A2: ( x in dom f or x in dom h ) by Th12; percases ( x in dom h or not x in dom h ) ; supposeA3: x in dom h ; ::_thesis: (f +* h) . b1 = (g +* h) . b1 hence (f +* h) . x = h . x by Th13 .= (g +* h) . x by A3, Th13 ; ::_thesis: verum end; supposeA4: not x in dom h ; ::_thesis: (f +* h) . b1 = (g +* h) . b1 then ( (f +* h) . x = f . x & (g +* h) . x = g . x ) by Th11; hence (f +* h) . x = (g +* h) . x by A1, A2, A4, GRFUNC_1:2; ::_thesis: verum end; end; end; hence f +* h c= g +* h by GRFUNC_1:2; ::_thesis: verum end; theorem :: FUNCT_4:124 for f, g, h being Function st f c= g & dom f misses dom h holds f c= g +* h proof let f, g, h be Function; ::_thesis: ( f c= g & dom f misses dom h implies f c= g +* h ) assume f c= g ; ::_thesis: ( not dom f misses dom h or f c= g +* h ) then A1: f +* h c= g +* h by Th123; assume dom f misses dom h ; ::_thesis: f c= g +* h then f c= f +* h by Th32; hence f c= g +* h by A1, XBOOLE_1:1; ::_thesis: verum end; registration let x, y be set ; clusterx .--> y -> trivial ; coherence x .--> y is trivial proof x .--> y = {[x,y]} by ZFMISC_1:29; hence x .--> y is trivial ; ::_thesis: verum end; end; theorem :: FUNCT_4:125 for f, g, h being Function st f tolerates g & g tolerates h & h tolerates f holds f +* g tolerates h proof let f, g, h be Function; ::_thesis: ( f tolerates g & g tolerates h & h tolerates f implies f +* g tolerates h ) assume that A1: f tolerates g and A2: g tolerates h and A3: h tolerates f ; ::_thesis: f +* g tolerates h let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom (f +* g)) /\ (dom h) or (f +* g) . x = h . x ) assume A4: x in (dom (f +* g)) /\ (dom h) ; ::_thesis: (f +* g) . x = h . x then x in dom (f +* g) by XBOOLE_0:def_4; then A5: ( x in dom f or x in dom g ) by Th12; x in dom h by A4, XBOOLE_0:def_4; then ( ( x in (dom h) /\ (dom f) & (f +* g) . x = f . x ) or ( x in (dom g) /\ (dom h) & (f +* g) . x = g . x ) ) by A1, A5, Th13, Th15, XBOOLE_0:def_4; hence (f +* g) . x = h . x by A2, A3, PARTFUN1:def_4; ::_thesis: verum end;