:: FUNCT_6 semantic presentation begin theorem Th1: :: FUNCT_6:1 for f being Function holds product f c= Funcs ((dom f),(Union f)) proof let f be Function; ::_thesis: product f c= Funcs ((dom f),(Union f)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product f or x in Funcs ((dom f),(Union f)) ) assume x in product f ; ::_thesis: x in Funcs ((dom f),(Union f)) then consider g being Function such that A1: x = g and A2: dom g = dom f and A3: for x being set st x in dom f holds g . x in f . x by CARD_3:def_5; rng g c= Union f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Union f ) A4: Union f = union (rng f) by CARD_3:def_4; assume y in rng g ; ::_thesis: y in Union f then consider z being set such that A5: ( z in dom g & y = g . z ) by FUNCT_1:def_3; ( y in f . z & f . z in rng f ) by A2, A3, A5, FUNCT_1:def_3; hence y in Union f by A4, TARSKI:def_4; ::_thesis: verum end; hence x in Funcs ((dom f),(Union f)) by A1, A2, FUNCT_2:def_2; ::_thesis: verum end; begin theorem Th2: :: FUNCT_6:2 for x being set for f being Function st x in dom (~ f) holds ex y, z being set st x = [y,z] proof let x be set ; ::_thesis: for f being Function st x in dom (~ f) holds ex y, z being set st x = [y,z] let f be Function; ::_thesis: ( x in dom (~ f) implies ex y, z being set st x = [y,z] ) assume A1: x in dom (~ f) ; ::_thesis: ex y, z being set st x = [y,z] ex X, Y being set st dom (~ f) c= [:X,Y:] by FUNCT_4:44; hence ex y, z being set st x = [y,z] by A1, RELAT_1:def_1; ::_thesis: verum end; theorem Th3: :: FUNCT_6:3 for X, Y, z being set holds ~ ([:X,Y:] --> z) = [:Y,X:] --> z proof let X, Y, z be set ; ::_thesis: ~ ([:X,Y:] --> z) = [:Y,X:] --> z A1: dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13; then A2: dom (~ ([:X,Y:] --> z)) = [:Y,X:] by FUNCT_4:46; A3: now__::_thesis:_for_x_being_set_st_x_in_[:Y,X:]_holds_ (~_([:X,Y:]_-->_z))_._x_=_([:Y,X:]_-->_z)_._x let x be set ; ::_thesis: ( x in [:Y,X:] implies (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x ) assume A4: x in [:Y,X:] ; ::_thesis: (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x then consider y1, y2 being set such that A5: x = [y2,y1] and A6: [y1,y2] in [:X,Y:] by A1, A2, FUNCT_4:def_2; A7: ([:X,Y:] --> z) . (y1,y2) = z by A6, FUNCOP_1:7; ([:Y,X:] --> z) . (y2,y1) = z by A4, A5, FUNCOP_1:7; then (~ ([:X,Y:] --> z)) . (y2,y1) = ([:Y,X:] --> z) . (y2,y1) by A1, A6, A7, FUNCT_4:def_2; hence (~ ([:X,Y:] --> z)) . x = ([:Y,X:] --> z) . x by A5; ::_thesis: verum end; dom ([:Y,X:] --> z) = [:Y,X:] by FUNCOP_1:13; hence ~ ([:X,Y:] --> z) = [:Y,X:] --> z by A2, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th4: :: FUNCT_6:4 for f being Function holds ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) ) proof let f be Function; ::_thesis: ( curry f = curry' (~ f) & uncurry f = ~ (uncurry' f) ) A1: dom (curry (~ (~ f))) = proj1 (dom (~ (~ f))) by FUNCT_5:def_1; A2: dom (curry f) = proj1 (dom f) by FUNCT_5:def_1; A3: dom (curry (~ (~ f))) = dom (curry f) proof thus dom (curry (~ (~ f))) c= dom (curry f) :: according to XBOOLE_0:def_10 ::_thesis: dom (curry f) c= dom (curry (~ (~ f))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (curry (~ (~ f))) or x in dom (curry f) ) assume x in dom (curry (~ (~ f))) ; ::_thesis: x in dom (curry f) then consider y being set such that A4: [x,y] in dom (~ (~ f)) by A1, XTUPLE_0:def_12; [y,x] in dom (~ f) by A4, FUNCT_4:42; then [x,y] in dom f by FUNCT_4:42; hence x in dom (curry f) by A2, XTUPLE_0:def_12; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (curry f) or x in dom (curry (~ (~ f))) ) assume x in dom (curry f) ; ::_thesis: x in dom (curry (~ (~ f))) then consider y being set such that A5: [x,y] in dom f by A2, XTUPLE_0:def_12; [y,x] in dom (~ f) by A5, FUNCT_4:42; then [x,y] in dom (~ (~ f)) by FUNCT_4:42; hence x in dom (curry (~ (~ f))) by A1, XTUPLE_0:def_12; ::_thesis: verum end; A6: curry' (~ f) = curry (~ (~ f)) by FUNCT_5:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(curry_f)_holds_ (curry_f)_._x_=_(curry'_(~_f))_._x let x be set ; ::_thesis: ( x in dom (curry f) implies (curry f) . x = (curry' (~ f)) . x ) assume A7: x in dom (curry f) ; ::_thesis: (curry f) . x = (curry' (~ f)) . x then reconsider g = (curry f) . x, h = (curry' (~ f)) . x as Function by A6, A3, FUNCT_5:30; A8: dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A7, FUNCT_5:31; A9: dom h = proj1 ((dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:]) by A6, A3, A7, FUNCT_5:34; A10: dom g = dom h proof thus dom g c= dom h :: according to XBOOLE_0:def_10 ::_thesis: dom h c= dom g proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom g or a in dom h ) assume a in dom g ; ::_thesis: a in dom h then consider b being set such that A11: [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A8, XTUPLE_0:def_13; [b,a] in [:{x},(proj2 (dom f)):] by A11, XBOOLE_0:def_4; then A12: [a,b] in [:(proj2 (dom f)),{x}:] by ZFMISC_1:88; [b,a] in dom f by A11, XBOOLE_0:def_4; then A13: [a,b] in dom (~ f) by FUNCT_4:42; proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17; then [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A13, A12, XBOOLE_0:def_4; hence a in dom h by A9, XTUPLE_0:def_12; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom h or a in dom g ) assume a in dom h ; ::_thesis: a in dom g then consider b being set such that A14: [a,b] in (dom (~ f)) /\ [:(proj1 (dom (~ f))),{x}:] by A9, XTUPLE_0:def_12; [a,b] in [:(proj1 (dom (~ f))),{x}:] by A14, XBOOLE_0:def_4; then A15: [b,a] in [:{x},(proj1 (dom (~ f))):] by ZFMISC_1:88; [a,b] in dom (~ f) by A14, XBOOLE_0:def_4; then A16: [b,a] in dom f by FUNCT_4:42; proj2 (dom f) = proj1 (dom (~ f)) by FUNCT_5:17; then [b,a] in (dom f) /\ [:{x},(proj2 (dom f)):] by A16, A15, XBOOLE_0:def_4; hence a in dom g by A8, XTUPLE_0:def_13; ::_thesis: verum end; now__::_thesis:_for_a_being_set_st_a_in_dom_g_holds_ g_._a_=_h_._a let a be set ; ::_thesis: ( a in dom g implies g . a = h . a ) assume A17: a in dom g ; ::_thesis: g . a = h . a then A18: ( [x,a] in dom f & g . a = f . (x,a) ) by A7, FUNCT_5:31; h . a = (~ f) . (a,x) by A6, A3, A7, A10, A17, FUNCT_5:34; hence g . a = h . a by A18, FUNCT_4:def_2; ::_thesis: verum end; hence (curry f) . x = (curry' (~ f)) . x by A10, FUNCT_1:2; ::_thesis: verum end; hence curry f = curry' (~ f) by A6, A3, FUNCT_1:2; ::_thesis: uncurry f = ~ (uncurry' f) A19: dom (uncurry f) = dom (~ (~ (uncurry f))) proof thus dom (uncurry f) c= dom (~ (~ (uncurry f))) :: according to XBOOLE_0:def_10 ::_thesis: dom (~ (~ (uncurry f))) c= dom (uncurry f) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom (uncurry f) or a in dom (~ (~ (uncurry f))) ) assume A20: a in dom (uncurry f) ; ::_thesis: a in dom (~ (~ (uncurry f))) then consider x being set , g being Function, y being set such that A21: a = [x,y] and x in dom f and g = f . x and y in dom g by FUNCT_5:def_2; [y,x] in dom (~ (uncurry f)) by A20, A21, FUNCT_4:42; hence a in dom (~ (~ (uncurry f))) by A21, FUNCT_4:42; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom (~ (~ (uncurry f))) or a in dom (uncurry f) ) assume a in dom (~ (~ (uncurry f))) ; ::_thesis: a in dom (uncurry f) then ex x, y being set st ( a = [y,x] & [x,y] in dom (~ (uncurry f)) ) by FUNCT_4:def_2; hence a in dom (uncurry f) by FUNCT_4:42; ::_thesis: verum end; A22: now__::_thesis:_for_a_being_set_st_a_in_dom_(~_(~_(uncurry_f)))_holds_ (uncurry_f)_._a_=_(~_(~_(uncurry_f)))_._a let a be set ; ::_thesis: ( a in dom (~ (~ (uncurry f))) implies (uncurry f) . a = (~ (~ (uncurry f))) . a ) assume a in dom (~ (~ (uncurry f))) ; ::_thesis: (uncurry f) . a = (~ (~ (uncurry f))) . a then consider x, y being set such that A23: a = [y,x] and A24: [x,y] in dom (~ (uncurry f)) by FUNCT_4:def_2; ( (~ (uncurry f)) . (x,y) = (uncurry f) . (y,x) & (~ (uncurry f)) . (x,y) = (~ (~ (uncurry f))) . (y,x) ) by A24, FUNCT_4:43, FUNCT_4:def_2; hence (uncurry f) . a = (~ (~ (uncurry f))) . a by A23; ::_thesis: verum end; uncurry' f = ~ (uncurry f) by FUNCT_5:def_4; hence uncurry f = ~ (uncurry' f) by A19, A22, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_6:5 for X, Y, z being set st [:X,Y:] <> {} holds ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) ) proof let X, Y, z be set ; ::_thesis: ( [:X,Y:] <> {} implies ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) ) ) assume A1: [:X,Y:] <> {} ; ::_thesis: ( curry ([:X,Y:] --> z) = X --> (Y --> z) & curry' ([:X,Y:] --> z) = Y --> (X --> z) ) A2: dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13; A3: dom (X --> z) = X by FUNCOP_1:13; A4: now__::_thesis:_for_x_being_set_st_x_in_Y_holds_ (curry'_([:X,Y:]_-->_z))_._x_=_(Y_-->_(X_-->_z))_._x let x be set ; ::_thesis: ( x in Y implies (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x ) assume A5: x in Y ; ::_thesis: (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x then consider f being Function such that A6: ( (curry' ([:X,Y:] --> z)) . x = f & dom f = X ) and rng f c= rng ([:X,Y:] --> z) and A7: for y being set st y in X holds f . y = ([:X,Y:] --> z) . (y,x) by A1, A2, FUNCT_5:32; A8: now__::_thesis:_for_y_being_set_st_y_in_X_holds_ f_._y_=_(X_-->_z)_._y let y be set ; ::_thesis: ( y in X implies f . y = (X --> z) . y ) assume A9: y in X ; ::_thesis: f . y = (X --> z) . y then A10: f . y = ([:X,Y:] --> z) . (y,x) by A7; ( (X --> z) . y = z & [y,x] in [:X,Y:] ) by A5, A9, FUNCOP_1:7, ZFMISC_1:87; hence f . y = (X --> z) . y by A10, FUNCOP_1:7; ::_thesis: verum end; (Y --> (X --> z)) . x = X --> z by A5, FUNCOP_1:7; hence (curry' ([:X,Y:] --> z)) . x = (Y --> (X --> z)) . x by A3, A6, A8, FUNCT_1:2; ::_thesis: verum end; A11: dom (Y --> z) = Y by FUNCOP_1:13; A12: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (curry_([:X,Y:]_-->_z))_._x_=_(X_-->_(Y_-->_z))_._x let x be set ; ::_thesis: ( x in X implies (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x ) assume A13: x in X ; ::_thesis: (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x then consider f being Function such that A14: ( (curry ([:X,Y:] --> z)) . x = f & dom f = Y ) and rng f c= rng ([:X,Y:] --> z) and A15: for y being set st y in Y holds f . y = ([:X,Y:] --> z) . (x,y) by A1, A2, FUNCT_5:29; A16: now__::_thesis:_for_y_being_set_st_y_in_Y_holds_ f_._y_=_(Y_-->_z)_._y let y be set ; ::_thesis: ( y in Y implies f . y = (Y --> z) . y ) assume A17: y in Y ; ::_thesis: f . y = (Y --> z) . y then A18: f . y = ([:X,Y:] --> z) . (x,y) by A15; ( (Y --> z) . y = z & [x,y] in [:X,Y:] ) by A13, A17, FUNCOP_1:7, ZFMISC_1:87; hence f . y = (Y --> z) . y by A18, FUNCOP_1:7; ::_thesis: verum end; (X --> (Y --> z)) . x = Y --> z by A13, FUNCOP_1:7; hence (curry ([:X,Y:] --> z)) . x = (X --> (Y --> z)) . x by A11, A14, A16, FUNCT_1:2; ::_thesis: verum end; ( dom (X --> (Y --> z)) = X & dom (curry ([:X,Y:] --> z)) = X ) by A1, A2, FUNCOP_1:13, FUNCT_5:24; hence curry ([:X,Y:] --> z) = X --> (Y --> z) by A12, FUNCT_1:2; ::_thesis: curry' ([:X,Y:] --> z) = Y --> (X --> z) ( dom (Y --> (X --> z)) = Y & dom (curry' ([:X,Y:] --> z)) = Y ) by A1, A2, FUNCOP_1:13, FUNCT_5:24; hence curry' ([:X,Y:] --> z) = Y --> (X --> z) by A4, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_6:6 for X, Y, z being set holds ( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z ) proof let X, Y, z be set ; ::_thesis: ( uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z)) = [:Y,X:] --> z ) A1: dom (X --> (Y --> z)) = X by FUNCOP_1:13; A2: dom (Y --> z) = Y by FUNCOP_1:13; rng (Y --> z) c= {z} by FUNCOP_1:13; then Y --> z in Funcs (Y,{z}) by A2, FUNCT_2:def_2; then ( rng (X --> (Y --> z)) c= {(Y --> z)} & {(Y --> z)} c= Funcs (Y,{z}) ) by FUNCOP_1:13, ZFMISC_1:31; then rng (X --> (Y --> z)) c= Funcs (Y,{z}) by XBOOLE_1:1; then A3: dom (uncurry (X --> (Y --> z))) = [:X,Y:] by A1, FUNCT_5:26; A4: now__::_thesis:_for_x_being_set_st_x_in_[:X,Y:]_holds_ (uncurry_(X_-->_(Y_-->_z)))_._x_=_([:X,Y:]_-->_z)_._x let x be set ; ::_thesis: ( x in [:X,Y:] implies (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x ) assume A5: x in [:X,Y:] ; ::_thesis: (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x then consider y1 being set , g being Function, y2 being set such that A6: x = [y1,y2] and A7: ( y1 in X & g = (X --> (Y --> z)) . y1 ) and A8: y2 in dom g by A1, A3, FUNCT_5:def_2; A9: g = Y --> z by A7, FUNCOP_1:7; then (Y --> z) . y2 = z by A2, A8, FUNCOP_1:7; then z = (uncurry (X --> (Y --> z))) . (y1,y2) by A1, A7, A8, A9, FUNCT_5:38; hence (uncurry (X --> (Y --> z))) . x = ([:X,Y:] --> z) . x by A5, A6, FUNCOP_1:7; ::_thesis: verum end; dom ([:X,Y:] --> z) = [:X,Y:] by FUNCOP_1:13; hence uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A3, A4, FUNCT_1:2; ::_thesis: uncurry' (X --> (Y --> z)) = [:Y,X:] --> z then ~ (uncurry (X --> (Y --> z))) = [:Y,X:] --> z by Th3; hence uncurry' (X --> (Y --> z)) = [:Y,X:] --> z by FUNCT_5:def_4; ::_thesis: verum end; theorem Th7: :: FUNCT_6:7 for x being set for f, g being Function st x in dom f & g = f . x holds ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) proof let x be set ; ::_thesis: for f, g being Function st x in dom f & g = f . x holds ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) let f, g be Function; ::_thesis: ( x in dom f & g = f . x implies ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) ) assume A1: ( x in dom f & g = f . x ) ; ::_thesis: ( rng g c= rng (uncurry f) & rng g c= rng (uncurry' f) ) thus rng g c= rng (uncurry f) ::_thesis: rng g c= rng (uncurry' f) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (uncurry f) ) assume y in rng g ; ::_thesis: y in rng (uncurry f) then ex z being set st ( z in dom g & y = g . z ) by FUNCT_1:def_3; hence y in rng (uncurry f) by A1, FUNCT_5:38; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng (uncurry' f) ) assume y in rng g ; ::_thesis: y in rng (uncurry' f) then ex z being set st ( z in dom g & y = g . z ) by FUNCT_1:def_3; hence y in rng (uncurry' f) by A1, FUNCT_5:39; ::_thesis: verum end; theorem Th8: :: FUNCT_6:8 for X being set for f being Function holds ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f ) proof let X be set ; ::_thesis: for f being Function holds ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f ) let f be Function; ::_thesis: ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f ) f in Funcs ((dom f),(rng f)) by FUNCT_2:def_2; then ( rng (X --> f) c= {f} & {f} c= Funcs ((dom f),(rng f)) ) by FUNCOP_1:13, ZFMISC_1:31; then ( dom (X --> f) = X & rng (X --> f) c= Funcs ((dom f),(rng f)) ) by FUNCOP_1:13, XBOOLE_1:1; hence ( dom (uncurry (X --> f)) = [:X,(dom f):] & rng (uncurry (X --> f)) c= rng f & dom (uncurry' (X --> f)) = [:(dom f),X:] & rng (uncurry' (X --> f)) c= rng f ) by FUNCT_5:26, FUNCT_5:41; ::_thesis: verum end; theorem :: FUNCT_6:9 for X being set for f being Function st X <> {} holds ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) proof let X be set ; ::_thesis: for f being Function st X <> {} holds ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) let f be Function; ::_thesis: ( X <> {} implies ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) ) set x = the Element of X; assume A1: X <> {} ; ::_thesis: ( rng (uncurry (X --> f)) = rng f & rng (uncurry' (X --> f)) = rng f ) then ( dom (X --> f) = X & (X --> f) . the Element of X = f ) by FUNCOP_1:7, FUNCOP_1:13; hence ( rng (uncurry (X --> f)) c= rng f & rng f c= rng (uncurry (X --> f)) & rng (uncurry' (X --> f)) c= rng f & rng f c= rng (uncurry' (X --> f)) ) by A1, Th7, Th8; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th10: :: FUNCT_6:10 for X, Y, Z being set for f being Function st [:X,Y:] <> {} & f in Funcs ([:X,Y:],Z) holds ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) proof let X, Y, Z be set ; ::_thesis: for f being Function st [:X,Y:] <> {} & f in Funcs ([:X,Y:],Z) holds ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) let f be Function; ::_thesis: ( [:X,Y:] <> {} & f in Funcs ([:X,Y:],Z) implies ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) ) assume A1: [:X,Y:] <> {} ; ::_thesis: ( not f in Funcs ([:X,Y:],Z) or ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) ) assume f in Funcs ([:X,Y:],Z) ; ::_thesis: ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) then A2: ex g being Function st ( f = g & dom g = [:X,Y:] & rng g c= Z ) by FUNCT_2:def_2; then ( rng (curry f) c= Funcs (Y,(rng f)) & Funcs (Y,(rng f)) c= Funcs (Y,Z) ) by FUNCT_5:35, FUNCT_5:56; then A3: rng (curry f) c= Funcs (Y,Z) by XBOOLE_1:1; ( rng (curry' f) c= Funcs (X,(rng f)) & Funcs (X,(rng f)) c= Funcs (X,Z) ) by A2, FUNCT_5:35, FUNCT_5:56; then A4: rng (curry' f) c= Funcs (X,Z) by XBOOLE_1:1; ( dom (curry f) = X & dom (curry' f) = Y ) by A1, A2, FUNCT_5:24; hence ( curry f in Funcs (X,(Funcs (Y,Z))) & curry' f in Funcs (Y,(Funcs (X,Z))) ) by A3, A4, FUNCT_2:def_2; ::_thesis: verum end; theorem Th11: :: FUNCT_6:11 for X, Y, Z being set for f being Function st f in Funcs (X,(Funcs (Y,Z))) holds ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) proof let X, Y, Z be set ; ::_thesis: for f being Function st f in Funcs (X,(Funcs (Y,Z))) holds ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) let f be Function; ::_thesis: ( f in Funcs (X,(Funcs (Y,Z))) implies ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) ) assume f in Funcs (X,(Funcs (Y,Z))) ; ::_thesis: ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) then A1: ex g being Function st ( f = g & dom g = X & rng g c= Funcs (Y,Z) ) by FUNCT_2:def_2; then A2: ( dom (uncurry f) = [:X,Y:] & dom (uncurry' f) = [:Y,X:] ) by FUNCT_5:26; ( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:41; hence ( uncurry f in Funcs ([:X,Y:],Z) & uncurry' f in Funcs ([:Y,X:],Z) ) by A2, FUNCT_2:def_2; ::_thesis: verum end; theorem :: FUNCT_6:12 for X, Y, Z, V1, V2 being set for f being Function st ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] holds f in Funcs ([:X,Y:],Z) proof let X, Y, Z, V1, V2 be set ; ::_thesis: for f being Function st ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] holds f in Funcs ([:X,Y:],Z) let f be Function; ::_thesis: ( ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) & dom f c= [:V1,V2:] implies f in Funcs ([:X,Y:],Z) ) assume ( curry f in Funcs (X,(Funcs (Y,Z))) or curry' f in Funcs (Y,(Funcs (X,Z))) ) ; ::_thesis: ( not dom f c= [:V1,V2:] or f in Funcs ([:X,Y:],Z) ) then A1: ( uncurry (curry f) in Funcs ([:X,Y:],Z) or uncurry' (curry' f) in Funcs ([:X,Y:],Z) ) by Th11; assume dom f c= [:V1,V2:] ; ::_thesis: f in Funcs ([:X,Y:],Z) hence f in Funcs ([:X,Y:],Z) by A1, FUNCT_5:50; ::_thesis: verum end; theorem :: FUNCT_6:13 for X, Y, Z, V1, V2 being set for f being Function st ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f = X holds f in Funcs (X,(Funcs (Y,Z))) proof let X, Y, Z, V1, V2 be set ; ::_thesis: for f being Function st ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f = X holds f in Funcs (X,(Funcs (Y,Z))) let f be Function; ::_thesis: ( ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f = X implies f in Funcs (X,(Funcs (Y,Z))) ) assume that A1: ( uncurry f in Funcs ([:X,Y:],Z) or uncurry' f in Funcs ([:Y,X:],Z) ) and A2: rng f c= PFuncs (V1,V2) and A3: dom f = X ; ::_thesis: f in Funcs (X,(Funcs (Y,Z))) A4: uncurry' f = ~ (uncurry f) by FUNCT_5:def_4; A5: ( ex g being Function st ( uncurry f = g & dom g = [:X,Y:] & rng g c= Z ) or ex g being Function st ( uncurry' f = g & dom g = [:Y,X:] & rng g c= Z ) ) by A1, FUNCT_2:def_2; then A6: dom (uncurry' f) = [:Y,X:] by A4, FUNCT_4:46; rng f c= Funcs (Y,Z) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs (Y,Z) ) assume A7: y in rng f ; ::_thesis: y in Funcs (Y,Z) then consider x being set such that A8: x in dom f and A9: y = f . x by FUNCT_1:def_3; ex g being Function st ( y = g & dom g c= V1 & rng g c= V2 ) by A2, A7, PARTFUN1:def_3; then reconsider h = y as Function ; A10: dom h = Y proof thus dom h c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= dom h proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom h or z in Y ) assume z in dom h ; ::_thesis: z in Y then [z,x] in dom (uncurry' f) by A8, A9, FUNCT_5:39; hence z in Y by A6, ZFMISC_1:87; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y or z in dom h ) assume z in Y ; ::_thesis: z in dom h then [z,x] in [:Y,X:] by A3, A8, ZFMISC_1:87; then [x,z] in dom (uncurry f) by A4, A6, FUNCT_4:42; then consider y1 being set , f1 being Function, y2 being set such that A11: [x,z] = [y1,y2] and y1 in dom f and A12: ( f1 = f . y1 & y2 in dom f1 ) by FUNCT_5:def_2; x = y1 by A11, XTUPLE_0:1; hence z in dom h by A9, A11, A12, XTUPLE_0:1; ::_thesis: verum end; rng h c= Z proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Z ) assume z in rng h ; ::_thesis: z in Z then ex y1 being set st ( y1 in dom h & z = h . y1 ) by FUNCT_1:def_3; then ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A8, A9, FUNCT_5:38, FUNCT_5:39; hence z in Z by A5; ::_thesis: verum end; hence y in Funcs (Y,Z) by A10, FUNCT_2:def_2; ::_thesis: verum end; hence f in Funcs (X,(Funcs (Y,Z))) by A3, FUNCT_2:def_2; ::_thesis: verum end; theorem :: FUNCT_6:14 for X, Y, Z being set for f being Function st f in PFuncs ([:X,Y:],Z) holds ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) proof let X, Y, Z be set ; ::_thesis: for f being Function st f in PFuncs ([:X,Y:],Z) holds ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) let f be Function; ::_thesis: ( f in PFuncs ([:X,Y:],Z) implies ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) ) assume f in PFuncs ([:X,Y:],Z) ; ::_thesis: ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) then A1: ex g being Function st ( f = g & dom g c= [:X,Y:] & rng g c= Z ) by PARTFUN1:def_3; then ( proj1 [:X,Y:] c= X & proj1 (dom f) c= proj1 [:X,Y:] ) by FUNCT_5:10, XTUPLE_0:8; then proj1 (dom f) c= X by XBOOLE_1:1; then A2: PFuncs ((proj1 (dom f)),(rng f)) c= PFuncs (X,Z) by A1, PARTFUN1:50; ( proj2 [:X,Y:] c= Y & proj2 (dom f) c= proj2 [:X,Y:] ) by A1, FUNCT_5:10, XTUPLE_0:9; then proj2 (dom f) c= Y by XBOOLE_1:1; then ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & PFuncs ((proj2 (dom f)),(rng f)) c= PFuncs (Y,Z) ) by A1, FUNCT_5:36, PARTFUN1:50; then A3: rng (curry f) c= PFuncs (Y,Z) by XBOOLE_1:1; rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) by FUNCT_5:36; then A4: rng (curry' f) c= PFuncs (X,Z) by A2, XBOOLE_1:1; ( dom (curry f) c= X & dom (curry' f) c= Y ) by A1, FUNCT_5:25; hence ( curry f in PFuncs (X,(PFuncs (Y,Z))) & curry' f in PFuncs (Y,(PFuncs (X,Z))) ) by A3, A4, PARTFUN1:def_3; ::_thesis: verum end; theorem Th15: :: FUNCT_6:15 for X, Y, Z being set for f being Function st f in PFuncs (X,(PFuncs (Y,Z))) holds ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) proof let X, Y, Z be set ; ::_thesis: for f being Function st f in PFuncs (X,(PFuncs (Y,Z))) holds ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) let f be Function; ::_thesis: ( f in PFuncs (X,(PFuncs (Y,Z))) implies ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) ) assume f in PFuncs (X,(PFuncs (Y,Z))) ; ::_thesis: ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) then A1: ex g being Function st ( f = g & dom g c= X & rng g c= PFuncs (Y,Z) ) by PARTFUN1:def_3; then ( dom (uncurry f) c= [:(dom f),Y:] & [:(dom f),Y:] c= [:X,Y:] ) by FUNCT_5:37, ZFMISC_1:96; then A2: dom (uncurry f) c= [:X,Y:] by XBOOLE_1:1; ( dom (uncurry' f) c= [:Y,(dom f):] & [:Y,(dom f):] c= [:Y,X:] ) by A1, FUNCT_5:37, ZFMISC_1:96; then A3: dom (uncurry' f) c= [:Y,X:] by XBOOLE_1:1; ( rng (uncurry f) c= Z & rng (uncurry' f) c= Z ) by A1, FUNCT_5:40; hence ( uncurry f in PFuncs ([:X,Y:],Z) & uncurry' f in PFuncs ([:Y,X:],Z) ) by A2, A3, PARTFUN1:def_3; ::_thesis: verum end; theorem :: FUNCT_6:16 for X, Y, Z, V1, V2 being set for f being Function st ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) & dom f c= [:V1,V2:] holds f in PFuncs ([:X,Y:],Z) proof let X, Y, Z, V1, V2 be set ; ::_thesis: for f being Function st ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) & dom f c= [:V1,V2:] holds f in PFuncs ([:X,Y:],Z) let f be Function; ::_thesis: ( ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) & dom f c= [:V1,V2:] implies f in PFuncs ([:X,Y:],Z) ) assume ( curry f in PFuncs (X,(PFuncs (Y,Z))) or curry' f in PFuncs (Y,(PFuncs (X,Z))) ) ; ::_thesis: ( not dom f c= [:V1,V2:] or f in PFuncs ([:X,Y:],Z) ) then A1: ( uncurry (curry f) in PFuncs ([:X,Y:],Z) or uncurry' (curry' f) in PFuncs ([:X,Y:],Z) ) by Th15; assume dom f c= [:V1,V2:] ; ::_thesis: f in PFuncs ([:X,Y:],Z) hence f in PFuncs ([:X,Y:],Z) by A1, FUNCT_5:50; ::_thesis: verum end; theorem :: FUNCT_6:17 for X, Y, Z, V1, V2 being set for f being Function st ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f c= X holds f in PFuncs (X,(PFuncs (Y,Z))) proof let X, Y, Z, V1, V2 be set ; ::_thesis: for f being Function st ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f c= X holds f in PFuncs (X,(PFuncs (Y,Z))) let f be Function; ::_thesis: ( ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) & rng f c= PFuncs (V1,V2) & dom f c= X implies f in PFuncs (X,(PFuncs (Y,Z))) ) assume that A1: ( uncurry f in PFuncs ([:X,Y:],Z) or uncurry' f in PFuncs ([:Y,X:],Z) ) and A2: rng f c= PFuncs (V1,V2) and A3: dom f c= X ; ::_thesis: f in PFuncs (X,(PFuncs (Y,Z))) A4: ( ex g being Function st ( uncurry f = g & dom g c= [:X,Y:] & rng g c= Z ) or ex g being Function st ( uncurry' f = g & dom g c= [:Y,X:] & rng g c= Z ) ) by A1, PARTFUN1:def_3; uncurry' f = ~ (uncurry f) by FUNCT_5:def_4; then A5: dom (uncurry' f) c= [:Y,X:] by A4, FUNCT_4:45; rng f c= PFuncs (Y,Z) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in PFuncs (Y,Z) ) assume A6: y in rng f ; ::_thesis: y in PFuncs (Y,Z) then consider x being set such that A7: ( x in dom f & y = f . x ) by FUNCT_1:def_3; ex g being Function st ( y = g & dom g c= V1 & rng g c= V2 ) by A2, A6, PARTFUN1:def_3; then reconsider h = y as Function ; A8: rng h c= Z proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Z ) assume z in rng h ; ::_thesis: z in Z then ex y1 being set st ( y1 in dom h & z = h . y1 ) by FUNCT_1:def_3; then ( z in rng (uncurry f) & z in rng (uncurry' f) ) by A7, FUNCT_5:38, FUNCT_5:39; hence z in Z by A4; ::_thesis: verum end; dom h c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom h or z in Y ) assume z in dom h ; ::_thesis: z in Y then [z,x] in dom (uncurry' f) by A7, FUNCT_5:39; hence z in Y by A5, ZFMISC_1:87; ::_thesis: verum end; hence y in PFuncs (Y,Z) by A8, PARTFUN1:def_3; ::_thesis: verum end; hence f in PFuncs (X,(PFuncs (Y,Z))) by A3, PARTFUN1:def_3; ::_thesis: verum end; begin definition let X be set ; func SubFuncs X -> set means :Def1: :: FUNCT_6:def 1 for x being set holds ( x in it iff ( x in X & x is Function ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in X & x is Function ) ) proof defpred S1[ set ] means \$1 is Function; ex Y being set st for x being set holds ( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); hence ex b1 being set st for x being set holds ( x in b1 iff ( x in X & x is Function ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in X & x is Function ) ) ) & ( for x being set holds ( x in b2 iff ( x in X & x is Function ) ) ) holds b1 = b2 proof defpred S1[ set ] means ( \$1 in X & \$1 is Function ); let X1, X2 be set ; ::_thesis: ( ( for x being set holds ( x in X1 iff ( x in X & x is Function ) ) ) & ( for x being set holds ( x in X2 iff ( x in X & x is Function ) ) ) implies X1 = X2 ) assume that A1: for x being set holds ( x in X1 iff S1[x] ) and A2: for x being set holds ( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2 thus X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum end; end; :: deftheorem Def1 defines SubFuncs FUNCT_6:def_1_:_ for X being set for b2 being set holds ( b2 = SubFuncs X iff for x being set holds ( x in b2 iff ( x in X & x is Function ) ) ); theorem Th18: :: FUNCT_6:18 for X being set holds SubFuncs X c= X proof let X be set ; ::_thesis: SubFuncs X c= X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubFuncs X or x in X ) thus ( not x in SubFuncs X or x in X ) by Def1; ::_thesis: verum end; theorem Th19: :: FUNCT_6:19 for x being set for f being Function holds ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) proof let x be set ; ::_thesis: for f being Function holds ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) let f be Function; ::_thesis: ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) ( ( f . x in rng f & f . x is Function ) iff f . x in SubFuncs (rng f) ) by Def1; hence ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) by FUNCT_1:def_3, FUNCT_1:def_7; ::_thesis: verum end; Lm1: for X being set st ( for x being set st x in X holds x is Function ) holds SubFuncs X = X proof let X be set ; ::_thesis: ( ( for x being set st x in X holds x is Function ) implies SubFuncs X = X ) assume for x being set st x in X holds x is Function ; ::_thesis: SubFuncs X = X then for x being set holds ( x in X iff ( x in X & x is Function ) ) ; hence SubFuncs X = X by Def1; ::_thesis: verum end; theorem :: FUNCT_6:20 for f, g, h being Function holds ( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} ) proof let f, g, h be Function; ::_thesis: ( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} ) thus SubFuncs {} = {} by Th18, XBOOLE_1:3; ::_thesis: ( SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} ) for x being set st x in {f} holds x is Function ; hence SubFuncs {f} = {f} by Lm1; ::_thesis: ( SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} ) for x being set st x in {f,g} holds x is Function ; hence SubFuncs {f,g} = {f,g} by Lm1; ::_thesis: SubFuncs {f,g,h} = {f,g,h} for x being set st x in {f,g,h} holds x is Function by ENUMSET1:def_1; hence SubFuncs {f,g,h} = {f,g,h} by Lm1; ::_thesis: verum end; theorem :: FUNCT_6:21 for Y, X being set st Y c= SubFuncs X holds SubFuncs Y = Y proof let Y, X be set ; ::_thesis: ( Y c= SubFuncs X implies SubFuncs Y = Y ) assume Y c= SubFuncs X ; ::_thesis: SubFuncs Y = Y then for x being set st x in Y holds x is Function by Def1; hence SubFuncs Y = Y by Lm1; ::_thesis: verum end; definition let f be Function; func doms f -> Function means :Def2: :: FUNCT_6:def 2 ( dom it = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds it . x = proj1 (f . x) ) ); existence ex b1 being Function st ( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj1 (f . x) ) ) proof deffunc H1( set ) -> set = proj1 (f . \$1); ex F being Function st ( dom F = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj1 (f . x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj1 (f . x) ) & dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b2 . x = proj1 (f . x) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds f1 . x = proj1 (f . x) ) & dom f2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds f2 . x = proj1 (f . x) ) implies f1 = f2 ) assume that A1: dom f1 = f " (SubFuncs (rng f)) and A2: for x being set st x in f " (SubFuncs (rng f)) holds f1 . x = proj1 (f . x) and A3: dom f2 = f " (SubFuncs (rng f)) and A4: for x being set st x in f " (SubFuncs (rng f)) holds f2 . x = proj1 (f . x) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_f_"_(SubFuncs_(rng_f))_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in f " (SubFuncs (rng f)) implies f1 . x = f2 . x ) assume A5: x in f " (SubFuncs (rng f)) ; ::_thesis: f1 . x = f2 . x then f1 . x = proj1 (f . x) by A2; hence f1 . x = f2 . x by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; func rngs f -> Function means :Def3: :: FUNCT_6:def 3 ( dom it = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds it . x = proj2 (f . x) ) ); existence ex b1 being Function st ( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj2 (f . x) ) ) proof deffunc H1( set ) -> set = proj2 (f . \$1); ex F being Function st ( dom F = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj2 (f . x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b1 . x = proj2 (f . x) ) & dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b2 . x = proj2 (f . x) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds f1 . x = proj2 (f . x) ) & dom f2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds f2 . x = proj2 (f . x) ) implies f1 = f2 ) assume that A6: dom f1 = f " (SubFuncs (rng f)) and A7: for x being set st x in f " (SubFuncs (rng f)) holds f1 . x = proj2 (f . x) and A8: dom f2 = f " (SubFuncs (rng f)) and A9: for x being set st x in f " (SubFuncs (rng f)) holds f2 . x = proj2 (f . x) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_f_"_(SubFuncs_(rng_f))_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in f " (SubFuncs (rng f)) implies f1 . x = f2 . x ) assume A10: x in f " (SubFuncs (rng f)) ; ::_thesis: f1 . x = f2 . x then f1 . x = proj2 (f . x) by A7; hence f1 . x = f2 . x by A9, A10; ::_thesis: verum end; hence f1 = f2 by A6, A8, FUNCT_1:2; ::_thesis: verum end; func meet f -> set equals :: FUNCT_6:def 4 meet (rng f); correctness coherence meet (rng f) is set ; ; end; :: deftheorem Def2 defines doms FUNCT_6:def_2_:_ for f, b2 being Function holds ( b2 = doms f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b2 . x = proj1 (f . x) ) ) ); :: deftheorem Def3 defines rngs FUNCT_6:def_3_:_ for f, b2 being Function holds ( b2 = rngs f iff ( dom b2 = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds b2 . x = proj2 (f . x) ) ) ); :: deftheorem defines meet FUNCT_6:def_4_:_ for f being Function holds meet f = meet (rng f); theorem Th22: :: FUNCT_6:22 for x being set for f, g being Function st x in dom f & g = f . x holds ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) proof let x be set ; ::_thesis: for f, g being Function st x in dom f & g = f . x holds ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) let f, g be Function; ::_thesis: ( x in dom f & g = f . x implies ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) ) assume that A1: x in dom f and A2: g = f . x ; ::_thesis: ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) g in rng f by A1, A2, FUNCT_1:def_3; then g in SubFuncs (rng f) by Def1; then x in f " (SubFuncs (rng f)) by A1, A2, FUNCT_1:def_7; hence ( x in dom (doms f) & (doms f) . x = dom g & x in dom (rngs f) & (rngs f) . x = rng g ) by A2, Def2, Def3; ::_thesis: verum end; theorem :: FUNCT_6:23 ( doms {} = {} & rngs {} = {} ) proof ( dom (doms {}) = {} " (SubFuncs {}) & dom (rngs {}) = {} " (SubFuncs {}) ) by Def2, Def3, RELAT_1:38; hence ( doms {} = {} & rngs {} = {} ) ; ::_thesis: verum end; theorem Th24: :: FUNCT_6:24 for X being set for f being Function holds ( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) ) proof let X be set ; ::_thesis: for f being Function holds ( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) ) let f be Function; ::_thesis: ( doms (X --> f) = X --> (dom f) & rngs (X --> f) = X --> (rng f) ) A1: ( dom (X --> (dom f)) = X & dom (doms (X --> f)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def2, FUNCOP_1:13; A2: rng (X --> f) c= {f} by FUNCOP_1:13; A3: SubFuncs (rng (X --> f)) = rng (X --> f) proof thus SubFuncs (rng (X --> f)) c= rng (X --> f) by Th18; :: according to XBOOLE_0:def_10 ::_thesis: rng (X --> f) c= SubFuncs (rng (X --> f)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (X --> f) or x in SubFuncs (rng (X --> f)) ) assume x in rng (X --> f) ; ::_thesis: x in SubFuncs (rng (X --> f)) hence x in SubFuncs (rng (X --> f)) by A2, Def1; ::_thesis: verum end; A4: ( dom (X --> f) = X & (X --> f) " (rng (X --> f)) = dom (X --> f) ) by FUNCOP_1:13, RELAT_1:134; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (doms_(X_-->_f))_._x_=_(X_-->_(dom_f))_._x let x be set ; ::_thesis: ( x in X implies (doms (X --> f)) . x = (X --> (dom f)) . x ) assume A5: x in X ; ::_thesis: (doms (X --> f)) . x = (X --> (dom f)) . x then ( (X --> f) . x = f & (X --> (dom f)) . x = dom f ) by FUNCOP_1:7; hence (doms (X --> f)) . x = (X --> (dom f)) . x by A4, A3, A5, Def2; ::_thesis: verum end; hence doms (X --> f) = X --> (dom f) by A1, A4, A3, FUNCT_1:2; ::_thesis: rngs (X --> f) = X --> (rng f) A6: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (rngs_(X_-->_f))_._x_=_(X_-->_(rng_f))_._x let x be set ; ::_thesis: ( x in X implies (rngs (X --> f)) . x = (X --> (rng f)) . x ) assume A7: x in X ; ::_thesis: (rngs (X --> f)) . x = (X --> (rng f)) . x then ( (X --> f) . x = f & (X --> (rng f)) . x = rng f ) by FUNCOP_1:7; hence (rngs (X --> f)) . x = (X --> (rng f)) . x by A4, A3, A7, Def3; ::_thesis: verum end; ( dom (X --> (rng f)) = X & dom (rngs (X --> f)) = (X --> f) " (SubFuncs (rng (X --> f))) ) by Def3, FUNCOP_1:13; hence rngs (X --> f) = X --> (rng f) by A4, A3, A6, FUNCT_1:2; ::_thesis: verum end; theorem Th25: :: FUNCT_6:25 for x being set for f being Function st f <> {} holds ( x in meet f iff for y being set st y in dom f holds x in f . y ) proof let x be set ; ::_thesis: for f being Function st f <> {} holds ( x in meet f iff for y being set st y in dom f holds x in f . y ) let f be Function; ::_thesis: ( f <> {} implies ( x in meet f iff for y being set st y in dom f holds x in f . y ) ) assume A1: f <> {} ; ::_thesis: ( x in meet f iff for y being set st y in dom f holds x in f . y ) thus ( x in meet f implies for y being set st y in dom f holds x in f . y ) ::_thesis: ( ( for y being set st y in dom f holds x in f . y ) implies x in meet f ) proof assume A2: x in meet f ; ::_thesis: for y being set st y in dom f holds x in f . y let y be set ; ::_thesis: ( y in dom f implies x in f . y ) assume y in dom f ; ::_thesis: x in f . y then f . y in rng f by FUNCT_1:def_3; then meet f c= f . y by SETFAM_1:3; hence x in f . y by A2; ::_thesis: verum end; assume A3: for y being set st y in dom f holds x in f . y ; ::_thesis: x in meet f now__::_thesis:_for_z_being_set_st_z_in_rng_f_holds_ x_in_z let z be set ; ::_thesis: ( z in rng f implies x in z ) assume z in rng f ; ::_thesis: x in z then ex y being set st ( y in dom f & z = f . y ) by FUNCT_1:def_3; hence x in z by A3; ::_thesis: verum end; hence x in meet f by A1, SETFAM_1:def_1; ::_thesis: verum end; theorem :: FUNCT_6:26 for Y being set holds ( Union ({} --> Y) = {} & meet ({} --> Y) = {} ) proof let Y be set ; ::_thesis: ( Union ({} --> Y) = {} & meet ({} --> Y) = {} ) union (rng ({} --> Y)) = {} by ZFMISC_1:2; hence ( Union ({} --> Y) = {} & meet ({} --> Y) = {} ) by CARD_3:def_4, SETFAM_1:def_1; ::_thesis: verum end; theorem Th27: :: FUNCT_6:27 for X, Y being set st X <> {} holds ( Union (X --> Y) = Y & meet (X --> Y) = Y ) proof let X, Y be set ; ::_thesis: ( X <> {} implies ( Union (X --> Y) = Y & meet (X --> Y) = Y ) ) assume X <> {} ; ::_thesis: ( Union (X --> Y) = Y & meet (X --> Y) = Y ) then A1: rng (X --> Y) = {Y} by FUNCOP_1:8; then union (rng (X --> Y)) = Y by ZFMISC_1:25; hence ( Union (X --> Y) = Y & meet (X --> Y) = Y ) by A1, CARD_3:def_4, SETFAM_1:10; ::_thesis: verum end; definition let f be Function; let x, y be set ; funcf .. (x,y) -> set equals :: FUNCT_6:def 5 (uncurry f) . (x,y); correctness coherence (uncurry f) . (x,y) is set ; ; end; :: deftheorem defines .. FUNCT_6:def_5_:_ for f being Function for x, y being set holds f .. (x,y) = (uncurry f) . (x,y); theorem :: FUNCT_6:28 for x, X, y being set for f being Function st x in X & y in dom f holds (X --> f) .. (x,y) = f . y proof let x, X, y be set ; ::_thesis: for f being Function st x in X & y in dom f holds (X --> f) .. (x,y) = f . y let f be Function; ::_thesis: ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y ) A1: ( x in X implies (X --> f) . x = f ) by FUNCOP_1:7; dom (X --> f) = X by FUNCOP_1:13; hence ( x in X & y in dom f implies (X --> f) .. (x,y) = f . y ) by A1, FUNCT_5:38; ::_thesis: verum end; begin definition let f be Function; func<:f:> -> Function equals :: FUNCT_6:def 6 curry ((uncurry' f) | [:(meet (doms f)),(dom f):]); correctness coherence curry ((uncurry' f) | [:(meet (doms f)),(dom f):]) is Function; ; end; :: deftheorem defines <: FUNCT_6:def_6_:_ for f being Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]); theorem Th29: :: FUNCT_6:29 for f being Function holds ( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) ) proof let f be Function; ::_thesis: ( dom <:f:> = meet (doms f) & rng <:f:> c= product (rngs f) ) set f9 = (uncurry' f) | [:(meet (doms f)),(dom f):]; dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) c= [:(meet (doms f)),(dom f):] by RELAT_1:58; hence A1: dom <:f:> c= meet (doms f) by FUNCT_5:25; :: according to XBOOLE_0:def_10 ::_thesis: ( meet (doms f) c= dom <:f:> & rng <:f:> c= product (rngs f) ) A2: dom (doms f) = f " (SubFuncs (rng f)) by Def2; thus meet (doms f) c= dom <:f:> ::_thesis: rng <:f:> c= product (rngs f) proof set y = the Element of rng (doms f); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (doms f) or x in dom <:f:> ) assume A3: x in meet (doms f) ; ::_thesis: x in dom <:f:> then A4: rng (doms f) <> {} by SETFAM_1:def_1; then A5: x in the Element of rng (doms f) by A3, SETFAM_1:def_1; consider z being set such that A6: z in dom (doms f) and A7: the Element of rng (doms f) = (doms f) . z by A4, FUNCT_1:def_3; f . z in SubFuncs (rng f) by A2, A6, FUNCT_1:def_7; then reconsider g = f . z as Function by Def1; A8: z in dom f by A2, A6, FUNCT_1:def_7; then the Element of rng (doms f) = dom g by A7, Th22; then A9: [x,z] in dom (uncurry' f) by A8, A5, FUNCT_5:39; [x,z] in [:(meet (doms f)),(dom f):] by A3, A8, ZFMISC_1:87; then [x,z] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by A9, XBOOLE_0:def_4; then [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by RELAT_1:61; then x in proj1 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by XTUPLE_0:def_12; hence x in dom <:f:> by FUNCT_5:def_1; ::_thesis: verum end; A10: dom (rngs f) = f " (SubFuncs (rng f)) by Def3; thus rng <:f:> c= product (rngs f) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng <:f:> or y in product (rngs f) ) A11: dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) = (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:61; A12: uncurry' f = ~ (uncurry f) by FUNCT_5:def_4; assume y in rng <:f:> ; ::_thesis: y in product (rngs f) then consider x being set such that A13: x in dom <:f:> and A14: y = <:f:> . x by FUNCT_1:def_3; reconsider g = y as Function by A13, A14, FUNCT_5:30; A15: dom g = proj2 ((dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):]) by A13, A14, FUNCT_5:31; A16: dom g = dom (rngs f) proof thus dom g c= dom (rngs f) :: according to XBOOLE_0:def_10 ::_thesis: dom (rngs f) c= dom g proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom g or z in dom (rngs f) ) assume z in dom g ; ::_thesis: z in dom (rngs f) then [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A13, A14, FUNCT_5:31; then [x,z] in dom (uncurry' f) by A11, XBOOLE_0:def_4; then [z,x] in dom (uncurry f) by A12, FUNCT_4:42; then consider y1 being set , h being Function, y2 being set such that A17: [z,x] = [y1,y2] and A18: y1 in dom f and A19: h = f . y1 and y2 in dom h by FUNCT_5:def_2; A20: z = y1 by A17, XTUPLE_0:1; h in rng f by A18, A19, FUNCT_1:def_3; then f . z in SubFuncs (rng f) by A19, A20, Def1; hence z in dom (rngs f) by A10, A18, A20, FUNCT_1:def_7; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (rngs f) or z in dom g ) A21: x in {x} by TARSKI:def_1; assume A22: z in dom (rngs f) ; ::_thesis: z in dom g then f . z in SubFuncs (rng f) by A10, FUNCT_1:def_7; then reconsider h = f . z as Function by Def1; A23: z in dom f by A10, A22, FUNCT_1:def_7; then dom h = (doms f) . z by Th22; then dom h in rng (doms f) by A2, A10, A22, FUNCT_1:def_3; then x in dom h by A1, A13, SETFAM_1:def_1; then [z,x] in dom (uncurry f) by A23, FUNCT_5:def_2; then A24: [x,z] in dom (uncurry' f) by A12, FUNCT_4:42; [x,z] in [:(meet (doms f)),(dom f):] by A1, A13, A23, ZFMISC_1:87; then A25: [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A11, A24, XBOOLE_0:def_4; then z in proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) by XTUPLE_0:def_13; then [x,z] in [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A21, ZFMISC_1:87; then [x,z] in (dom ((uncurry' f) | [:(meet (doms f)),(dom f):])) /\ [:{x},(proj2 (dom ((uncurry' f) | [:(meet (doms f)),(dom f):]))):] by A25, XBOOLE_0:def_4; hence z in dom g by A15, XTUPLE_0:def_13; ::_thesis: verum end; now__::_thesis:_for_z_being_set_st_z_in_dom_(rngs_f)_holds_ g_._z_in_(rngs_f)_._z let z be set ; ::_thesis: ( z in dom (rngs f) implies g . z in (rngs f) . z ) assume A26: z in dom (rngs f) ; ::_thesis: g . z in (rngs f) . z then f . z in SubFuncs (rng f) by A10, FUNCT_1:def_7; then reconsider h = f . z as Function by Def1; A27: z in dom f by A10, A26, FUNCT_1:def_7; then dom h = (doms f) . z by Th22; then dom h in rng (doms f) by A2, A10, A26, FUNCT_1:def_3; then A28: x in dom h by A1, A13, SETFAM_1:def_1; then A29: h . x in rng h by FUNCT_1:def_3; ( g . z = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (x,z) & [x,z] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) ) by A13, A14, A16, A26, FUNCT_5:31; then (uncurry' f) . (x,z) = g . z by FUNCT_1:47; then g . z = h . x by A27, A28, FUNCT_5:39; hence g . z in (rngs f) . z by A27, A29, Th22; ::_thesis: verum end; hence y in product (rngs f) by A16, CARD_3:def_5; ::_thesis: verum end; end; theorem Th30: :: FUNCT_6:30 for x being set for f being Function st x in dom <:f:> holds <:f:> . x is Function proof let x be set ; ::_thesis: for f being Function st x in dom <:f:> holds <:f:> . x is Function let f be Function; ::_thesis: ( x in dom <:f:> implies <:f:> . x is Function ) assume x in dom <:f:> ; ::_thesis: <:f:> . x is Function then A1: <:f:> . x in rng <:f:> by FUNCT_1:def_3; rng <:f:> c= product (rngs f) by Th29; then ex g being Function st ( <:f:> . x = g & dom g = dom (rngs f) & ( for x being set st x in dom (rngs f) holds g . x in (rngs f) . x ) ) by A1, CARD_3:def_5; hence <:f:> . x is Function ; ::_thesis: verum end; theorem Th31: :: FUNCT_6:31 for x being set for f, g being Function st x in dom <:f:> & g = <:f:> . x holds ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) ) proof let x be set ; ::_thesis: for f, g being Function st x in dom <:f:> & g = <:f:> . x holds ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) ) let f, g be Function; ::_thesis: ( x in dom <:f:> & g = <:f:> . x implies ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) ) ) A1: ( rng <:f:> c= product (rngs f) & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3, Th29; assume A2: ( x in dom <:f:> & g = <:f:> . x ) ; ::_thesis: ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) ) then g in rng <:f:> by FUNCT_1:def_3; hence dom g = f " (SubFuncs (rng f)) by A1, CARD_3:9; ::_thesis: for y being set st y in dom g holds ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) let y be set ; ::_thesis: ( y in dom g implies ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) assume A3: y in dom g ; ::_thesis: ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) A4: [x,y] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A2, A3, FUNCT_5:31; then [x,y] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:61; then A5: [x,y] in dom (uncurry' f) by XBOOLE_0:def_4; g . y = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (x,y) by A2, A3, FUNCT_5:31; then A6: g . y = (uncurry' f) . (x,y) by A4, FUNCT_1:47; ~ (uncurry f) = uncurry' f by FUNCT_5:def_4; hence ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) by A6, A5, FUNCT_4:42, FUNCT_4:43; ::_thesis: verum end; theorem Th32: :: FUNCT_6:32 for x being set for f being Function st x in dom <:f:> holds for g being Function st g in rng f holds x in dom g proof let x be set ; ::_thesis: for f being Function st x in dom <:f:> holds for g being Function st g in rng f holds x in dom g let f be Function; ::_thesis: ( x in dom <:f:> implies for g being Function st g in rng f holds x in dom g ) assume A1: x in dom <:f:> ; ::_thesis: for g being Function st g in rng f holds x in dom g let g be Function; ::_thesis: ( g in rng f implies x in dom g ) assume g in rng f ; ::_thesis: x in dom g then consider y being set such that A2: ( y in dom f & g = f . y ) by FUNCT_1:def_3; ( y in dom (doms f) & (doms f) . y = dom g ) by A2, Th22; then dom g in rng (doms f) by FUNCT_1:def_3; then A3: meet (rng (doms f)) c= dom g by SETFAM_1:3; meet (doms f) = dom <:f:> by Th29; hence x in dom g by A1, A3; ::_thesis: verum end; theorem :: FUNCT_6:33 for x being set for g, f being Function st g in rng f & ( for g being Function st g in rng f holds x in dom g ) holds x in dom <:f:> proof let x be set ; ::_thesis: for g, f being Function st g in rng f & ( for g being Function st g in rng f holds x in dom g ) holds x in dom <:f:> let g, f be Function; ::_thesis: ( g in rng f & ( for g being Function st g in rng f holds x in dom g ) implies x in dom <:f:> ) assume that A1: g in rng f and A2: for g being Function st g in rng f holds x in dom g ; ::_thesis: x in dom <:f:> ex y being set st ( y in dom f & g = f . y ) by A1, FUNCT_1:def_3; then A3: doms f <> {} by Th22, RELAT_1:38; A4: now__::_thesis:_for_y_being_set_st_y_in_dom_(doms_f)_holds_ x_in_(doms_f)_._y let y be set ; ::_thesis: ( y in dom (doms f) implies x in (doms f) . y ) assume y in dom (doms f) ; ::_thesis: x in (doms f) . y then A5: y in f " (SubFuncs (rng f)) by Def2; then f . y in SubFuncs (rng f) by FUNCT_1:def_7; then reconsider g = f . y as Function by Def1; A6: y in dom f by A5, FUNCT_1:def_7; then g in rng f by FUNCT_1:def_3; then x in dom g by A2; hence x in (doms f) . y by A6, Th22; ::_thesis: verum end; dom <:f:> = meet (doms f) by Th29; hence x in dom <:f:> by A3, A4, Th25; ::_thesis: verum end; theorem Th34: :: FUNCT_6:34 for x, y being set for f, g, h being Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds g . y = h . x proof let x, y be set ; ::_thesis: for f, g, h being Function st x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y holds g . y = h . x let f, g, h be Function; ::_thesis: ( x in dom f & g = f . x & y in dom <:f:> & h = <:f:> . y implies g . y = h . x ) assume that A1: ( x in dom f & g = f . x ) and A2: y in dom <:f:> and A3: h = <:f:> . y ; ::_thesis: g . y = h . x dom h = f " (SubFuncs (rng f)) by A2, A3, Th31; then x in dom h by A1, Th19; then A4: h . x = (uncurry f) . (x,y) by A2, A3, Th31; g in rng f by A1, FUNCT_1:def_3; then y in dom g by A2, Th32; hence g . y = h . x by A1, A4, FUNCT_5:38; ::_thesis: verum end; theorem :: FUNCT_6:35 for x, y being set for f being Function st x in dom f & f . x is Function & y in dom <:f:> holds f .. (x,y) = <:f:> .. (y,x) proof let x, y be set ; ::_thesis: for f being Function st x in dom f & f . x is Function & y in dom <:f:> holds f .. (x,y) = <:f:> .. (y,x) let f be Function; ::_thesis: ( x in dom f & f . x is Function & y in dom <:f:> implies f .. (x,y) = <:f:> .. (y,x) ) assume that A1: x in dom f and A2: f . x is Function and A3: y in dom <:f:> ; ::_thesis: f .. (x,y) = <:f:> .. (y,x) reconsider g = f . x, h = <:f:> . y as Function by A2, A3, Th30; A4: dom h = f " (SubFuncs (rng f)) by A3, Th31; A5: g in rng f by A1, FUNCT_1:def_3; then g in SubFuncs (rng f) by Def1; then A6: x in dom h by A1, A4, FUNCT_1:def_7; y in dom g by A3, A5, Th32; hence f .. (x,y) = g . y by A1, FUNCT_5:38 .= h . x by A1, A3, Th34 .= <:f:> .. (y,x) by A3, A6, FUNCT_5:38 ; ::_thesis: verum end; definition let f be Function; func Frege f -> Function means :Def7: :: FUNCT_6:def 7 ( dom it = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( it . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) ); existence ex b1 being Function st ( dom b1 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( b1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) ) proof defpred S1[ set , set ] means ex g, h being Function st ( \$1 = g & \$2 = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds h . z = (uncurry f) . (z,(g . z)) ) ); A1: for x being set st x in product (doms f) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in product (doms f) implies ex y being set st S1[x,y] ) assume x in product (doms f) ; ::_thesis: ex y being set st S1[x,y] then consider g being Function such that A2: x = g and dom g = dom (doms f) and for x being set st x in dom (doms f) holds g . x in (doms f) . x by CARD_3:def_5; deffunc H1( set ) -> set = (uncurry f) . [\$1,(g . \$1)]; consider h being Function such that A3: ( dom h = f " (SubFuncs (rng f)) & ( for z being set st z in f " (SubFuncs (rng f)) holds h . z = H1(z) ) ) from FUNCT_1:sch_3(); reconsider y = h as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ex h being Function st ( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds h . z = (uncurry f) . (z,(g . z)) ) ) take h ; ::_thesis: ( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds h . z = (uncurry f) . (z,(g . z)) ) ) thus ( x = g & y = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds h . z = (uncurry f) . (z,(g . z)) ) ) by A2, A3; ::_thesis: verum end; consider F being Function such that A4: ( dom F = product (doms f) & ( for x being set st x in product (doms f) holds S1[x,F . x] ) ) from CLASSES1:sch_1(A1); take F ; ::_thesis: ( dom F = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) ) thus dom F = product (doms f) by A4; ::_thesis: for g being Function st g in product (doms f) holds ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) let g be Function; ::_thesis: ( g in product (doms f) implies ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) assume g in product (doms f) ; ::_thesis: ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) then ex g1, h being Function st ( g = g1 & F . g = h & dom h = f " (SubFuncs (rng f)) & ( for z being set st z in dom h holds h . z = (uncurry f) . (z,(g1 . z)) ) ) by A4; hence ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( b1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) & dom b2 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( b2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( f1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) & dom f2 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( f2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) implies f1 = f2 ) assume that A5: dom f1 = product (doms f) and A6: for g being Function st g in product (doms f) holds ex h being Function st ( f1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) and A7: dom f2 = product (doms f) and A8: for g being Function st g in product (doms f) holds ex h being Function st ( f2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_product_(doms_f)_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in product (doms f) implies f1 . x = f2 . x ) assume A9: x in product (doms f) ; ::_thesis: f1 . x = f2 . x then consider g being Function such that A10: x = g and dom g = dom (doms f) and for x being set st x in dom (doms f) holds g . x in (doms f) . x by CARD_3:def_5; consider h2 being Function such that A11: f2 . g = h2 and A12: dom h2 = f " (SubFuncs (rng f)) and A13: for y being set st y in dom h2 holds h2 . y = (uncurry f) . (y,(g . y)) by A8, A9, A10; consider h1 being Function such that A14: f1 . g = h1 and A15: dom h1 = f " (SubFuncs (rng f)) and A16: for y being set st y in dom h1 holds h1 . y = (uncurry f) . (y,(g . y)) by A6, A9, A10; now__::_thesis:_for_z_being_set_st_z_in_f_"_(SubFuncs_(rng_f))_holds_ h1_._z_=_h2_._z let z be set ; ::_thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = h2 . z ) assume A17: z in f " (SubFuncs (rng f)) ; ::_thesis: h1 . z = h2 . z then h1 . z = (uncurry f) . (z,(g . z)) by A15, A16; hence h1 . z = h2 . z by A12, A13, A17; ::_thesis: verum end; hence f1 . x = f2 . x by A10, A14, A15, A11, A12, FUNCT_1:2; ::_thesis: verum end; hence f1 = f2 by A5, A7, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines Frege FUNCT_6:def_7_:_ for f, b2 being Function holds ( b2 = Frege f iff ( dom b2 = product (doms f) & ( for g being Function st g in product (doms f) holds ex h being Function st ( b2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) ) ); theorem :: FUNCT_6:36 for x being set for g, f being Function st g in product (doms f) & x in dom g holds (Frege f) .. (g,x) = f .. (x,(g . x)) proof let x be set ; ::_thesis: for g, f being Function st g in product (doms f) & x in dom g holds (Frege f) .. (g,x) = f .. (x,(g . x)) let g, f be Function; ::_thesis: ( g in product (doms f) & x in dom g implies (Frege f) .. (g,x) = f .. (x,(g . x)) ) assume that A1: g in product (doms f) and A2: x in dom g ; ::_thesis: (Frege f) .. (g,x) = f .. (x,(g . x)) A3: dom g = dom (doms f) by A1, CARD_3:9; A4: dom (doms f) = f " (SubFuncs (rng f)) by Def2; consider h being Function such that A5: (Frege f) . g = h and A6: dom h = f " (SubFuncs (rng f)) and A7: for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) by A1, Def7; dom (Frege f) = product (doms f) by Def7; hence (Frege f) .. (g,x) = h . x by A1, A2, A5, A6, A3, A4, FUNCT_5:38 .= f .. (x,(g . x)) by A2, A6, A7, A3, A4 ; ::_thesis: verum end; Lm2: for f being Function holds rng (Frege f) c= product (rngs f) proof let f be Function; ::_thesis: rng (Frege f) c= product (rngs f) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Frege f) or x in product (rngs f) ) assume x in rng (Frege f) ; ::_thesis: x in product (rngs f) then consider y being set such that A1: y in dom (Frege f) and A2: x = (Frege f) . y by FUNCT_1:def_3; A3: dom (Frege f) = product (doms f) by Def7; then consider g being Function such that A4: y = g and dom g = dom (doms f) and A5: for z being set st z in dom (doms f) holds g . z in (doms f) . z by A1, CARD_3:def_5; consider h being Function such that A6: (Frege f) . g = h and A7: dom h = f " (SubFuncs (rng f)) and A8: for z being set st z in dom h holds h . z = (uncurry f) . (z,(g . z)) by A1, A3, A4, Def7; A9: dom (rngs f) = f " (SubFuncs (rng f)) by Def3; A10: dom (doms f) = f " (SubFuncs (rng f)) by Def2; now__::_thesis:_for_z_being_set_st_z_in_dom_(rngs_f)_holds_ h_._z_in_(rngs_f)_._z let z be set ; ::_thesis: ( z in dom (rngs f) implies h . z in (rngs f) . z ) assume A11: z in dom (rngs f) ; ::_thesis: h . z in (rngs f) . z then f . z in SubFuncs (rng f) by A9, FUNCT_1:def_7; then reconsider t = f . z as Function by Def1; A12: g . z in (doms f) . z by A5, A9, A10, A11; A13: z in dom f by A9, A11, FUNCT_1:def_7; then A14: (rngs f) . z = rng t by Th22; A15: (doms f) . z = dom t by A13, Th22; then A16: t . (g . z) in rng t by A12, FUNCT_1:def_3; t . (g . z) = (uncurry f) . (z,(g . z)) by A13, A12, A15, FUNCT_5:38; hence h . z in (rngs f) . z by A7, A8, A9, A11, A14, A16; ::_thesis: verum end; hence x in product (rngs f) by A2, A4, A6, A7, A9, CARD_3:def_5; ::_thesis: verum end; theorem :: FUNCT_6:37 for x being set for f, g, h, h9 being Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) proof let x be set ; ::_thesis: for f, g, h, h9 being Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) let f, g, h, h9 be Function; ::_thesis: ( x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h implies ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) ) assume that A1: ( x in dom f & g = f . x ) and A2: h in product (doms f) and A3: h9 = (Frege f) . h ; ::_thesis: ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) A4: x in f " (SubFuncs (rng f)) by A1, Th19; A5: dom (doms f) = f " (SubFuncs (rng f)) by Def2; ( ex f2 being Function st ( h = f2 & dom f2 = dom (doms f) & ( for x being set st x in dom (doms f) holds f2 . x in (doms f) . x ) ) & (doms f) . x = dom g ) by A1, A2, Th22, CARD_3:def_5; hence A6: h . x in dom g by A5, A4; ::_thesis: ( h9 . x = g . (h . x) & h9 in product (rngs f) ) ex f1 being Function st ( (Frege f) . h = f1 & dom f1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom f1 holds f1 . x = (uncurry f) . (x,(h . x)) ) ) by A2, Def7; hence h9 . x = (uncurry f) . (x,(h . x)) by A3, A4 .= g . (h . x) by A1, A6, FUNCT_5:38 ; ::_thesis: h9 in product (rngs f) A7: rng (Frege f) c= product (rngs f) by Lm2; dom (Frege f) = product (doms f) by Def7; then h9 in rng (Frege f) by A2, A3, FUNCT_1:def_3; hence h9 in product (rngs f) by A7; ::_thesis: verum end; Lm3: for f being Function holds product (rngs f) c= rng (Frege f) proof let f be Function; ::_thesis: product (rngs f) c= rng (Frege f) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (rngs f) or x in rng (Frege f) ) deffunc H1( set ) -> set = (doms f) . \$1; assume x in product (rngs f) ; ::_thesis: x in rng (Frege f) then consider g being Function such that A1: x = g and A2: dom g = dom (rngs f) and A3: for y being set st y in dom (rngs f) holds g . y in (rngs f) . y by CARD_3:def_5; defpred S1[ set , set ] means ex f1 being Function st ( f1 = f . \$1 & f1 . \$2 = g . \$1 ); consider h being Function such that A4: ( dom h = f " (SubFuncs (rng f)) & ( for x being set st x in f " (SubFuncs (rng f)) holds for y being set holds ( y in h . x iff ( y in H1(x) & S1[x,y] ) ) ) ) from CARD_3:sch_2(); A5: product (doms f) = dom (Frege f) by Def7; A6: dom (doms f) = f " (SubFuncs (rng f)) by Def2; A7: dom (rngs f) = f " (SubFuncs (rng f)) by Def3; A8: now__::_thesis:_for_X_being_set_st_X_in_rng_h_holds_ X_<>_{} let X be set ; ::_thesis: ( X in rng h implies X <> {} ) assume X in rng h ; ::_thesis: X <> {} then consider x being set such that A9: x in dom h and A10: X = h . x by FUNCT_1:def_3; f . x in SubFuncs (rng f) by A4, A9, FUNCT_1:def_7; then reconsider fx = f . x as Function by Def1; A11: x in dom f by A4, A9, FUNCT_1:def_7; then A12: (rngs f) . x = rng fx by Th22; g . x in (rngs f) . x by A3, A7, A4, A9; then A13: ex y being set st ( y in dom fx & g . x = fx . y ) by A12, FUNCT_1:def_3; (doms f) . x = dom fx by A11, Th22; hence X <> {} by A4, A9, A10, A13; ::_thesis: verum end; A14: now__::_thesis:_(_f_"_(SubFuncs_(rng_f))_<>_{}_implies_x_in_rng_(Frege_f)_) assume f " (SubFuncs (rng f)) <> {} ; ::_thesis: x in rng (Frege f) then reconsider D = rng h as non empty set by A4, RELAT_1:42; consider Ch being Function such that A15: dom Ch = D and A16: for x being set st x in D holds Ch . x in x by A8, FUNCT_1:111; A17: dom (Ch * h) = dom h by A15, RELAT_1:27; now__::_thesis:_for_y_being_set_st_y_in_dom_(doms_f)_holds_ (Ch_*_h)_._y_in_(doms_f)_._y let y be set ; ::_thesis: ( y in dom (doms f) implies (Ch * h) . y in (doms f) . y ) assume A18: y in dom (doms f) ; ::_thesis: (Ch * h) . y in (doms f) . y then ( (Ch * h) . y = Ch . (h . y) & h . y in rng h ) by A6, A4, A17, FUNCT_1:12, FUNCT_1:def_3; then (Ch * h) . y in h . y by A16; hence (Ch * h) . y in (doms f) . y by A6, A4, A18; ::_thesis: verum end; then A19: Ch * h in product (doms f) by A6, A4, A17, CARD_3:def_5; then consider h1 being Function such that A20: (Frege f) . (Ch * h) = h1 and A21: dom h1 = f " (SubFuncs (rng f)) and A22: for x being set st x in dom h1 holds h1 . x = (uncurry f) . (x,((Ch * h) . x)) by Def7; now__::_thesis:_for_z_being_set_st_z_in_f_"_(SubFuncs_(rng_f))_holds_ h1_._z_=_g_._z let z be set ; ::_thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = g . z ) assume A23: z in f " (SubFuncs (rng f)) ; ::_thesis: h1 . z = g . z then A24: h1 . z = (uncurry f) . (z,((Ch * h) . z)) by A21, A22; ( (Ch * h) . z = Ch . (h . z) & h . z in rng h ) by A4, A17, A23, FUNCT_1:12, FUNCT_1:def_3; then A25: (Ch * h) . z in h . z by A16; then consider f1 being Function such that A26: f1 = f . z and A27: f1 . ((Ch * h) . z) = g . z by A4, A23; A28: (Ch * h) . z in (doms f) . z by A4, A23, A25; A29: z in dom f by A23, FUNCT_1:def_7; then (doms f) . z = dom f1 by A26, Th22; hence h1 . z = g . z by A29, A24, A26, A27, A28, FUNCT_5:38; ::_thesis: verum end; then x = h1 by A1, A2, A7, A21, FUNCT_1:2; hence x in rng (Frege f) by A5, A19, A20, FUNCT_1:def_3; ::_thesis: verum end; now__::_thesis:_(_f_"_(SubFuncs_(rng_f))_=_{}_implies_x_in_rng_(Frege_f)_) assume A30: f " (SubFuncs (rng f)) = {} ; ::_thesis: x in rng (Frege f) then A31: g = {} by A2, Def3; dom (Frege f) = {{}} by A6, A5, A30, CARD_3:10, RELAT_1:41; then A32: {} in dom (Frege f) by TARSKI:def_1; then consider h being Function such that A33: (Frege f) . {} = h and A34: dom h = f " (SubFuncs (rng f)) and for x being set st x in dom h holds h . x = (uncurry f) . (x,({} . x)) by A5, Def7; h = {} by A30, A34; hence x in rng (Frege f) by A1, A31, A32, A33, FUNCT_1:def_3; ::_thesis: verum end; hence x in rng (Frege f) by A14; ::_thesis: verum end; theorem Th38: :: FUNCT_6:38 for f being Function holds rng (Frege f) = product (rngs f) proof let f be Function; ::_thesis: rng (Frege f) = product (rngs f) thus ( rng (Frege f) c= product (rngs f) & product (rngs f) c= rng (Frege f) ) by Lm2, Lm3; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th39: :: FUNCT_6:39 for f being Function st not {} in rng f holds ( Frege f is one-to-one iff for g being Function st g in rng f holds g is one-to-one ) proof let f be Function; ::_thesis: ( not {} in rng f implies ( Frege f is one-to-one iff for g being Function st g in rng f holds g is one-to-one ) ) set h0 = the Element of product (doms f); A1: dom (doms f) = f " (SubFuncs (rng f)) by Def2; assume A2: not {} in rng f ; ::_thesis: ( Frege f is one-to-one iff for g being Function st g in rng f holds g is one-to-one ) now__::_thesis:_not_{}_in_rng_(doms_f) assume {} in rng (doms f) ; ::_thesis: contradiction then consider x being set such that A3: x in dom (doms f) and A4: {} = (doms f) . x by FUNCT_1:def_3; A5: x in f " (SubFuncs (rng f)) by A3, Def2; then f . x in SubFuncs (rng f) by FUNCT_1:def_7; then reconsider g = f . x as Function by Def1; A6: x in dom f by A5, FUNCT_1:def_7; then A7: g in rng f by FUNCT_1:def_3; {} = dom g by A4, A6, Th22; hence contradiction by A2, A7, RELAT_1:41; ::_thesis: verum end; then product (doms f) <> {} by CARD_3:26; then consider h being Function such that the Element of product (doms f) = h and dom h = dom (doms f) and A8: for x being set st x in dom (doms f) holds h . x in (doms f) . x by CARD_3:def_5; A9: dom (Frege f) = product (doms f) by Def7; thus ( Frege f is one-to-one implies for g being Function st g in rng f holds g is one-to-one ) ::_thesis: ( ( for g being Function st g in rng f holds g is one-to-one ) implies Frege f is one-to-one ) proof deffunc H1( set ) -> set = h . \$1; assume A10: for x, y being set st x in dom (Frege f) & y in dom (Frege f) & (Frege f) . x = (Frege f) . y holds x = y ; :: according to FUNCT_1:def_4 ::_thesis: for g being Function st g in rng f holds g is one-to-one let g be Function; ::_thesis: ( g in rng f implies g is one-to-one ) assume g in rng f ; ::_thesis: g is one-to-one then consider z being set such that A11: ( z in dom f & g = f . z ) by FUNCT_1:def_3; defpred S1[ set ] means \$1 = z; let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom g or not b1 in dom g or not g . x = g . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y ) deffunc H2( set ) -> set = x; consider h1 being Function such that A12: ( dom h1 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds ( ( S1[a] implies h1 . a = H2(a) ) & ( not S1[a] implies h1 . a = H1(a) ) ) ) ) from PARTFUN1:sch_1(); assume that A13: x in dom g and A14: y in dom g and A15: g . x = g . y ; ::_thesis: x = y now__::_thesis:_for_a_being_set_st_a_in_dom_(doms_f)_holds_ h1_._a_in_(doms_f)_._a let a be set ; ::_thesis: ( a in dom (doms f) implies h1 . a in (doms f) . a ) assume A16: a in dom (doms f) ; ::_thesis: h1 . a in (doms f) . a then A17: ( a <> z implies h1 . a = h . a ) by A1, A12; ( a = z implies h1 . a = x ) by A1, A12, A16; hence h1 . a in (doms f) . a by A8, A11, A13, A16, A17, Th22; ::_thesis: verum end; then A18: h1 in product (doms f) by A1, A12, CARD_3:def_5; then consider g1 being Function such that A19: (Frege f) . h1 = g1 and A20: dom g1 = f " (SubFuncs (rng f)) and A21: for x being set st x in dom g1 holds g1 . x = (uncurry f) . (x,(h1 . x)) by Def7; defpred S2[ set ] means \$1 = z; deffunc H3( set ) -> set = h . \$1; deffunc H4( set ) -> set = y; consider h2 being Function such that A22: ( dom h2 = f " (SubFuncs (rng f)) & ( for a being set st a in f " (SubFuncs (rng f)) holds ( ( S2[a] implies h2 . a = H4(a) ) & ( not S2[a] implies h2 . a = H3(a) ) ) ) ) from PARTFUN1:sch_1(); now__::_thesis:_for_a_being_set_st_a_in_dom_(doms_f)_holds_ h2_._a_in_(doms_f)_._a let a be set ; ::_thesis: ( a in dom (doms f) implies h2 . a in (doms f) . a ) assume A23: a in dom (doms f) ; ::_thesis: h2 . a in (doms f) . a then A24: ( a <> z implies h2 . a = h . a ) by A1, A22; ( a = z implies h2 . a = y ) by A1, A22, A23; hence h2 . a in (doms f) . a by A8, A11, A14, A23, A24, Th22; ::_thesis: verum end; then A25: h2 in product (doms f) by A1, A22, CARD_3:def_5; then consider g2 being Function such that A26: (Frege f) . h2 = g2 and A27: dom g2 = f " (SubFuncs (rng f)) and A28: for x being set st x in dom g2 holds g2 . x = (uncurry f) . (x,(h2 . x)) by Def7; now__::_thesis:_for_a_being_set_st_a_in_f_"_(SubFuncs_(rng_f))_holds_ g1_._a_=_g2_._a let a be set ; ::_thesis: ( a in f " (SubFuncs (rng f)) implies g1 . b1 = g2 . b1 ) assume A29: a in f " (SubFuncs (rng f)) ; ::_thesis: g1 . b1 = g2 . b1 then A30: g2 . a = (uncurry f) . (a,(h2 . a)) by A27, A28; A31: g1 . a = (uncurry f) . (a,(h1 . a)) by A20, A21, A29; percases ( a <> z or a = z ) ; supposeA32: a <> z ; ::_thesis: g1 . b1 = g2 . b1 then h1 . a = h . a by A12, A29; hence g1 . a = g2 . a by A22, A29, A30, A31, A32; ::_thesis: verum end; supposeA33: a = z ; ::_thesis: g1 . b1 = g2 . b1 then h1 . a = x by A12, A29; then A34: g1 . a = g . x by A11, A13, A31, A33, FUNCT_5:38; h2 . a = y by A22, A29, A33; hence g1 . a = g2 . a by A11, A14, A15, A30, A33, A34, FUNCT_5:38; ::_thesis: verum end; end; end; then g1 = g2 by A20, A27, FUNCT_1:2; then A35: h1 = h2 by A9, A10, A18, A19, A25, A26; g in rng f by A11, FUNCT_1:def_3; then g in SubFuncs (rng f) by Def1; then A36: z in f " (SubFuncs (rng f)) by A11, FUNCT_1:def_7; then h1 . z = x by A12; hence x = y by A36, A22, A35; ::_thesis: verum end; assume A37: for g being Function st g in rng f holds g is one-to-one ; ::_thesis: Frege f is one-to-one let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (Frege f) or not b1 in dom (Frege f) or not (Frege f) . x = (Frege f) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (Frege f) or not y in dom (Frege f) or not (Frege f) . x = (Frege f) . y or x = y ) assume that A38: x in dom (Frege f) and A39: y in dom (Frege f) and A40: (Frege f) . x = (Frege f) . y ; ::_thesis: x = y consider g2 being Function such that A41: y = g2 and A42: dom g2 = dom (doms f) and A43: for x being set st x in dom (doms f) holds g2 . x in (doms f) . x by A9, A39, CARD_3:def_5; consider g1 being Function such that A44: x = g1 and A45: dom g1 = dom (doms f) and A46: for x being set st x in dom (doms f) holds g1 . x in (doms f) . x by A9, A38, CARD_3:def_5; consider h2 being Function such that A47: (Frege f) . g2 = h2 and A48: ( dom h2 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h2 holds h2 . x = (uncurry f) . (x,(g2 . x)) ) ) by A9, A39, A41, Def7; consider h1 being Function such that A49: (Frege f) . g1 = h1 and A50: ( dom h1 = f " (SubFuncs (rng f)) & ( for x being set st x in dom h1 holds h1 . x = (uncurry f) . (x,(g1 . x)) ) ) by A9, A38, A44, Def7; now__::_thesis:_for_a_being_set_st_a_in_f_"_(SubFuncs_(rng_f))_holds_ g1_._a_=_g2_._a let a be set ; ::_thesis: ( a in f " (SubFuncs (rng f)) implies g1 . a = g2 . a ) assume A51: a in f " (SubFuncs (rng f)) ; ::_thesis: g1 . a = g2 . a then f . a in SubFuncs (rng f) by FUNCT_1:def_7; then reconsider g = f . a as Function by Def1; A52: a in dom f by A51, FUNCT_1:def_7; then A53: dom g = (doms f) . a by Th22; then A54: g2 . a in dom g by A1, A43, A51; A55: g1 . a in dom g by A1, A46, A51, A53; h2 . a = (uncurry f) . (a,(g2 . a)) by A48, A51; then A56: h2 . a = g . (g2 . a) by A52, A54, FUNCT_5:38; g in rng f by A52, FUNCT_1:def_3; then A57: g is one-to-one by A37; h1 . a = (uncurry f) . (a,(g1 . a)) by A50, A51; then h1 . a = g . (g1 . a) by A52, A55, FUNCT_5:38; hence g1 . a = g2 . a by A40, A44, A41, A49, A47, A55, A54, A56, A57, FUNCT_1:def_4; ::_thesis: verum end; hence x = y by A1, A44, A45, A41, A42, FUNCT_1:2; ::_thesis: verum end; begin theorem :: FUNCT_6:40 ( <:{}:> = {} & Frege {} = {} .--> {} ) proof A1: dom (doms {}) = {} " (SubFuncs {}) by Def2, RELAT_1:38; then A2: product (doms {}) = {{}} by CARD_3:10, RELAT_1:41; A3: now__::_thesis:_for_x_being_set_st_x_in_{{}}_holds_ (Frege_{})_._x_=_{} let x be set ; ::_thesis: ( x in {{}} implies (Frege {}) . x = {} ) assume A4: x in {{}} ; ::_thesis: (Frege {}) . x = {} then A5: x = {} by TARSKI:def_1; then ex h being Function st ( (Frege {}) . {} = h & dom h = {} " (SubFuncs (rng {})) & ( for x being set st x in dom h holds h . x = (uncurry {}) . (x,({} . x)) ) ) by A2, A4, Def7; hence (Frege {}) . x = {} by A5; ::_thesis: verum end; A6: meet {} = {} by SETFAM_1:def_1; rng (doms {}) = {} by A1, RELAT_1:38, RELAT_1:41; then dom <:{}:> = {} by A6, Th29; hence <:{}:> = {} ; ::_thesis: Frege {} = {} .--> {} dom (Frege {}) = product (doms {}) by Def7; hence Frege {} = {} .--> {} by A2, A3, FUNCOP_1:11; ::_thesis: verum end; theorem :: FUNCT_6:41 for X being set for f being Function st X <> {} holds ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds <:(X --> f):> . x = X --> (f . x) ) ) proof let X be set ; ::_thesis: for f being Function st X <> {} holds ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds <:(X --> f):> . x = X --> (f . x) ) ) let f be Function; ::_thesis: ( X <> {} implies ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds <:(X --> f):> . x = X --> (f . x) ) ) ) assume A1: X <> {} ; ::_thesis: ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds <:(X --> f):> . x = X --> (f . x) ) ) thus A2: dom <:(X --> f):> = meet (doms (X --> f)) by Th29 .= meet (X --> (dom f)) by Th24 .= dom f by A1, Th27 ; ::_thesis: for x being set st x in dom f holds <:(X --> f):> . x = X --> (f . x) A3: ( rng <:(X --> f):> c= product (rngs (X --> f)) & rngs (X --> f) = X --> (rng f) ) by Th24, Th29; let x be set ; ::_thesis: ( x in dom f implies <:(X --> f):> . x = X --> (f . x) ) assume A4: x in dom f ; ::_thesis: <:(X --> f):> . x = X --> (f . x) then <:(X --> f):> . x in rng <:(X --> f):> by A2, FUNCT_1:def_3; then consider g being Function such that A5: <:(X --> f):> . x = g and A6: dom g = dom (X --> (rng f)) and for y being set st y in dom (X --> (rng f)) holds g . y in (X --> (rng f)) . y by A3, CARD_3:def_5; A7: dom g = X by A6, FUNCOP_1:13; A8: dom (X --> f) = X by FUNCOP_1:13; A9: now__::_thesis:_for_y_being_set_st_y_in_X_holds_ g_._y_=_(X_-->_(f_._x))_._y let y be set ; ::_thesis: ( y in X implies g . y = (X --> (f . x)) . y ) assume A10: y in X ; ::_thesis: g . y = (X --> (f . x)) . y then ( g . y = (uncurry (X --> f)) . (y,x) & (X --> f) . y = f ) by A2, A4, A5, A7, Th31, FUNCOP_1:7; then g . y = f . x by A4, A8, A10, FUNCT_5:38; hence g . y = (X --> (f . x)) . y by A10, FUNCOP_1:7; ::_thesis: verum end; dom (X --> (f . x)) = X by FUNCOP_1:13; hence <:(X --> f):> . x = X --> (f . x) by A5, A7, A9, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_6:42 for X being set for f being Function holds ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) & ( for g being Function st g in Funcs (X,(dom f)) holds (Frege (X --> f)) . g = f * g ) ) proof let X be set ; ::_thesis: for f being Function holds ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) & ( for g being Function st g in Funcs (X,(dom f)) holds (Frege (X --> f)) . g = f * g ) ) let f be Function; ::_thesis: ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) & ( for g being Function st g in Funcs (X,(dom f)) holds (Frege (X --> f)) . g = f * g ) ) A1: product (X --> (dom f)) = Funcs (X,(dom f)) by CARD_3:11; A2: doms (X --> f) = X --> (dom f) by Th24; ( rngs (X --> f) = X --> (rng f) & product (X --> (rng f)) = Funcs (X,(rng f)) ) by Th24, CARD_3:11; hence ( dom (Frege (X --> f)) = Funcs (X,(dom f)) & rng (Frege (X --> f)) = Funcs (X,(rng f)) ) by A2, A1, Def7, Th38; ::_thesis: for g being Function st g in Funcs (X,(dom f)) holds (Frege (X --> f)) . g = f * g let g be Function; ::_thesis: ( g in Funcs (X,(dom f)) implies (Frege (X --> f)) . g = f * g ) assume A3: g in Funcs (X,(dom f)) ; ::_thesis: (Frege (X --> f)) . g = f * g then consider h being Function such that A4: (Frege (X --> f)) . g = h and A5: dom h = (X --> f) " (SubFuncs (rng (X --> f))) and A6: for x being set st x in dom h holds h . x = (uncurry (X --> f)) . (x,(g . x)) by A2, A1, Def7; dom (X --> (dom f)) = X by FUNCOP_1:13; then A7: dom h = X by A2, A5, Def2; A8: ex g9 being Function st ( g = g9 & dom g9 = X & rng g9 c= dom f ) by A3, FUNCT_2:def_2; then A9: dom (f * g) = X by RELAT_1:27; A10: dom (X --> f) = X by FUNCOP_1:13; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (f_*_g)_._x_=_h_._x let x be set ; ::_thesis: ( x in X implies (f * g) . x = h . x ) assume A11: x in X ; ::_thesis: (f * g) . x = h . x then A12: ( h . x = (uncurry (X --> f)) . (x,(g . x)) & (X --> f) . x = f ) by A6, A7, FUNCOP_1:7; ( g . x in rng g & (f * g) . x = f . (g . x) ) by A8, A9, A11, FUNCT_1:12, FUNCT_1:def_3; hence (f * g) . x = h . x by A8, A10, A11, A12, FUNCT_5:38; ::_thesis: verum end; hence (Frege (X --> f)) . g = f * g by A4, A7, A9, FUNCT_1:2; ::_thesis: verum end; theorem Th43: :: FUNCT_6:43 for X being set for f, g being Function st dom f = X & dom g = X & ( for x being set st x in X holds f . x,g . x are_equipotent ) holds product f, product g are_equipotent proof let X be set ; ::_thesis: for f, g being Function st dom f = X & dom g = X & ( for x being set st x in X holds f . x,g . x are_equipotent ) holds product f, product g are_equipotent let f, g be Function; ::_thesis: ( dom f = X & dom g = X & ( for x being set st x in X holds f . x,g . x are_equipotent ) implies product f, product g are_equipotent ) assume that A1: dom f = X and A2: dom g = X and A3: for x being set st x in X holds f . x,g . x are_equipotent ; ::_thesis: product f, product g are_equipotent defpred S1[ set , set ] means ex f1 being Function st ( \$2 = f1 & f1 is one-to-one & dom f1 = f . \$1 & rng f1 = g . \$1 ); A4: for x being set st x in X holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] ) assume x in X ; ::_thesis: ex y being set st S1[x,y] then f . x,g . x are_equipotent by A3; then ex h being Function st ( h is one-to-one & dom h = f . x & rng h = g . x ) by WELLORD2:def_4; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider h being Function such that A5: ( dom h = X & ( for x being set st x in X holds S1[x,h . x] ) ) from CLASSES1:sch_1(A4); A6: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (rngs_h)_._x_=_g_._x let x be set ; ::_thesis: ( x in X implies (rngs h) . x = g . x ) assume A7: x in X ; ::_thesis: (rngs h) . x = g . x then ex f1 being Function st ( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5; hence (rngs h) . x = g . x by A5, A7, Th22; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_rng_h_holds_ x_is_Function let x be set ; ::_thesis: ( x in rng h implies x is Function ) assume x in rng h ; ::_thesis: x is Function then consider a being set such that A8: ( a in X & x = h . a ) by A5, FUNCT_1:def_3; ex f1 being Function st ( x = f1 & f1 is one-to-one & dom f1 = f . a & rng f1 = g . a ) by A5, A8; hence x is Function ; ::_thesis: verum end; then SubFuncs (rng h) = rng h by Lm1; then A9: h " (SubFuncs (rng h)) = X by A5, RELAT_1:134; then dom (rngs h) = X by Def3; then A10: rngs h = g by A2, A6, FUNCT_1:2; A11: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (doms_h)_._x_=_f_._x let x be set ; ::_thesis: ( x in X implies (doms h) . x = f . x ) assume A12: x in X ; ::_thesis: (doms h) . x = f . x then ex f1 being Function st ( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5; hence (doms h) . x = f . x by A5, A12, Th22; ::_thesis: verum end; dom (doms h) = X by A9, Def2; then A13: doms h = f by A1, A11, FUNCT_1:2; now__::_thesis:_product_f,_product_g_are_equipotent percases ( {} in rng h or not {} in rng h ) ; suppose {} in rng h ; ::_thesis: product f, product g are_equipotent then consider x being set such that A14: x in X and A15: {} = h . x by A5, FUNCT_1:def_3; A16: ex f1 being Function st ( {} = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A14, A15; then {} in rng f by A1, A14, FUNCT_1:def_3, RELAT_1:38; then A17: product f = {} by CARD_3:26; {} in rng g by A2, A14, A16, FUNCT_1:def_3, RELAT_1:38; hence product f, product g are_equipotent by A17, CARD_3:26; ::_thesis: verum end; supposeA18: not {} in rng h ; ::_thesis: product f, product g are_equipotent A19: now__::_thesis:_for_f1_being_Function_st_f1_in_rng_h_holds_ f1_is_one-to-one let f1 be Function; ::_thesis: ( f1 in rng h implies f1 is one-to-one ) assume f1 in rng h ; ::_thesis: f1 is one-to-one then consider x being set such that A20: x in X and A21: f1 = h . x by A5, FUNCT_1:def_3; ex f1 being Function st ( h . x = f1 & f1 is one-to-one & dom f1 = f . x & rng f1 = g . x ) by A5, A20; hence f1 is one-to-one by A21; ::_thesis: verum end; thus product f, product g are_equipotent ::_thesis: verum proof take Frege h ; :: according to WELLORD2:def_4 ::_thesis: ( Frege h is one-to-one & dom (Frege h) = product f & rng (Frege h) = product g ) thus ( Frege h is one-to-one & dom (Frege h) = product f & rng (Frege h) = product g ) by A13, A10, A18, A19, Def7, Th38, Th39; ::_thesis: verum end; end; end; end; hence product f, product g are_equipotent ; ::_thesis: verum end; theorem Th44: :: FUNCT_6:44 for f, h, g being Function st dom f = dom h & dom g = rng h & h is one-to-one & ( for x being set st x in dom h holds f . x,g . (h . x) are_equipotent ) holds product f, product g are_equipotent proof let f, h, g be Function; ::_thesis: ( dom f = dom h & dom g = rng h & h is one-to-one & ( for x being set st x in dom h holds f . x,g . (h . x) are_equipotent ) implies product f, product g are_equipotent ) set X = dom f; assume that A1: dom f = dom h and A2: dom g = rng h and A3: h is one-to-one and A4: for x being set st x in dom h holds f . x,g . (h . x) are_equipotent ; ::_thesis: product f, product g are_equipotent A5: h * (h ") = id (dom g) by A2, A3, FUNCT_1:39; A6: dom (g * h) = dom f by A1, A2, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x,(g_*_h)_._x_are_equipotent let x be set ; ::_thesis: ( x in dom f implies f . x,(g * h) . x are_equipotent ) assume A7: x in dom f ; ::_thesis: f . x,(g * h) . x are_equipotent then f . x,g . (h . x) are_equipotent by A1, A4; hence f . x,(g * h) . x are_equipotent by A6, A7, FUNCT_1:12; ::_thesis: verum end; then A8: product f, product (g * h) are_equipotent by A6, Th43; defpred S1[ set , set ] means ex f1 being Function st ( \$1 = f1 & \$2 = f1 * (h ") ); A9: for x being set st x in product (g * h) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in product (g * h) implies ex y being set st S1[x,y] ) assume x in product (g * h) ; ::_thesis: ex y being set st S1[x,y] then ex f1 being Function st ( x = f1 & dom f1 = dom (g * h) & ( for y being set st y in dom (g * h) holds f1 . y in (g * h) . y ) ) by CARD_3:def_5; then consider f1 being Function such that A10: x = f1 ; f1 * (h ") = f1 * (h ") ; hence ex y being set st S1[x,y] by A10; ::_thesis: verum end; consider F being Function such that A11: ( dom F = product (g * h) & ( for x being set st x in product (g * h) holds S1[x,F . x] ) ) from CLASSES1:sch_1(A9); A12: rng (h ") = dom f by A1, A3, FUNCT_1:33; A13: F is one-to-one proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y ) assume that A14: x in dom F and A15: y in dom F and A16: F . x = F . y ; ::_thesis: x = y consider g2 being Function such that A17: y = g2 and A18: F . y = g2 * (h ") by A11, A15; A19: dom g2 = dom f by A6, A11, A15, A17, CARD_3:9; consider g1 being Function such that A20: x = g1 and A21: F . x = g1 * (h ") by A11, A14; dom g1 = dom f by A6, A11, A14, A20, CARD_3:9; hence x = y by A12, A16, A20, A21, A17, A18, A19, FUNCT_1:86; ::_thesis: verum end; A22: ( (g * h) * (h ") = g * (h * (h ")) & g * (id (dom g)) = g ) by RELAT_1:36, RELAT_1:52; A23: product g c= rng F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product g or x in rng F ) assume x in product g ; ::_thesis: x in rng F then consider f1 being Function such that A24: x = f1 and A25: dom f1 = dom g and A26: for z being set st z in dom g holds f1 . z in g . z by CARD_3:def_5; A27: dom (f1 * h) = dom f by A1, A2, A25, RELAT_1:27; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ (f1_*_h)_._z_in_(g_*_h)_._z let z be set ; ::_thesis: ( z in dom f implies (f1 * h) . z in (g * h) . z ) assume A28: z in dom f ; ::_thesis: (f1 * h) . z in (g * h) . z then A29: h . z in dom g by A1, A2, FUNCT_1:def_3; A30: (h ") . (h . z) = z by A1, A3, A28, FUNCT_1:34; (f1 * h) . z = f1 . (h . z) by A27, A28, FUNCT_1:12; then (f1 * h) . z in ((g * h) * (h ")) . (h . z) by A5, A22, A26, A29; hence (f1 * h) . z in (g * h) . z by A5, A22, A29, A30, FUNCT_1:12; ::_thesis: verum end; then A31: f1 * h in product (g * h) by A6, A27, CARD_3:def_5; then ex f2 being Function st ( f1 * h = f2 & F . (f1 * h) = f2 * (h ") ) by A11; then F . (f1 * h) = f1 * (id (dom g)) by A5, RELAT_1:36 .= x by A24, A25, RELAT_1:51 ; hence x in rng F by A11, A31, FUNCT_1:def_3; ::_thesis: verum end; A32: dom (h ") = rng h by A3, FUNCT_1:33; rng F c= product g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in product g ) assume x in rng F ; ::_thesis: x in product g then consider y being set such that A33: y in dom F and A34: x = F . y by FUNCT_1:def_3; consider f1 being Function such that A35: y = f1 and A36: dom f1 = dom f and A37: for z being set st z in dom f holds f1 . z in (g * h) . z by A6, A11, A33, CARD_3:def_5; A38: dom (f1 * (h ")) = dom g by A2, A12, A32, A36, RELAT_1:27; A39: now__::_thesis:_for_z_being_set_st_z_in_dom_g_holds_ (f1_*_(h_"))_._z_in_g_._z let z be set ; ::_thesis: ( z in dom g implies (f1 * (h ")) . z in g . z ) assume A40: z in dom g ; ::_thesis: (f1 * (h ")) . z in g . z then A41: (h ") . z in dom f by A2, A12, A32, FUNCT_1:def_3; ( g . z = (g * h) . ((h ") . z) & (f1 * (h ")) . z = f1 . ((h ") . z) ) by A5, A22, A38, A40, FUNCT_1:12; hence (f1 * (h ")) . z in g . z by A37, A41; ::_thesis: verum end; ex f1 being Function st ( y = f1 & F . y = f1 * (h ") ) by A11, A33; hence x in product g by A34, A35, A38, A39, CARD_3:def_5; ::_thesis: verum end; then rng F = product g by A23, XBOOLE_0:def_10; then product (g * h), product g are_equipotent by A11, A13, WELLORD2:def_4; hence product f, product g are_equipotent by A8, WELLORD2:15; ::_thesis: verum end; theorem :: FUNCT_6:45 for X being set for f being Function for P being Permutation of X st dom f = X holds product f, product (f * P) are_equipotent proof let X be set ; ::_thesis: for f being Function for P being Permutation of X st dom f = X holds product f, product (f * P) are_equipotent let f be Function; ::_thesis: for P being Permutation of X st dom f = X holds product f, product (f * P) are_equipotent let P be Permutation of X; ::_thesis: ( dom f = X implies product f, product (f * P) are_equipotent ) assume A1: dom f = X ; ::_thesis: product f, product (f * P) are_equipotent A2: rng P = X by FUNCT_2:def_3; dom P = X by FUNCT_2:52; then A3: dom (f * P) = X by A1, A2, RELAT_1:27; A4: rng (P ") = X by FUNCT_2:def_3; A5: dom (P ") = X by FUNCT_2:52; now__::_thesis:_for_x_being_set_st_x_in_dom_(P_")_holds_ f_._x,(f_*_P)_._((P_")_._x)_are_equipotent let x be set ; ::_thesis: ( x in dom (P ") implies f . x,(f * P) . ((P ") . x) are_equipotent ) assume A6: x in dom (P ") ; ::_thesis: f . x,(f * P) . ((P ") . x) are_equipotent then (P ") . x in X by A4, FUNCT_1:def_3; then (f * P) . ((P ") . x) = f . (P . ((P ") . x)) by A3, FUNCT_1:12 .= f . x by A5, A2, A6, FUNCT_1:35 ; hence f . x,(f * P) . ((P ") . x) are_equipotent ; ::_thesis: verum end; hence product f, product (f * P) are_equipotent by A1, A5, A4, A3, Th44; ::_thesis: verum end; begin definition let f be Function; let X be set ; func Funcs (f,X) -> Function means :Def8: :: FUNCT_6:def 8 ( dom it = dom f & ( for x being set st x in dom f holds it . x = Funcs ((f . x),X) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs ((f . x),X) ) ) proof deffunc H1( set ) -> set = Funcs ((f . \$1),X); ex F being Function st ( dom F = dom f & ( for x being set st x in dom f holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs ((f . x),X) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs ((f . x),X) ) & dom b2 = dom f & ( for x being set st x in dom f holds b2 . x = Funcs ((f . x),X) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = dom f & ( for x being set st x in dom f holds f1 . x = Funcs ((f . x),X) ) & dom f2 = dom f & ( for x being set st x in dom f holds f2 . x = Funcs ((f . x),X) ) implies f1 = f2 ) assume that A1: dom f1 = dom f and A2: for x being set st x in dom f holds f1 . x = Funcs ((f . x),X) and A3: dom f2 = dom f and A4: for x being set st x in dom f holds f2 . x = Funcs ((f . x),X) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f implies f1 . x = f2 . x ) assume A5: x in dom f ; ::_thesis: f1 . x = f2 . x then f1 . x = Funcs ((f . x),X) by A2; hence f1 . x = f2 . x by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def8 defines Funcs FUNCT_6:def_8_:_ for f being Function for X being set for b3 being Function holds ( b3 = Funcs (f,X) iff ( dom b3 = dom f & ( for x being set st x in dom f holds b3 . x = Funcs ((f . x),X) ) ) ); theorem :: FUNCT_6:46 for f being Function st not {} in rng f holds Funcs (f,{}) = (dom f) --> {} proof let f be Function; ::_thesis: ( not {} in rng f implies Funcs (f,{}) = (dom f) --> {} ) assume A1: not {} in rng f ; ::_thesis: Funcs (f,{}) = (dom f) --> {} A2: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ ((dom_f)_-->_{})_._x_=_Funcs_((f_._x),{}) let x be set ; ::_thesis: ( x in dom f implies ((dom f) --> {}) . x = Funcs ((f . x),{}) ) assume A3: x in dom f ; ::_thesis: ((dom f) --> {}) . x = Funcs ((f . x),{}) then A4: f . x <> {} by A1, FUNCT_1:def_3; thus ((dom f) --> {}) . x = {} by A3, FUNCOP_1:7 .= Funcs ((f . x),{}) by A4 ; ::_thesis: verum end; dom ((dom f) --> {}) = dom f by FUNCOP_1:13; hence Funcs (f,{}) = (dom f) --> {} by A2, Def8; ::_thesis: verum end; theorem :: FUNCT_6:47 for X being set holds Funcs ({},X) = {} proof let X be set ; ::_thesis: Funcs ({},X) = {} dom (Funcs ({},X)) = dom {} by Def8; hence Funcs ({},X) = {} ; ::_thesis: verum end; theorem :: FUNCT_6:48 for X, Y, Z being set holds Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) proof let X, Y, Z be set ; ::_thesis: Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) A1: X = dom (X --> Y) by FUNCOP_1:13; A2: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (Funcs_((X_-->_Y),Z))_._x_=_Funcs_(Y,Z) let x be set ; ::_thesis: ( x in X implies (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) ) assume A3: x in X ; ::_thesis: (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) then (Funcs ((X --> Y),Z)) . x = Funcs (((X --> Y) . x),Z) by A1, Def8; hence (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) by A3, FUNCOP_1:7; ::_thesis: verum end; dom (Funcs ((X --> Y),Z)) = dom (X --> Y) by Def8; hence Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) by A1, A2, FUNCOP_1:11; ::_thesis: verum end; Lm4: for x, y, z being set for f, g being Function st [x,y] in dom f & g = (curry f) . x & z in dom g holds [x,z] in dom f proof let x, y, z be set ; ::_thesis: for f, g being Function st [x,y] in dom f & g = (curry f) . x & z in dom g holds [x,z] in dom f let f, g be Function; ::_thesis: ( [x,y] in dom f & g = (curry f) . x & z in dom g implies [x,z] in dom f ) assume [x,y] in dom f ; ::_thesis: ( not g = (curry f) . x or not z in dom g or [x,z] in dom f ) then x in proj1 (dom f) by XTUPLE_0:def_12; then A1: ex g9 being Function st ( (curry f) . x = g9 & dom g9 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g9 holds g9 . y = f . (x,y) ) ) by FUNCT_5:def_1; assume ( g = (curry f) . x & z in dom g ) ; ::_thesis: [x,z] in dom f then consider y being set such that A2: [y,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, XTUPLE_0:def_13; [y,z] in [:{x},(proj2 (dom f)):] by A2, XBOOLE_0:def_4; then A3: y in {x} by ZFMISC_1:87; [y,z] in dom f by A2, XBOOLE_0:def_4; hence [x,z] in dom f by A3, TARSKI:def_1; ::_thesis: verum end; theorem :: FUNCT_6:49 for X being set for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent proof let X be set ; ::_thesis: for f being Function holds Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent let f be Function; ::_thesis: Funcs ((Union (disjoin f)),X), product (Funcs (f,X)) are_equipotent defpred S1[ set , set ] means ex g, h being Function st ( \$1 = g & \$2 = h & dom h = dom f & ( for y being set st y in dom f holds ( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) ) ); A1: for x being set st x in Funcs ((Union (disjoin f)),X) holds ex z being set st S1[x,z] proof defpred S2[ set ] means f . \$1 = {} ; deffunc H1( set ) -> set = {} ; let x be set ; ::_thesis: ( x in Funcs ((Union (disjoin f)),X) implies ex z being set st S1[x,z] ) assume x in Funcs ((Union (disjoin f)),X) ; ::_thesis: ex z being set st S1[x,z] then consider g being Function such that A2: x = g and dom g = Union (disjoin f) and rng g c= X by FUNCT_2:def_2; deffunc H2( set ) -> set = (curry' g) . \$1; ex h being Function st ( dom h = dom f & ( for y being set st y in dom f holds ( ( S2[y] implies h . y = H1(y) ) & ( not S2[y] implies h . y = H2(y) ) ) ) ) from PARTFUN1:sch_1(); hence ex z being set st S1[x,z] by A2; ::_thesis: verum end; consider F being Function such that A3: ( dom F = Funcs ((Union (disjoin f)),X) & ( for x being set st x in Funcs ((Union (disjoin f)),X) holds S1[x,F . x] ) ) from CLASSES1:sch_1(A1); take F ; :: according to WELLORD2:def_4 ::_thesis: ( F is one-to-one & dom F = Funcs ((Union (disjoin f)),X) & rng F = product (Funcs (f,X)) ) thus F is one-to-one ::_thesis: ( dom F = Funcs ((Union (disjoin f)),X) & rng F = product (Funcs (f,X)) ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y ) assume that A4: x in dom F and A5: y in dom F and A6: F . x = F . y ; ::_thesis: x = y A7: ex f2 being Function st ( y = f2 & dom f2 = Union (disjoin f) & rng f2 c= X ) by A3, A5, FUNCT_2:def_2; consider g1, h1 being Function such that A8: x = g1 and A9: F . x = h1 and dom h1 = dom f and A10: for y being set st y in dom f holds ( ( f . y = {} implies h1 . y = {} ) & ( f . y <> {} implies h1 . y = (curry' g1) . y ) ) by A3, A4; consider g2, h2 being Function such that A11: y = g2 and A12: F . y = h2 and dom h2 = dom f and A13: for y being set st y in dom f holds ( ( f . y = {} implies h2 . y = {} ) & ( f . y <> {} implies h2 . y = (curry' g2) . y ) ) by A3, A5; A14: ex f1 being Function st ( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A4, FUNCT_2:def_2; now__::_thesis:_for_z_being_set_st_z_in_Union_(disjoin_f)_holds_ g1_._z_=_g2_._z let z be set ; ::_thesis: ( z in Union (disjoin f) implies g1 . z = g2 . z ) assume A15: z in Union (disjoin f) ; ::_thesis: g1 . z = g2 . z then A16: z = [(z `1),(z `2)] by CARD_3:22; A17: ( z `2 in dom f & z `1 in f . (z `2) ) by A15, CARD_3:22; then A18: h2 . (z `2) = (curry' g2) . (z `2) by A13; then reconsider g91 = h1 . (z `2), g92 = h2 . (z `2) as Function by A6, A7, A9, A11, A12, A15, A16, FUNCT_5:21; A19: g2 . ((z `1),(z `2)) = g92 . (z `1) by A7, A11, A15, A16, A18, FUNCT_5:22; h1 . (z `2) = (curry' g1) . (z `2) by A10, A17; then g1 . ((z `1),(z `2)) = g91 . (z `1) by A14, A8, A15, A16, FUNCT_5:22; hence g1 . z = g2 . z by A6, A9, A12, A16, A19; ::_thesis: verum end; hence x = y by A14, A7, A8, A11, FUNCT_1:2; ::_thesis: verum end; thus dom F = Funcs ((Union (disjoin f)),X) by A3; ::_thesis: rng F = product (Funcs (f,X)) thus rng F c= product (Funcs (f,X)) :: according to XBOOLE_0:def_10 ::_thesis: product (Funcs (f,X)) c= rng F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in product (Funcs (f,X)) ) assume y in rng F ; ::_thesis: y in product (Funcs (f,X)) then consider x being set such that A20: x in dom F and A21: y = F . x by FUNCT_1:def_3; consider g, h being Function such that A22: x = g and A23: F . x = h and A24: dom h = dom f and A25: for y being set st y in dom f holds ( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3, A20; A26: ex f1 being Function st ( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A20, FUNCT_2:def_2; A27: now__::_thesis:_for_z_being_set_st_z_in_dom_(Funcs_(f,X))_holds_ h_._z_in_(Funcs_(f,X))_._z let z be set ; ::_thesis: ( z in dom (Funcs (f,X)) implies h . z in (Funcs (f,X)) . z ) assume z in dom (Funcs (f,X)) ; ::_thesis: h . z in (Funcs (f,X)) . z then A28: z in dom f by Def8; then A29: (Funcs (f,X)) . z = Funcs ((f . z),X) by Def8; A30: now__::_thesis:_(_f_._z_<>_{}_implies_h_._z_in_(Funcs_(f,X))_._z_) set a = the Element of f . z; assume A31: f . z <> {} ; ::_thesis: h . z in (Funcs (f,X)) . z ( [ the Element of f . z,z] `1 = the Element of f . z & [ the Element of f . z,z] `2 = z ) ; then A32: [ the Element of f . z,z] in Union (disjoin f) by A28, A31, CARD_3:22; then reconsider k = (curry' g) . z as Function by A22, A26, FUNCT_5:21; A33: z in dom (curry' g) by A22, A26, A32, FUNCT_5:21; then rng k c= rng g by FUNCT_5:34; then A34: rng k c= X by A22, A26, XBOOLE_1:1; A35: dom k = proj1 ((dom g) /\ [:(proj1 (dom g)),{z}:]) by A33, FUNCT_5:34; A36: dom k = f . z proof thus dom k c= f . z :: according to XBOOLE_0:def_10 ::_thesis: f . z c= dom k proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom k or b in f . z ) assume b in dom k ; ::_thesis: b in f . z then consider c being set such that A37: [b,c] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A35, XTUPLE_0:def_12; [b,c] in [:(proj1 (dom g)),{z}:] by A37, XBOOLE_0:def_4; then A38: c in {z} by ZFMISC_1:87; A39: ( [b,c] `1 = b & [b,c] `2 = c ) ; [b,c] in dom g by A37, XBOOLE_0:def_4; then b in f . c by A22, A26, A39, CARD_3:22; hence b in f . z by A38, TARSKI:def_1; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in f . z or b in dom k ) assume A40: b in f . z ; ::_thesis: b in dom k A41: z in {z} by TARSKI:def_1; ( [b,z] `1 = b & [b,z] `2 = z ) ; then A42: [b,z] in dom g by A22, A26, A28, A40, CARD_3:22; then b in proj1 (dom g) by XTUPLE_0:def_12; then [b,z] in [:(proj1 (dom g)),{z}:] by A41, ZFMISC_1:87; then [b,z] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A42, XBOOLE_0:def_4; hence b in dom k by A35, XTUPLE_0:def_12; ::_thesis: verum end; h . z = k by A25, A28, A31; hence h . z in (Funcs (f,X)) . z by A29, A34, A36, FUNCT_2:def_2; ::_thesis: verum end; now__::_thesis:_(_f_._z_=_{}_implies_h_._z_in_(Funcs_(f,X))_._z_) assume f . z = {} ; ::_thesis: h . z in (Funcs (f,X)) . z then ( h . z = {} & (Funcs (f,X)) . z = {{}} ) by A25, A28, A29, FUNCT_5:57; hence h . z in (Funcs (f,X)) . z by TARSKI:def_1; ::_thesis: verum end; hence h . z in (Funcs (f,X)) . z by A30; ::_thesis: verum end; dom h = dom (Funcs (f,X)) by A24, Def8; hence y in product (Funcs (f,X)) by A21, A23, A27, CARD_3:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Funcs (f,X)) or x in rng F ) assume x in product (Funcs (f,X)) ; ::_thesis: x in rng F then consider s being Function such that A43: x = s and A44: dom s = dom (Funcs (f,X)) and A45: for z being set st z in dom (Funcs (f,X)) holds s . z in (Funcs (f,X)) . z by CARD_3:def_5; A46: dom s = dom f by A44, Def8; A47: uncurry' s = ~ (uncurry s) by FUNCT_5:def_4; A48: dom (uncurry' s) = Union (disjoin f) proof thus dom (uncurry' s) c= Union (disjoin f) :: according to XBOOLE_0:def_10 ::_thesis: Union (disjoin f) c= dom (uncurry' s) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom (uncurry' s) or z in Union (disjoin f) ) assume A49: z in dom (uncurry' s) ; ::_thesis: z in Union (disjoin f) then consider z1, z2 being set such that A50: z = [z1,z2] by A47, Th2; A51: ( z `1 = z1 & z `2 = z2 ) by A50, MCART_1:7; [z2,z1] in dom (uncurry s) by A47, A49, A50, FUNCT_4:42; then consider a being set , u being Function, b being set such that A52: [z2,z1] = [a,b] and A53: a in dom s and A54: u = s . a and A55: b in dom u by FUNCT_5:def_2; A56: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) ; ( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A53, A54, Def8; then A57: ex j being Function st ( u = j & dom j = f . z2 & rng j c= X ) by A52, A56, FUNCT_2:def_2; ( [a,b] `2 = b & [z2,z1] `2 = z1 ) ; hence z in Union (disjoin f) by A46, A50, A52, A53, A55, A51, A56, A57, CARD_3:22; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Union (disjoin f) or z in dom (uncurry' s) ) assume A58: z in Union (disjoin f) ; ::_thesis: z in dom (uncurry' s) then A59: ( z `1 in f . (z `2) & z = [(z `1),(z `2)] ) by CARD_3:22; A60: z `2 in dom f by A58, CARD_3:22; then ( s . (z `2) in (Funcs (f,X)) . (z `2) & (Funcs (f,X)) . (z `2) = Funcs ((f . (z `2)),X) ) by A44, A45, A46, Def8; then ex j being Function st ( s . (z `2) = j & dom j = f . (z `2) & rng j c= X ) by FUNCT_2:def_2; hence z in dom (uncurry' s) by A46, A60, A59, FUNCT_5:39; ::_thesis: verum end; rng (uncurry' s) c= X proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in rng (uncurry' s) or d in X ) assume d in rng (uncurry' s) ; ::_thesis: d in X then consider z being set such that A61: z in dom (uncurry' s) and A62: d = (uncurry' s) . z by FUNCT_1:def_3; consider z1, z2 being set such that A63: z = [z1,z2] by A47, A61, Th2; [z2,z1] in dom (uncurry s) by A47, A61, A63, FUNCT_4:42; then consider a being set , u being Function, b being set such that A64: [z2,z1] = [a,b] and A65: ( a in dom s & u = s . a ) and A66: b in dom u by FUNCT_5:def_2; A67: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) ; ( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A65, Def8; then A68: ex j being Function st ( u = j & dom j = f . z2 & rng j c= X ) by A64, A67, FUNCT_2:def_2; A69: ( [a,b] `2 = b & [z2,z1] `2 = z1 ) ; (uncurry' s) . (b,a) = u . b by A65, A66, FUNCT_5:39; then d in rng u by A62, A63, A64, A66, A67, A69, FUNCT_1:def_3; hence d in X by A68; ::_thesis: verum end; then A70: uncurry' s in dom F by A3, A48, FUNCT_2:def_2; then consider g, h being Function such that A71: uncurry' s = g and A72: F . (uncurry' s) = h and A73: dom h = dom f and A74: for y being set st y in dom f holds ( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ s_._z_=_h_._z let z be set ; ::_thesis: ( z in dom f implies s . z = h . z ) assume A75: z in dom f ; ::_thesis: s . z = h . z then ( s . z in (Funcs (f,X)) . z & (Funcs (f,X)) . z = Funcs ((f . z),X) ) by A44, A45, A46, Def8; then consider v being Function such that A76: s . z = v and A77: dom v = f . z and rng v c= X by FUNCT_2:def_2; A78: now__::_thesis:_(_f_._z_<>_{}_implies_s_._z_=_h_._z_) set a = the Element of f . z; assume A79: f . z <> {} ; ::_thesis: s . z = h . z then A80: [ the Element of f . z,z] in dom (uncurry' s) by A46, A75, A76, A77, FUNCT_5:39; then reconsider j = (curry' (uncurry' s)) . z as Function by FUNCT_5:21; A81: j = (curry (~ (uncurry' s))) . z by FUNCT_5:def_3; A82: ~ (uncurry' s) = uncurry s by Th4; then A83: [z, the Element of f . z] in dom (uncurry s) by A80, FUNCT_4:42; A84: dom j = dom v proof thus dom j c= dom v :: according to XBOOLE_0:def_10 ::_thesis: dom v c= dom j proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom j or b in dom v ) assume b in dom j ; ::_thesis: b in dom v then [z,b] in dom (uncurry s) by A81, A82, A83, Lm4; then consider a1 being set , g1 being Function, a2 being set such that A85: [z,b] = [a1,a2] and a1 in dom s and A86: ( g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def_2; z = a1 by A85, XTUPLE_0:1; hence b in dom v by A76, A85, A86, XTUPLE_0:1; ::_thesis: verum end; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in dom v or b in dom j ) assume b in dom v ; ::_thesis: b in dom j then [z,b] in dom (uncurry s) by A46, A75, A76, FUNCT_5:38; hence b in dom j by A81, A82, FUNCT_5:20; ::_thesis: verum end; now__::_thesis:_for_b_being_set_st_b_in_f_._z_holds_ j_._b_=_v_._b let b be set ; ::_thesis: ( b in f . z implies j . b = v . b ) assume b in f . z ; ::_thesis: j . b = v . b then A87: [z,b] in dom (uncurry s) by A77, A81, A82, A83, A84, Lm4; then consider a1 being set , g1 being Function, a2 being set such that A88: [z,b] = [a1,a2] and A89: ( a1 in dom s & g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def_2; A90: j . b = (uncurry s) . (z,b) by A81, A82, A87, FUNCT_5:20; ( z = a1 & b = a2 ) by A88, XTUPLE_0:1; hence j . b = v . b by A76, A89, A90, FUNCT_5:38; ::_thesis: verum end; then v = j by A77, A84, FUNCT_1:2; hence s . z = h . z by A71, A74, A75, A76, A79; ::_thesis: verum end; ( f . z = {} implies ( s . z = {} & h . z = {} ) ) by A74, A75, A76, A77; hence s . z = h . z by A78; ::_thesis: verum end; then h = s by A46, A73, FUNCT_1:2; hence x in rng F by A43, A70, A72, FUNCT_1:def_3; ::_thesis: verum end; definition let X be set ; let f be Function; func Funcs (X,f) -> Function means :Def9: :: FUNCT_6:def 9 ( dom it = dom f & ( for x being set st x in dom f holds it . x = Funcs (X,(f . x)) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs (X,(f . x)) ) ) proof deffunc H1( set ) -> set = Funcs (X,(f . \$1)); ex F being Function st ( dom F = dom f & ( for x being set st x in dom f holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs (X,(f . x)) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = Funcs (X,(f . x)) ) & dom b2 = dom f & ( for x being set st x in dom f holds b2 . x = Funcs (X,(f . x)) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = dom f & ( for x being set st x in dom f holds f1 . x = Funcs (X,(f . x)) ) & dom f2 = dom f & ( for x being set st x in dom f holds f2 . x = Funcs (X,(f . x)) ) implies f1 = f2 ) assume that A1: dom f1 = dom f and A2: for x being set st x in dom f holds f1 . x = Funcs (X,(f . x)) and A3: dom f2 = dom f and A4: for x being set st x in dom f holds f2 . x = Funcs (X,(f . x)) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f implies f1 . x = f2 . x ) assume A5: x in dom f ; ::_thesis: f1 . x = f2 . x then f1 . x = Funcs (X,(f . x)) by A2; hence f1 . x = f2 . x by A4, A5; ::_thesis: verum end; hence f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def9 defines Funcs FUNCT_6:def_9_:_ for X being set for f, b3 being Function holds ( b3 = Funcs (X,f) iff ( dom b3 = dom f & ( for x being set st x in dom f holds b3 . x = Funcs (X,(f . x)) ) ) ); Lm5: for X being set for f being Function st f <> {} & X <> {} holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent proof let X be set ; ::_thesis: for f being Function st f <> {} & X <> {} holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent let f be Function; ::_thesis: ( f <> {} & X <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent ) defpred S1[ set , set ] means ex g being Function st ( \$1 = g & \$2 = <:g:> ); assume that A1: f <> {} and A2: X <> {} ; ::_thesis: product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent A3: for x being set st x in product (Funcs (X,f)) holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in product (Funcs (X,f)) implies ex y being set st S1[x,y] ) assume x in product (Funcs (X,f)) ; ::_thesis: ex y being set st S1[x,y] then ex g being Function st ( x = g & dom g = dom (Funcs (X,f)) & ( for x being set st x in dom (Funcs (X,f)) holds g . x in (Funcs (X,f)) . x ) ) by CARD_3:def_5; then reconsider g = x as Function ; reconsider y = <:g:> as set ; take y ; ::_thesis: S1[x,y] take g ; ::_thesis: ( x = g & y = <:g:> ) thus ( x = g & y = <:g:> ) ; ::_thesis: verum end; consider F being Function such that A4: ( dom F = product (Funcs (X,f)) & ( for x being set st x in product (Funcs (X,f)) holds S1[x,F . x] ) ) from CLASSES1:sch_1(A3); take F ; :: according to WELLORD2:def_4 ::_thesis: ( F is one-to-one & dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) ) A5: for g being Function st g in product (Funcs (X,f)) holds ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f ) proof let g be Function; ::_thesis: ( g in product (Funcs (X,f)) implies ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f ) ) A6: g " (rng g) = dom g by RELAT_1:134; A7: dom (Funcs (X,f)) = dom f by Def9; assume A8: g in product (Funcs (X,f)) ; ::_thesis: ( dom <:g:> = X & SubFuncs (rng g) = rng g & rng <:g:> c= product f ) then A9: dom g = dom (Funcs (X,f)) by CARD_3:9; A10: now__::_thesis:_for_a_being_set_st_a_in_rng_g_holds_ a_is_Function let a be set ; ::_thesis: ( a in rng g implies a is Function ) assume a in rng g ; ::_thesis: a is Function then consider z being set such that A11: z in dom g and A12: a = g . z by FUNCT_1:def_3; ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A9, A7, A11, Def9, CARD_3:9; hence a is Function by A12; ::_thesis: verum end; then A13: SubFuncs (rng g) = rng g by Lm1; A14: now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ ((dom_f)_-->_X)_._z_=_proj1_(g_._z) let z be set ; ::_thesis: ( z in dom f implies ((dom f) --> X) . z = proj1 (g . z) ) assume A15: z in dom f ; ::_thesis: ((dom f) --> X) . z = proj1 (g . z) then ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A7, Def9, CARD_3:9; then ex h being Function st ( g . z = h & dom h = X & rng h c= f . z ) by FUNCT_2:def_2; hence ((dom f) --> X) . z = proj1 (g . z) by A15, FUNCOP_1:7; ::_thesis: verum end; dom ((dom f) --> X) = dom f by FUNCOP_1:13; then doms g = (dom f) --> X by A9, A7, A13, A6, A14, Def2; then meet (doms g) = X by A1, Th27; hence A16: ( dom <:g:> = X & SubFuncs (rng g) = rng g ) by A10, Lm1, Th29; ::_thesis: rng <:g:> c= product f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng <:g:> or y in product f ) assume y in rng <:g:> ; ::_thesis: y in product f then consider x being set such that A17: x in dom <:g:> and A18: y = <:g:> . x by FUNCT_1:def_3; reconsider h = y as Function by A17, A18, Th30; A19: dom h = dom f by A9, A7, A13, A6, A17, A18, Th31; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ h_._z_in_f_._z let z be set ; ::_thesis: ( z in dom f implies h . z in f . z ) assume A20: z in dom f ; ::_thesis: h . z in f . z then A21: (uncurry g) . (z,x) = h . z by A17, A18, A19, Th31; ( g . z in (Funcs (X,f)) . z & (Funcs (X,f)) . z = Funcs (X,(f . z)) ) by A8, A7, A20, Def9, CARD_3:9; then consider j being Function such that A22: g . z = j and A23: dom j = X and A24: rng j c= f . z by FUNCT_2:def_2; A25: j . x in rng j by A16, A17, A23, FUNCT_1:def_3; (uncurry g) . (z,x) = j . x by A9, A7, A16, A17, A20, A22, A23, FUNCT_5:38; hence h . z in f . z by A24, A21, A25; ::_thesis: verum end; hence y in product f by A19, CARD_3:def_5; ::_thesis: verum end; thus F is one-to-one ::_thesis: ( dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom F or not b1 in dom F or not F . x = F . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom F or not y in dom F or not F . x = F . y or x = y ) assume that A26: x in dom F and A27: y in dom F and A28: F . x = F . y and A29: x <> y ; ::_thesis: contradiction consider gy being Function such that A30: y = gy and A31: F . y = <:gy:> by A4, A27; consider gx being Function such that A32: x = gx and A33: F . x = <:gx:> by A4, A26; A34: dom gx = dom (Funcs (X,f)) by A4, A26, A32, CARD_3:9; A35: dom (Funcs (X,f)) = dom f by Def9; A36: dom gy = dom (Funcs (X,f)) by A4, A27, A30, CARD_3:9; now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ gx_._z_=_gy_._z let z be set ; ::_thesis: ( z in dom f implies gx . z = gy . z ) assume A37: z in dom f ; ::_thesis: gx . z = gy . z then A38: (Funcs (X,f)) . z = Funcs (X,(f . z)) by Def9; gy . z in (Funcs (X,f)) . z by A4, A27, A30, A35, A37, CARD_3:9; then consider hy being Function such that A39: ( gy . z = hy & dom hy = X ) and rng hy c= f . z by A38, FUNCT_2:def_2; gx . z in (Funcs (X,f)) . z by A4, A26, A32, A35, A37, CARD_3:9; then consider hx being Function such that A40: ( gx . z = hx & dom hx = X ) and rng hx c= f . z by A38, FUNCT_2:def_2; A41: dom <:gx:> = X by A4, A5, A26, A32; A42: ( SubFuncs (rng gx) = rng gx & gx " (rng gx) = dom gx ) by A4, A5, A26, A32, RELAT_1:134; now__::_thesis:_for_b_being_set_st_b_in_X_holds_ hx_._b_=_hy_._b let b be set ; ::_thesis: ( b in X implies hx . b = hy . b ) assume A43: b in X ; ::_thesis: hx . b = hy . b then reconsider fx = <:gx:> . b as Function by A41, Th30; A44: ( (uncurry gx) . (z,b) = hx . b & (uncurry gy) . (z,b) = hy . b ) by A34, A36, A35, A37, A40, A39, A43, FUNCT_5:38; A45: dom fx = dom gx by A41, A42, A43, Th31; then fx . z = (uncurry gx) . (z,b) by A34, A35, A37, A41, A43, Th31; hence hx . b = hy . b by A28, A33, A31, A34, A35, A37, A41, A43, A45, A44, Th31; ::_thesis: verum end; hence gx . z = gy . z by A40, A39, FUNCT_1:2; ::_thesis: verum end; hence contradiction by A29, A32, A30, A34, A36, A35, FUNCT_1:2; ::_thesis: verum end; thus dom F = product (Funcs (X,f)) by A4; ::_thesis: rng F = Funcs (X,(product f)) thus rng F c= Funcs (X,(product f)) :: according to XBOOLE_0:def_10 ::_thesis: Funcs (X,(product f)) c= rng F proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in Funcs (X,(product f)) ) assume y in rng F ; ::_thesis: y in Funcs (X,(product f)) then consider x being set such that A46: x in dom F and A47: y = F . x by FUNCT_1:def_3; consider g being Function such that A48: x = g and A49: y = <:g:> by A4, A46, A47; ( dom <:g:> = X & rng <:g:> c= product f ) by A4, A5, A46, A48; hence y in Funcs (X,(product f)) by A49, FUNCT_2:def_2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Funcs (X,(product f)) or y in rng F ) assume y in Funcs (X,(product f)) ; ::_thesis: y in rng F then consider h being Function such that A50: y = h and A51: dom h = X and A52: rng h c= product f by FUNCT_2:def_2; set g = <:h:>; A53: h " (rng h) = dom h by RELAT_1:134; A54: now__::_thesis:_for_z_being_set_st_z_in_X_holds_ (X_-->_(dom_f))_._z_=_(doms_h)_._z let z be set ; ::_thesis: ( z in X implies (X --> (dom f)) . z = (doms h) . z ) assume A55: z in X ; ::_thesis: (X --> (dom f)) . z = (doms h) . z then h . z in rng h by A51, FUNCT_1:def_3; then A56: ex j being Function st ( h . z = j & dom j = dom f & ( for x being set st x in dom f holds j . x in f . x ) ) by A52, CARD_3:def_5; thus (X --> (dom f)) . z = dom f by A55, FUNCOP_1:7 .= (doms h) . z by A51, A55, A56, Th22 ; ::_thesis: verum end; A57: meet (doms h) = dom <:h:> by Th29; now__::_thesis:_for_z_being_set_st_z_in_rng_h_holds_ z_is_Function let z be set ; ::_thesis: ( z in rng h implies z is Function ) assume z in rng h ; ::_thesis: z is Function then ex j being Function st ( z = j & dom j = dom f & ( for x being set st x in dom f holds j . x in f . x ) ) by A52, CARD_3:def_5; hence z is Function ; ::_thesis: verum end; then A58: SubFuncs (rng h) = rng h by Lm1; ( dom (doms h) = h " (SubFuncs (rng h)) & dom ((dom h) --> (dom f)) = dom h ) by Def2, FUNCOP_1:13; then X --> (dom f) = doms h by A51, A58, A53, A54, FUNCT_1:2; then A59: dom <:h:> = dom f by A2, A57, Th27; A60: now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ <:h:>_._z_in_(Funcs_(X,f))_._z let z be set ; ::_thesis: ( z in dom f implies <:h:> . z in (Funcs (X,f)) . z ) assume A61: z in dom f ; ::_thesis: <:h:> . z in (Funcs (X,f)) . z then reconsider i = <:h:> . z as Function by A59, Th30; A62: dom i = X by A51, A58, A53, A59, A61, Th31; rng i c= f . z proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng i or x in f . z ) assume x in rng i ; ::_thesis: x in f . z then consider a being set such that A63: a in dom i and A64: x = i . a by FUNCT_1:def_3; h . a in rng h by A51, A62, A63, FUNCT_1:def_3; then consider j being Function such that A65: ( h . a = j & dom j = dom f ) and A66: for x being set st x in dom f holds j . x in f . x by A52, CARD_3:def_5; i . a = (uncurry h) . (a,z) by A59, A61, A63, Th31 .= j . z by A51, A61, A62, A63, A65, FUNCT_5:38 ; hence x in f . z by A61, A64, A66; ::_thesis: verum end; then <:h:> . z in Funcs (X,(f . z)) by A62, FUNCT_2:def_2; hence <:h:> . z in (Funcs (X,f)) . z by A61, Def9; ::_thesis: verum end; A67: meet (doms <:h:>) = dom <:<:h:>:> by Th29; product f c= Funcs ((dom f),(Union f)) by Th1; then A68: rng h c= Funcs ((dom f),(Union f)) by A52, XBOOLE_1:1; then A69: dom (uncurry h) = [:(dom h),(dom f):] by FUNCT_5:26; dom f = dom (Funcs (X,f)) by Def9; then A70: <:h:> in product (Funcs (X,f)) by A59, A60, CARD_3:def_5; then A71: ex g9 being Function st ( <:h:> = g9 & F . <:h:> = <:g9:> ) by A4; dom (uncurry' h) = [:(dom f),(dom h):] by A68, FUNCT_5:26; then A72: (uncurry' h) | [:(meet (doms h)),(dom h):] = uncurry' h by A57, A59, RELAT_1:68; A73: ( uncurry' h = ~ (uncurry h) & curry (~ (uncurry h)) = curry' (uncurry h) ) by FUNCT_5:def_3, FUNCT_5:def_4; dom <:<:h:>:> = X by A5, A70; then A74: (uncurry h) | [:(meet (doms <:h:>)),(dom <:h:>):] = uncurry h by A51, A59, A69, A67, RELAT_1:68; uncurry' (curry' (uncurry h)) = uncurry h by A69, FUNCT_5:49; then <:<:h:>:> = h by A1, A68, A72, A74, A73, FUNCT_5:48; hence y in rng F by A4, A50, A70, A71, FUNCT_1:def_3; ::_thesis: verum end; theorem Th50: :: FUNCT_6:50 for f being Function holds Funcs ({},f) = (dom f) --> {{}} proof let f be Function; ::_thesis: Funcs ({},f) = (dom f) --> {{}} A1: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (Funcs_({},f))_._x_=_{{}} let x be set ; ::_thesis: ( x in dom f implies (Funcs ({},f)) . x = {{}} ) assume x in dom f ; ::_thesis: (Funcs ({},f)) . x = {{}} hence (Funcs ({},f)) . x = Funcs ({},(f . x)) by Def9 .= {{}} by FUNCT_5:57 ; ::_thesis: verum end; dom (Funcs ({},f)) = dom f by Def9; hence Funcs ({},f) = (dom f) --> {{}} by A1, FUNCOP_1:11; ::_thesis: verum end; theorem Th51: :: FUNCT_6:51 for X being set holds Funcs (X,{}) = {} proof let X be set ; ::_thesis: Funcs (X,{}) = {} dom (Funcs (X,{})) = dom {} by Def9; hence Funcs (X,{}) = {} ; ::_thesis: verum end; theorem :: FUNCT_6:52 for X, Y, Z being set holds Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z)) proof let X, Y, Z be set ; ::_thesis: Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z)) A1: Y = dom (Y --> Z) by FUNCOP_1:13; A2: now__::_thesis:_for_x_being_set_st_x_in_Y_holds_ (Funcs_(X,(Y_-->_Z)))_._x_=_Funcs_(X,Z) let x be set ; ::_thesis: ( x in Y implies (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) ) assume A3: x in Y ; ::_thesis: (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) then (Funcs (X,(Y --> Z))) . x = Funcs (X,((Y --> Z) . x)) by A1, Def9; hence (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) by A3, FUNCOP_1:7; ::_thesis: verum end; dom (Funcs (X,(Y --> Z))) = dom (Y --> Z) by Def9; hence Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z)) by A1, A2, FUNCOP_1:11; ::_thesis: verum end; theorem :: FUNCT_6:53 for X being set for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent proof let X be set ; ::_thesis: for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent let f be Function; ::_thesis: product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent A1: Funcs (X,(product {})) = {(X --> {})} by CARD_3:10, FUNCT_5:59; A2: product (Funcs ({},f)) = product ((dom f) --> {{}}) by Th50 .= Funcs ((dom f),{{}}) by CARD_3:11 .= {((dom f) --> {})} by FUNCT_5:59 ; A3: ( Funcs ({},(product f)) = {{}} & product (Funcs (X,{})) = {{}} ) by Th51, CARD_3:10, FUNCT_5:57; ( X <> {} & f <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent ) by Lm5; hence product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent by A2, A3, A1, CARD_1:28; ::_thesis: verum end; begin definition let f be Function; func commute f -> Function-yielding Function equals :: FUNCT_6:def 10 curry' (uncurry f); coherence curry' (uncurry f) is Function-yielding Function proof set g = curry' (uncurry f); for x being set st x in dom (curry' (uncurry f)) holds (curry' (uncurry f)) . x is Function by FUNCT_5:33; hence curry' (uncurry f) is Function-yielding Function by FUNCOP_1:def_6; ::_thesis: verum end; end; :: deftheorem defines commute FUNCT_6:def_10_:_ for f being Function holds commute f = curry' (uncurry f); theorem :: FUNCT_6:54 for f being Function for x being set st x in dom (commute f) holds (commute f) . x is Function ; theorem Th55: :: FUNCT_6:55 for A, B, C being set for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds commute f in Funcs (B,(Funcs (A,C))) proof let A, B, C be set ; ::_thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds commute f in Funcs (B,(Funcs (A,C))) let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies commute f in Funcs (B,(Funcs (A,C))) ) assume ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) ) ; ::_thesis: commute f in Funcs (B,(Funcs (A,C))) then ( [:A,B:] <> {} & uncurry f in Funcs ([:A,B:],C) ) by Th11, ZFMISC_1:90; hence commute f in Funcs (B,(Funcs (A,C))) by Th10; ::_thesis: verum end; theorem :: FUNCT_6:56 for A, B, C being set for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds for g, h being Function for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) proof let A, B, C be set ; ::_thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds for g, h being Function for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies for g, h being Function for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) ) assume that A1: ( A <> {} & B <> {} ) and A2: f in Funcs (A,(Funcs (B,C))) ; ::_thesis: for g, h being Function for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) set uf = uncurry f; set cf = commute f; let g, h be Function; ::_thesis: for x, y being set st x in A & y in B & f . x = g & (commute f) . y = h holds ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) let x, y be set ; ::_thesis: ( x in A & y in B & f . x = g & (commute f) . y = h implies ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) ) assume that A3: x in A and A4: y in B and A5: f . x = g and A6: (commute f) . y = h ; ::_thesis: ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) commute f in Funcs (B,(Funcs (A,C))) by A1, A2, Th55; then A7: ex g being Function st ( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by FUNCT_2:def_2; then (commute f) . y in rng (commute f) by A4, FUNCT_1:def_3; then A8: ex t being Function st ( t = h & dom t = A & rng t c= C ) by A6, A7, FUNCT_2:def_2; A9: ex g being Function st ( g = f & dom g = A & rng g c= Funcs (B,C) ) by A2, FUNCT_2:def_2; then f . x in rng f by A3, FUNCT_1:def_3; then A10: ex t being Function st ( t = g & dom t = B & rng t c= C ) by A5, A9, FUNCT_2:def_2; then ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y ) by A3, A4, A5, A9, FUNCT_5:38; hence ( h . x = g . y & dom h = A & dom g = B & rng h c= C & rng g c= C ) by A6, A10, A8, FUNCT_5:22; ::_thesis: verum end; theorem :: FUNCT_6:57 for A, B, C being set for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds commute (commute f) = f proof let A, B, C be set ; ::_thesis: for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds commute (commute f) = f let f be Function; ::_thesis: ( A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) implies commute (commute f) = f ) assume that A1: ( A <> {} & B <> {} ) and A2: f in Funcs (A,(Funcs (B,C))) ; ::_thesis: commute (commute f) = f A3: ex g being Function st ( g = f & dom g = A & rng g c= Funcs (B,C) ) by A2, FUNCT_2:def_2; set cf = commute f; A4: commute f in Funcs (B,(Funcs (A,C))) by A1, A2, Th55; then commute (commute f) in Funcs (A,(Funcs (B,C))) by A1, Th55; then A5: ex h being Function st ( h = commute (commute f) & dom h = A & rng h c= Funcs (B,C) ) by FUNCT_2:def_2; A6: ex g being Function st ( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by A4, FUNCT_2:def_2; for x being set st x in A holds f . x = (commute (commute f)) . x proof set ccf = commute (commute f); set uf = uncurry f; set ucf = uncurry (commute f); let x be set ; ::_thesis: ( x in A implies f . x = (commute (commute f)) . x ) assume A7: x in A ; ::_thesis: f . x = (commute (commute f)) . x then f . x in rng f by A3, FUNCT_1:def_3; then consider g being Function such that A8: ( g = f . x & dom g = B ) and rng g c= C by A3, FUNCT_2:def_2; (commute (commute f)) . x in rng (commute (commute f)) by A5, A7, FUNCT_1:def_3; then consider h being Function such that A9: h = (commute (commute f)) . x and A10: dom h = B and rng h c= C by A5, FUNCT_2:def_2; A11: for y being set st y in B holds for h being Function st h = (commute f) . y holds ( x in dom h & h . x = g . y ) proof let y be set ; ::_thesis: ( y in B implies for h being Function st h = (commute f) . y holds ( x in dom h & h . x = g . y ) ) assume y in B ; ::_thesis: for h being Function st h = (commute f) . y holds ( x in dom h & h . x = g . y ) then A12: ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y ) by A3, A7, A8, FUNCT_5:38; let h be Function; ::_thesis: ( h = (commute f) . y implies ( x in dom h & h . x = g . y ) ) assume h = (commute f) . y ; ::_thesis: ( x in dom h & h . x = g . y ) hence ( x in dom h & h . x = g . y ) by A12, FUNCT_5:22; ::_thesis: verum end; A13: for y being set st y in B holds ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) proof let y be set ; ::_thesis: ( y in B implies ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) ) reconsider h = (commute f) . y as Function ; assume A14: y in B ; ::_thesis: ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) then ( x in dom h & h . x = g . y ) by A11; hence ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) by A6, A14, FUNCT_5:38; ::_thesis: verum end; for y being set st y in B holds h . y = g . y proof let y be set ; ::_thesis: ( y in B implies h . y = g . y ) assume y in B ; ::_thesis: h . y = g . y then ( [y,x] in dom (uncurry (commute f)) & (uncurry (commute f)) . (y,x) = g . y ) by A13; hence h . y = g . y by A9, FUNCT_5:22; ::_thesis: verum end; hence f . x = (commute (commute f)) . x by A8, A9, A10, FUNCT_1:2; ::_thesis: verum end; hence commute (commute f) = f by A3, A5, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_6:58 commute {} = {} by FUNCT_5:42, FUNCT_5:43; theorem :: FUNCT_6:59 for f being Function-yielding Function holds dom (doms f) = dom f proof let f be Function-yielding Function; ::_thesis: dom (doms f) = dom f thus dom (doms f) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (doms f) proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (doms f) or i in dom f ) dom (doms f) = f " (SubFuncs (rng f)) by Def2; hence ( not i in dom (doms f) or i in dom f ) by Th19; ::_thesis: verum end; thus dom f c= dom (doms f) ::_thesis: verum proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom f or i in dom (doms f) ) assume A1: i in dom f ; ::_thesis: i in dom (doms f) ( f . i is Function & dom (doms f) = f " (SubFuncs (rng f)) ) by Def2; hence i in dom (doms f) by A1, Th19; ::_thesis: verum end; end; theorem :: FUNCT_6:60 for f being Function-yielding Function holds dom (rngs f) = dom f proof let f be Function-yielding Function; ::_thesis: dom (rngs f) = dom f thus dom (rngs f) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (rngs f) proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom (rngs f) or i in dom f ) dom (rngs f) = f " (SubFuncs (rng f)) by Def3; hence ( not i in dom (rngs f) or i in dom f ) by Th19; ::_thesis: verum end; thus dom f c= dom (rngs f) ::_thesis: verum proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in dom f or i in dom (rngs f) ) assume A1: i in dom f ; ::_thesis: i in dom (rngs f) ( f . i is Function & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3; hence i in dom (rngs f) by A1, Th19; ::_thesis: verum end; end;