:: FUNCT_5 semantic presentation begin scheme :: FUNCT_5:sch 1 LambdaFS{ F1() -> set , F2( set ) -> set } : ex f being Function st ( dom f = F1() & ( for g being Function st g in F1() holds f . g = F2(g) ) ) proof consider f being Function such that A1: ( dom f = F1() & ( for x being set st x in F1() holds f . x = F2(x) ) ) from FUNCT_1:sch_3(); take f ; ::_thesis: ( dom f = F1() & ( for g being Function st g in F1() holds f . g = F2(g) ) ) thus ( dom f = F1() & ( for g being Function st g in F1() holds f . g = F2(g) ) ) by A1; ::_thesis: verum end; theorem Th1: :: FUNCT_5:1 ~ {} = {} proof ( [:{},{}:] = {} & dom {} = {} ) by ZFMISC_1:90; then dom (~ {}) = {} by FUNCT_4:46; hence ~ {} = {} ; ::_thesis: verum end; theorem :: FUNCT_5:2 canceled; theorem :: FUNCT_5:3 canceled; theorem :: FUNCT_5:4 canceled; theorem :: FUNCT_5:5 canceled; theorem :: FUNCT_5:6 canceled; theorem :: FUNCT_5:7 canceled; theorem Th8: :: FUNCT_5:8 ( proj1 {} = {} & proj2 {} = {} ) ; theorem Th9: :: FUNCT_5:9 for Y, X being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) proof let Y, X be set ; ::_thesis: ( ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) implies ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) ) set y = the Element of Y; assume ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) ; ::_thesis: ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) then A1: Y <> {} by ZFMISC_1:90; now__::_thesis:_for_x_being_set_holds_ (_x_in_X_iff_ex_y_being_set_st_[x,y]_in_[:X,Y:]_) let x be set ; ::_thesis: ( x in X iff ex y being set st [x,y] in [:X,Y:] ) ( x in X implies [x, the Element of Y] in [:X,Y:] ) by A1, ZFMISC_1:87; hence ( x in X iff ex y being set st [x,y] in [:X,Y:] ) by ZFMISC_1:87; ::_thesis: verum end; hence proj1 [:X,Y:] = X by XTUPLE_0:def_12; ::_thesis: proj2 [:Y,X:] = X now__::_thesis:_for_x_being_set_holds_ (_x_in_X_iff_ex_y_being_set_st_[y,x]_in_[:Y,X:]_) let x be set ; ::_thesis: ( x in X iff ex y being set st [y,x] in [:Y,X:] ) ( x in X implies [ the Element of Y,x] in [:Y,X:] ) by A1, ZFMISC_1:87; hence ( x in X iff ex y being set st [y,x] in [:Y,X:] ) by ZFMISC_1:87; ::_thesis: verum end; hence proj2 [:Y,X:] = X by XTUPLE_0:def_13; ::_thesis: verum end; theorem Th10: :: FUNCT_5:10 for X, Y being set holds ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) proof let X, Y be set ; ::_thesis: ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) thus proj1 [:X,Y:] c= X ::_thesis: proj2 [:X,Y:] c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 [:X,Y:] or x in X ) assume x in proj1 [:X,Y:] ; ::_thesis: x in X then ex y being set st [x,y] in [:X,Y:] by XTUPLE_0:def_12; hence x in X by ZFMISC_1:87; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 [:X,Y:] or y in Y ) assume y in proj2 [:X,Y:] ; ::_thesis: y in Y then ex x being set st [x,y] in [:X,Y:] by XTUPLE_0:def_13; hence y in Y by ZFMISC_1:87; ::_thesis: verum end; theorem Th11: :: FUNCT_5:11 for Z, X, Y being set st Z c= [:X,Y:] holds ( proj1 Z c= X & proj2 Z c= Y ) proof let Z, X, Y be set ; ::_thesis: ( Z c= [:X,Y:] implies ( proj1 Z c= X & proj2 Z c= Y ) ) assume Z c= [:X,Y:] ; ::_thesis: ( proj1 Z c= X & proj2 Z c= Y ) then A1: ( proj1 Z c= proj1 [:X,Y:] & proj2 Z c= proj2 [:X,Y:] ) by XTUPLE_0:8, XTUPLE_0:9; ( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) by Th10; hence ( proj1 Z c= X & proj2 Z c= Y ) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th12: :: FUNCT_5:12 for x, y being set holds ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} ) proof let x, y be set ; ::_thesis: ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} ) thus proj1 {[x,y]} c= {x} :: according to XBOOLE_0:def_10 ::_thesis: ( {x} c= proj1 {[x,y]} & proj2 {[x,y]} = {y} ) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in proj1 {[x,y]} or z in {x} ) assume z in proj1 {[x,y]} ; ::_thesis: z in {x} then consider t being set such that A1: [z,t] in {[x,y]} by XTUPLE_0:def_12; [z,t] = [x,y] by A1, TARSKI:def_1; then z = x by XTUPLE_0:1; hence z in {x} by TARSKI:def_1; ::_thesis: verum end; thus {x} c= proj1 {[x,y]} ::_thesis: proj2 {[x,y]} = {y} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x} or z in proj1 {[x,y]} ) assume z in {x} ; ::_thesis: z in proj1 {[x,y]} then z = x by TARSKI:def_1; then [z,y] in {[x,y]} by TARSKI:def_1; hence z in proj1 {[x,y]} by XTUPLE_0:def_12; ::_thesis: verum end; thus proj2 {[x,y]} c= {y} :: according to XBOOLE_0:def_10 ::_thesis: {y} c= proj2 {[x,y]} proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in proj2 {[x,y]} or z in {y} ) assume z in proj2 {[x,y]} ; ::_thesis: z in {y} then consider t being set such that A2: [t,z] in {[x,y]} by XTUPLE_0:def_13; [t,z] = [x,y] by A2, TARSKI:def_1; then z = y by XTUPLE_0:1; hence z in {y} by TARSKI:def_1; ::_thesis: verum end; thus {y} c= proj2 {[x,y]} ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {y} or z in proj2 {[x,y]} ) assume z in {y} ; ::_thesis: z in proj2 {[x,y]} then z = y by TARSKI:def_1; then [x,z] in {[x,y]} by TARSKI:def_1; hence z in proj2 {[x,y]} by XTUPLE_0:def_13; ::_thesis: verum end; end; theorem :: FUNCT_5:13 for x, y, z, t being set holds ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) proof let x, y, z, t be set ; ::_thesis: ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) A1: ( proj2 {[x,y]} = {y} & proj2 {[z,t]} = {t} ) by Th12; {[x,y],[z,t]} = {[x,y]} \/ {[z,t]} by ENUMSET1:1; then A2: ( proj1 {[x,y],[z,t]} = (proj1 {[x,y]}) \/ (proj1 {[z,t]}) & proj2 {[x,y],[z,t]} = (proj2 {[x,y]}) \/ (proj2 {[z,t]}) ) by XTUPLE_0:23, XTUPLE_0:27; ( proj1 {[x,y]} = {x} & proj1 {[z,t]} = {z} ) by Th12; hence ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) by A2, A1, ENUMSET1:1; ::_thesis: verum end; theorem Th14: :: FUNCT_5:14 for X being set st ( for x, y being set holds not [x,y] in X ) holds ( proj1 X = {} & proj2 X = {} ) proof let X be set ; ::_thesis: ( ( for x, y being set holds not [x,y] in X ) implies ( proj1 X = {} & proj2 X = {} ) ) set x = the Element of proj2 X; assume A1: for x, y being set holds not [x,y] in X ; ::_thesis: ( proj1 X = {} & proj2 X = {} ) hereby ::_thesis: proj2 X = {} set x = the Element of proj1 X; assume proj1 X <> {} ; ::_thesis: contradiction then ex y being set st [ the Element of proj1 X,y] in X by XTUPLE_0:def_12; hence contradiction by A1; ::_thesis: verum end; assume proj2 X <> {} ; ::_thesis: contradiction then ex y being set st [y, the Element of proj2 X] in X by XTUPLE_0:def_13; hence contradiction by A1; ::_thesis: verum end; theorem :: FUNCT_5:15 for X being set st ( proj1 X = {} or proj2 X = {} ) holds for x, y being set holds not [x,y] in X by XTUPLE_0:def_12, XTUPLE_0:def_13; theorem :: FUNCT_5:16 for X being set holds ( proj1 X = {} iff proj2 X = {} ) proof let X be set ; ::_thesis: ( proj1 X = {} iff proj2 X = {} ) ( ( proj1 X = {} or proj2 X = {} ) implies for x, y being set holds not [x,y] in X ) by XTUPLE_0:def_12, XTUPLE_0:def_13; hence ( proj1 X = {} iff proj2 X = {} ) by Th14; ::_thesis: verum end; theorem Th17: :: FUNCT_5:17 for f being Function holds ( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) ) proof let f be Function; ::_thesis: ( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) ) thus proj1 (dom f) c= proj2 (dom (~ f)) :: according to XBOOLE_0:def_10 ::_thesis: ( proj2 (dom (~ f)) c= proj1 (dom f) & proj2 (dom f) = proj1 (dom (~ f)) ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 (dom f) or x in proj2 (dom (~ f)) ) assume x in proj1 (dom f) ; ::_thesis: x in proj2 (dom (~ f)) then consider y being set such that A1: [x,y] in dom f by XTUPLE_0:def_12; [y,x] in dom (~ f) by A1, FUNCT_4:42; hence x in proj2 (dom (~ f)) by XTUPLE_0:def_13; ::_thesis: verum end; thus proj2 (dom (~ f)) c= proj1 (dom f) ::_thesis: proj2 (dom f) = proj1 (dom (~ f)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 (dom (~ f)) or y in proj1 (dom f) ) assume y in proj2 (dom (~ f)) ; ::_thesis: y in proj1 (dom f) then consider x being set such that A2: [x,y] in dom (~ f) by XTUPLE_0:def_13; [y,x] in dom f by A2, FUNCT_4:42; hence y in proj1 (dom f) by XTUPLE_0:def_12; ::_thesis: verum end; thus proj2 (dom f) c= proj1 (dom (~ f)) :: according to XBOOLE_0:def_10 ::_thesis: proj1 (dom (~ f)) c= proj2 (dom f) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 (dom f) or y in proj1 (dom (~ f)) ) assume y in proj2 (dom f) ; ::_thesis: y in proj1 (dom (~ f)) then consider x being set such that A3: [x,y] in dom f by XTUPLE_0:def_13; [y,x] in dom (~ f) by A3, FUNCT_4:42; hence y in proj1 (dom (~ f)) by XTUPLE_0:def_12; ::_thesis: verum end; thus proj1 (dom (~ f)) c= proj2 (dom f) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 (dom (~ f)) or x in proj2 (dom f) ) assume x in proj1 (dom (~ f)) ; ::_thesis: x in proj2 (dom f) then consider y being set such that A4: [x,y] in dom (~ f) by XTUPLE_0:def_12; [y,x] in dom f by A4, FUNCT_4:42; hence x in proj2 (dom f) by XTUPLE_0:def_13; ::_thesis: verum end; end; theorem :: FUNCT_5:18 for f being Relation holds ( proj1 f = dom f & proj2 f = rng f ) ; definition let f be Function; func curry f -> Function means :Def1: :: FUNCT_5:def 1 ( dom it = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( it . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ); existence ex b1 being Function st ( dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ) proof defpred S1[ set , Function] means ( dom \$2 = proj2 ((dom f) /\ [:{\$1},(proj2 (dom f)):]) & ( for y being set st y in dom \$2 holds \$2 . y = f . (\$1,y) ) ); defpred S2[ set , set ] means ex g being Function st ( \$2 = g & S1[\$1,g] ); A1: for x, y, z being set st x in proj1 (dom f) & S2[x,y] & S2[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( x in proj1 (dom f) & S2[x,y] & S2[x,z] implies y = z ) assume x in proj1 (dom f) ; ::_thesis: ( not S2[x,y] or not S2[x,z] or y = z ) given g1 being Function such that A2: y = g1 and A3: S1[x,g1] ; ::_thesis: ( not S2[x,z] or y = z ) given g2 being Function such that A4: z = g2 and A5: S1[x,g2] ; ::_thesis: y = z now__::_thesis:_for_t_being_set_st_t_in_proj2_((dom_f)_/\_[:{x},(proj2_(dom_f)):])_holds_ g1_._t_=_g2_._t let t be set ; ::_thesis: ( t in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) implies g1 . t = g2 . t ) assume A6: t in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) ; ::_thesis: g1 . t = g2 . t then g1 . t = f . (x,t) by A3; hence g1 . t = g2 . t by A5, A6; ::_thesis: verum end; hence y = z by A2, A3, A4, A5, FUNCT_1:2; ::_thesis: verum end; A7: for x being set st x in proj1 (dom f) holds ex y being set st S2[x,y] proof let x be set ; ::_thesis: ( x in proj1 (dom f) implies ex y being set st S2[x,y] ) assume x in proj1 (dom f) ; ::_thesis: ex y being set st S2[x,y] deffunc H1( set ) -> set = f . [x,\$1]; consider g being Function such that A8: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) holds g . y = H1(y) ) ) from FUNCT_1:sch_3(); reconsider y = g as set ; take y ; ::_thesis: S2[x,y] take g ; ::_thesis: ( y = g & S1[x,g] ) thus ( y = g & S1[x,g] ) by A8; ::_thesis: verum end; ex g being Function st ( dom g = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds S2[x,g . x] ) ) from FUNCT_1:sch_2(A1, A7); hence ex b1 being Function st ( dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) & dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( dom f1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( f1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) & dom f2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( f2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) implies f1 = f2 ) assume that A9: dom f1 = proj1 (dom f) and A10: for x being set st x in proj1 (dom f) holds ex g being Function st ( f1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) and A11: dom f2 = proj1 (dom f) and A12: for x being set st x in proj1 (dom f) holds ex g being Function st ( f2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ; ::_thesis: f1 = f2 now__::_thesis:_for_x_being_set_st_x_in_proj1_(dom_f)_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in proj1 (dom f) implies f1 . x = f2 . x ) assume A13: x in proj1 (dom f) ; ::_thesis: f1 . x = f2 . x then consider g1 being Function such that A14: f1 . x = g1 and A15: dom g1 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and A16: for y being set st y in dom g1 holds g1 . y = f . (x,y) by A10; consider g2 being Function such that A17: f2 . x = g2 and A18: dom g2 = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and A19: for y being set st y in dom g2 holds g2 . y = f . (x,y) by A12, A13; now__::_thesis:_for_y_being_set_st_y_in_proj2_((dom_f)_/\_[:{x},(proj2_(dom_f)):])_holds_ g1_._y_=_g2_._y let y be set ; ::_thesis: ( y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) implies g1 . y = g2 . y ) assume A20: y in proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) ; ::_thesis: g1 . y = g2 . y then g1 . y = f . (x,y) by A15, A16; hence g1 . y = g2 . y by A18, A19, A20; ::_thesis: verum end; hence f1 . x = f2 . x by A14, A15, A17, A18, FUNCT_1:2; ::_thesis: verum end; hence f1 = f2 by A9, A11, FUNCT_1:2; ::_thesis: verum end; func uncurry f -> Function means :Def2: :: FUNCT_5:def 2 ( ( for t being set holds ( t in dom it iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom it & g = f . (x `1) holds it . x = g . (x `2) ) ); existence ex b1 being Function st ( ( for t being set holds ( t in dom b1 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b1 & g = f . (x `1) holds b1 . x = g . (x `2) ) ) proof defpred S1[ set , set ] means ex g being Function st ( g = f . (\$1 `1) & \$2 = g . (\$1 `2) ); deffunc H1( Function) -> set = dom \$1; defpred S2[ set ] means f . \$1 is Function; consider X being set such that A21: for x being set holds ( x in X iff ( x in dom f & S2[x] ) ) from XBOOLE_0:sch_1(); defpred S3[ set ] means for g1 being Function st g1 = f . (\$1 `1) holds \$1 `2 in dom g1; consider g being Function such that A22: ( dom g = f .: X & ( for g1 being Function st g1 in f .: X holds g . g1 = H1(g1) ) ) from FUNCT_5:sch_1(); consider Y being set such that A23: for x being set holds ( x in Y iff ( x in [:X,(union (rng g)):] & S3[x] ) ) from XBOOLE_0:sch_1(); A24: for x being set st x in Y holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Y implies ex y being set st S1[x,y] ) assume x in Y ; ::_thesis: ex y being set st S1[x,y] then x in [:X,(union (rng g)):] by A23; then x `1 in X by MCART_1:10; then reconsider h = f . (x `1) as Function by A21; take h . (x `2) ; ::_thesis: S1[x,h . (x `2)] take h ; ::_thesis: ( h = f . (x `1) & h . (x `2) = h . (x `2) ) thus ( h = f . (x `1) & h . (x `2) = h . (x `2) ) ; ::_thesis: verum end; A25: for x, x1, x2 being set st x in Y & S1[x,x1] & S1[x,x2] holds x1 = x2 ; consider F being Function such that A26: ( dom F = Y & ( for x being set st x in Y holds S1[x,F . x] ) ) from FUNCT_1:sch_2(A25, A24); take F ; ::_thesis: ( ( for t being set holds ( t in dom F iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom F & g = f . (x `1) holds F . x = g . (x `2) ) ) thus for t being set holds ( t in dom F iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ::_thesis: for x being set for g being Function st x in dom F & g = f . (x `1) holds F . x = g . (x `2) proof let t be set ; ::_thesis: ( t in dom F iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) thus ( t in dom F implies ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ::_thesis: ( ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) implies t in dom F ) proof assume A27: t in dom F ; ::_thesis: ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) take x = t `1 ; ::_thesis: ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) t in [:X,(union (rng g)):] by A23, A26, A27; then A29: x in X by MCART_1:10; then reconsider h = f . x as Function by A21; take h ; ::_thesis: ex y being set st ( t = [x,y] & x in dom f & h = f . x & y in dom h ) take t `2 ; ::_thesis: ( t = [x,(t `2)] & x in dom f & h = f . x & t `2 in dom h ) thus ( t = [x,(t `2)] & x in dom f & h = f . x & t `2 in dom h ) by A21, A23, A26, A27, A29, MCART_1:21; ::_thesis: verum end; given x being set , h being Function, y being set such that A30: t = [x,y] and A31: x in dom f and A32: h = f . x and A33: y in dom h ; ::_thesis: t in dom F A34: x in X by A21, A31, A32; then h in f .: X by A31, A32, FUNCT_1:def_6; then ( g . h = dom h & g . h in rng g ) by A22, FUNCT_1:def_3; then dom h c= union (rng g) by ZFMISC_1:74; then A35: t in [:X,(union (rng g)):] by A30, A33, A34, ZFMISC_1:87; t `1 = x by A30, MCART_1:7; then for g1 being Function st g1 = f . (t `1) holds t `2 in dom g1 by A30, A32, A33, MCART_1:7; hence t in dom F by A23, A26, A35; ::_thesis: verum end; let x be set ; ::_thesis: for g being Function st x in dom F & g = f . (x `1) holds F . x = g . (x `2) let h be Function; ::_thesis: ( x in dom F & h = f . (x `1) implies F . x = h . (x `2) ) assume that A36: x in dom F and A37: h = f . (x `1) ; ::_thesis: F . x = h . (x `2) ex g being Function st ( g = f . (x `1) & F . x = g . (x `2) ) by A26, A36; hence F . x = h . (x `2) by A37; ::_thesis: verum end; uniqueness for b1, b2 being Function st ( for t being set holds ( t in dom b1 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b1 & g = f . (x `1) holds b1 . x = g . (x `2) ) & ( for t being set holds ( t in dom b2 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b2 & g = f . (x `1) holds b2 . x = g . (x `2) ) holds b1 = b2 proof defpred S1[ set ] means ex x being set ex g being Function ex y being set st ( \$1 = [x,y] & x in dom f & g = f . x & y in dom g ); let f1, f2 be Function; ::_thesis: ( ( for t being set holds ( t in dom f1 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom f1 & g = f . (x `1) holds f1 . x = g . (x `2) ) & ( for t being set holds ( t in dom f2 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom f2 & g = f . (x `1) holds f2 . x = g . (x `2) ) implies f1 = f2 ) assume that A38: for t being set holds ( t in dom f1 iff S1[t] ) and A39: for x being set for g being Function st x in dom f1 & g = f . (x `1) holds f1 . x = g . (x `2) and A40: for t being set holds ( t in dom f2 iff S1[t] ) and A41: for x being set for g being Function st x in dom f2 & g = f . (x `1) holds f2 . x = g . (x `2) ; ::_thesis: f1 = f2 A42: dom f1 = dom f2 from XBOOLE_0:sch_2(A38, A40); now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume A43: x in dom f1 ; ::_thesis: f1 . x = f2 . x then consider z being set , g being Function, y being set such that A44: x = [z,y] and z in dom f and A45: g = f . z and y in dom g by A38; A46: ( z = x `1 & y = x `2 ) by A44, MCART_1:7; then f1 . x = g . y by A39, A43, A45; hence f1 . x = f2 . x by A41, A42, A43, A45, A46; ::_thesis: verum end; hence f1 = f2 by A42, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines curry FUNCT_5:def_1_:_ for f, b2 being Function holds ( b2 = curry f iff ( dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds ex g being Function st ( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) ) ) ); :: deftheorem Def2 defines uncurry FUNCT_5:def_2_:_ for f, b2 being Function holds ( b2 = uncurry f iff ( ( for t being set holds ( t in dom b2 iff ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set for g being Function st x in dom b2 & g = f . (x `1) holds b2 . x = g . (x `2) ) ) ); definition let f be Function; func curry' f -> Function equals :: FUNCT_5:def 3 curry (~ f); correctness coherence curry (~ f) is Function; ; func uncurry' f -> Function equals :: FUNCT_5:def 4 ~ (uncurry f); correctness coherence ~ (uncurry f) is Function; ; end; :: deftheorem defines curry' FUNCT_5:def_3_:_ for f being Function holds curry' f = curry (~ f); :: deftheorem defines uncurry' FUNCT_5:def_4_:_ for f being Function holds uncurry' f = ~ (uncurry f); theorem Th19: :: FUNCT_5:19 for x, y being set for f being Function st [x,y] in dom f holds ( x in dom (curry f) & (curry f) . x is Function ) proof let x, y be set ; ::_thesis: for f being Function st [x,y] in dom f holds ( x in dom (curry f) & (curry f) . x is Function ) let f be Function; ::_thesis: ( [x,y] in dom f implies ( x in dom (curry f) & (curry f) . x is Function ) ) assume [x,y] in dom f ; ::_thesis: ( x in dom (curry f) & (curry f) . x is Function ) then A1: x in proj1 (dom f) by XTUPLE_0:def_12; hence x in dom (curry f) by Def1; ::_thesis: (curry f) . x is Function ex g being Function st ( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) by A1, Def1; hence (curry f) . x is Function ; ::_thesis: verum end; theorem Th20: :: FUNCT_5:20 for x, y being set for f, g being Function st [x,y] in dom f & g = (curry f) . x holds ( y in dom g & g . y = f . (x,y) ) proof let x, y be set ; ::_thesis: for f, g being Function st [x,y] in dom f & g = (curry f) . x holds ( y in dom g & g . y = f . (x,y) ) let f, g be Function; ::_thesis: ( [x,y] in dom f & g = (curry f) . x implies ( y in dom g & g . y = f . (x,y) ) ) assume that A1: [x,y] in dom f and A2: g = (curry f) . x ; ::_thesis: ( y in dom g & g . y = f . (x,y) ) x in proj1 (dom f) by A1, XTUPLE_0:def_12; then A3: ex h being Function st ( (curry f) . x = h & dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom h holds h . y = f . (x,y) ) ) by Def1; y in proj2 (dom f) by A1, XTUPLE_0:def_13; then [x,y] in [:{x},(proj2 (dom f)):] by ZFMISC_1:105; then [x,y] in (dom f) /\ [:{x},(proj2 (dom f)):] by A1, XBOOLE_0:def_4; hence y in dom g by A2, A3, XTUPLE_0:def_13; ::_thesis: g . y = f . (x,y) hence g . y = f . (x,y) by A2, A3; ::_thesis: verum end; theorem :: FUNCT_5:21 for x, y being set for f being Function st [x,y] in dom f holds ( y in dom (curry' f) & (curry' f) . y is Function ) proof let x, y be set ; ::_thesis: for f being Function st [x,y] in dom f holds ( y in dom (curry' f) & (curry' f) . y is Function ) let f be Function; ::_thesis: ( [x,y] in dom f implies ( y in dom (curry' f) & (curry' f) . y is Function ) ) assume [x,y] in dom f ; ::_thesis: ( y in dom (curry' f) & (curry' f) . y is Function ) then [y,x] in dom (~ f) by FUNCT_4:42; hence ( y in dom (curry' f) & (curry' f) . y is Function ) by Th19; ::_thesis: verum end; theorem Th22: :: FUNCT_5:22 for x, y being set for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds ( x in dom g & g . x = f . (x,y) ) proof let x, y be set ; ::_thesis: for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds ( x in dom g & g . x = f . (x,y) ) let f, g be Function; ::_thesis: ( [x,y] in dom f & g = (curry' f) . y implies ( x in dom g & g . x = f . (x,y) ) ) assume [x,y] in dom f ; ::_thesis: ( not g = (curry' f) . y or ( x in dom g & g . x = f . (x,y) ) ) then A1: [y,x] in dom (~ f) by FUNCT_4:42; assume A2: g = (curry' f) . y ; ::_thesis: ( x in dom g & g . x = f . (x,y) ) then g . x = (~ f) . (y,x) by A1, Th20; hence ( x in dom g & g . x = f . (x,y) ) by A1, A2, Th20, FUNCT_4:43; ::_thesis: verum end; theorem :: FUNCT_5:23 for f being Function holds dom (curry' f) = proj2 (dom f) proof let f be Function; ::_thesis: dom (curry' f) = proj2 (dom f) dom (curry (~ f)) = proj1 (dom (~ f)) by Def1; hence dom (curry' f) = proj2 (dom f) by Th17; ::_thesis: verum end; theorem Th24: :: FUNCT_5:24 for X, Y being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds ( dom (curry f) = X & dom (curry' f) = Y ) proof let X, Y be set ; ::_thesis: for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds ( dom (curry f) = X & dom (curry' f) = Y ) let f be Function; ::_thesis: ( [:X,Y:] <> {} & dom f = [:X,Y:] implies ( dom (curry f) = X & dom (curry' f) = Y ) ) assume that A1: [:X,Y:] <> {} and A2: dom f = [:X,Y:] ; ::_thesis: ( dom (curry f) = X & dom (curry' f) = Y ) dom (curry f) = proj1 (dom f) by Def1; hence dom (curry f) = X by A1, A2, Th9; ::_thesis: dom (curry' f) = Y thus dom (curry' f) = proj1 (dom (~ f)) by Def1 .= proj1 [:Y,X:] by A2, FUNCT_4:46 .= Y by A1, Th9 ; ::_thesis: verum end; theorem Th25: :: FUNCT_5:25 for X, Y being set for f being Function st dom f c= [:X,Y:] holds ( dom (curry f) c= X & dom (curry' f) c= Y ) proof let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds ( dom (curry f) c= X & dom (curry' f) c= Y ) let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies ( dom (curry f) c= X & dom (curry' f) c= Y ) ) assume A1: dom f c= [:X,Y:] ; ::_thesis: ( dom (curry f) c= X & dom (curry' f) c= Y ) dom (curry f) = proj1 (dom f) by Def1; hence dom (curry f) c= X by A1, Th11; ::_thesis: dom (curry' f) c= Y A2: dom (curry' f) = proj1 (dom (~ f)) by Def1; dom (~ f) c= [:Y,X:] by A1, FUNCT_4:45; hence dom (curry' f) c= Y by A2, Th11; ::_thesis: verum end; theorem Th26: :: FUNCT_5:26 for X, Y being set for f being Function st rng f c= Funcs (X,Y) holds ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= Funcs (X,Y) holds ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) let f be Function; ::_thesis: ( rng f c= Funcs (X,Y) implies ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) ) defpred S1[ set ] means ex x being set ex g being Function ex y being set st ( \$1 = [x,y] & x in dom f & g = f . x & y in dom g ); assume A1: rng f c= Funcs (X,Y) ; ::_thesis: ( dom (uncurry f) = [:(dom f),X:] & dom (uncurry' f) = [:X,(dom f):] ) A2: for t being set holds ( t in [:(dom f),X:] iff S1[t] ) proof let t be set ; ::_thesis: ( t in [:(dom f),X:] iff S1[t] ) thus ( t in [:(dom f),X:] implies ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ::_thesis: ( S1[t] implies t in [:(dom f),X:] ) proof assume A3: t in [:(dom f),X:] ; ::_thesis: ex x being set ex g being Function ex y being set st ( t = [x,y] & x in dom f & g = f . x & y in dom g ) then t `1 in dom f by MCART_1:10; then f . (t `1) in rng f by FUNCT_1:def_3; then consider g being Function such that A4: ( f . (t `1) = g & dom g = X ) and rng g c= Y by A1, FUNCT_2:def_2; take t `1 ; ::_thesis: ex g being Function ex y being set st ( t = [(t `1),y] & t `1 in dom f & g = f . (t `1) & y in dom g ) take g ; ::_thesis: ex y being set st ( t = [(t `1),y] & t `1 in dom f & g = f . (t `1) & y in dom g ) take t `2 ; ::_thesis: ( t = [(t `1),(t `2)] & t `1 in dom f & g = f . (t `1) & t `2 in dom g ) thus ( t = [(t `1),(t `2)] & t `1 in dom f & g = f . (t `1) & t `2 in dom g ) by A3, A4, MCART_1:10, MCART_1:21; ::_thesis: verum end; given x being set , g being Function, y being set such that A5: t = [x,y] and A6: x in dom f and A7: g = f . x and A8: y in dom g ; ::_thesis: t in [:(dom f),X:] g in rng f by A6, A7, FUNCT_1:def_3; then ex g1 being Function st ( g = g1 & dom g1 = X & rng g1 c= Y ) by A1, FUNCT_2:def_2; hence t in [:(dom f),X:] by A5, A6, A8, ZFMISC_1:87; ::_thesis: verum end; A9: for t being set holds ( t in dom (uncurry f) iff S1[t] ) by Def2; thus dom (uncurry f) = [:(dom f),X:] from XBOOLE_0:sch_2(A9, A2); ::_thesis: dom (uncurry' f) = [:X,(dom f):] hence dom (uncurry' f) = [:X,(dom f):] by FUNCT_4:46; ::_thesis: verum end; theorem :: FUNCT_5:27 for f being Function st ( for x, y being set holds not [x,y] in dom f ) holds ( curry f = {} & curry' f = {} ) proof let f be Function; ::_thesis: ( ( for x, y being set holds not [x,y] in dom f ) implies ( curry f = {} & curry' f = {} ) ) assume A1: for x, y being set holds not [x,y] in dom f ; ::_thesis: ( curry f = {} & curry' f = {} ) then proj1 (dom f) = {} by Th14; then dom (curry f) = {} by Def1; hence curry f = {} ; ::_thesis: curry' f = {} now__::_thesis:_for_x,_y_being_set_holds_not_[x,y]_in_dom_(~_f) let x, y be set ; ::_thesis: not [x,y] in dom (~ f) assume [x,y] in dom (~ f) ; ::_thesis: contradiction then [y,x] in dom f by FUNCT_4:42; hence contradiction by A1; ::_thesis: verum end; then proj1 (dom (~ f)) = {} by Th14; then dom (curry (~ f)) = {} by Def1; hence curry' f = {} ; ::_thesis: verum end; theorem :: FUNCT_5:28 for f being Function st ( for x being set holds ( not x in dom f or not f . x is Function ) ) holds ( uncurry f = {} & uncurry' f = {} ) proof let f be Function; ::_thesis: ( ( for x being set holds ( not x in dom f or not f . x is Function ) ) implies ( uncurry f = {} & uncurry' f = {} ) ) assume A1: for x being set holds ( not x in dom f or not f . x is Function ) ; ::_thesis: ( uncurry f = {} & uncurry' f = {} ) A2: now__::_thesis:_not_dom_(uncurry_f)_<>_{} set t = the Element of dom (uncurry f); assume dom (uncurry f) <> {} ; ::_thesis: contradiction then ex x being set ex g being Function ex y being set st ( the Element of dom (uncurry f) = [x,y] & x in dom f & g = f . x & y in dom g ) by Def2; hence contradiction by A1; ::_thesis: verum end; hence uncurry f = {} ; ::_thesis: uncurry' f = {} thus uncurry' f = {} by A2, Th1, RELAT_1:41; ::_thesis: verum end; theorem Th29: :: FUNCT_5:29 for X, Y, x being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) proof let X, Y, x be set ; ::_thesis: for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & x in X holds ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) let f be Function; ::_thesis: ( [:X,Y:] <> {} & dom f = [:X,Y:] & x in X implies ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) ) assume that A1: [:X,Y:] <> {} and A2: dom f = [:X,Y:] and A3: x in X ; ::_thesis: ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) {x} c= X by A3, ZFMISC_1:31; then A4: [:{x},Y:] /\ (dom f) = [:{x},Y:] by A2, ZFMISC_1:101; x in proj1 (dom f) by A1, A2, A3, Th9; then consider g being Function such that A5: (curry f) . x = g and A6: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) by Def1; take g ; ::_thesis: ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) A7: proj2 [:{x},Y:] = Y by Th9; A8: proj2 (dom f) = Y by A2, A3, Th9; rng g c= rng f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in rng f ) assume z in rng g ; ::_thesis: z in rng f then consider y being set such that A9: ( y in dom g & z = g . y ) by FUNCT_1:def_3; ( [x,y] in dom f & z = f . (x,y) ) by A2, A3, A6, A8, A4, A7, A9, ZFMISC_1:87; hence z in rng f by FUNCT_1:def_3; ::_thesis: verum end; hence ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) by A5, A6, A8, A4, A7; ::_thesis: verum end; theorem Th30: :: FUNCT_5:30 for x being set for f being Function st x in dom (curry f) holds (curry f) . x is Function proof let x be set ; ::_thesis: for f being Function st x in dom (curry f) holds (curry f) . x is Function let f be Function; ::_thesis: ( x in dom (curry f) implies (curry f) . x is Function ) assume A1: x in dom (curry f) ; ::_thesis: (curry f) . x is Function dom (curry f) = proj1 (dom f) by Def1; then ex g being Function st ( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds g . y = f . (x,y) ) ) by A1, Def1; hence (curry f) . x is Function ; ::_thesis: verum end; theorem Th31: :: FUNCT_5:31 for x being set for f, g being Function st x in dom (curry f) & g = (curry f) . x holds ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) proof let x be set ; ::_thesis: for f, g being Function st x in dom (curry f) & g = (curry f) . x holds ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) let f, g be Function; ::_thesis: ( x in dom (curry f) & g = (curry f) . x implies ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) ) assume that A1: x in dom (curry f) and A2: g = (curry f) . x ; ::_thesis: ( dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) dom (curry f) = proj1 (dom f) by Def1; then consider h being Function such that A3: (curry f) . x = h and A4: dom h = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) and A5: for y being set st y in dom h holds h . y = f . (x,y) by A1, Def1; thus dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) by A2, A3, A4; ::_thesis: ( dom g c= proj2 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) (dom f) /\ [:{x},(proj2 (dom f)):] c= dom f by XBOOLE_1:17; hence dom g c= proj2 (dom f) by A2, A3, A4, XTUPLE_0:9; ::_thesis: ( rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) ) ) thus rng g c= rng f ::_thesis: for y being set st y in dom g holds ( g . y = f . (x,y) & [x,y] in dom f ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in rng f ) assume y in rng g ; ::_thesis: y in rng f then consider z being set such that A6: z in dom g and A7: y = g . z by FUNCT_1:def_3; consider t being set such that A8: [t,z] in (dom f) /\ [:{x},(proj2 (dom f)):] by A2, A3, A4, A6, XTUPLE_0:def_13; ( [t,z] in dom f & [t,z] in [:{x},(proj2 (dom f)):] ) by A8, XBOOLE_0:def_4; then A9: [x,z] in dom f by ZFMISC_1:105; h . z = f . (x,z) by A2, A3, A5, A6; hence y in rng f by A2, A3, A7, A9, FUNCT_1:def_3; ::_thesis: verum end; let y be set ; ::_thesis: ( y in dom g implies ( g . y = f . (x,y) & [x,y] in dom f ) ) assume A10: y in dom g ; ::_thesis: ( g . y = f . (x,y) & [x,y] in dom f ) then consider t being set such that A11: [t,y] in (dom f) /\ [:{x},(proj2 (dom f)):] by A2, A3, A4, XTUPLE_0:def_13; ( [t,y] in dom f & [t,y] in [:{x},(proj2 (dom f)):] ) by A11, XBOOLE_0:def_4; hence ( g . y = f . (x,y) & [x,y] in dom f ) by A2, A3, A5, A10, ZFMISC_1:105; ::_thesis: verum end; theorem Th32: :: FUNCT_5:32 for X, Y, y being set for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) proof let X, Y, y be set ; ::_thesis: for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y holds ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) let f be Function; ::_thesis: ( [:X,Y:] <> {} & dom f = [:X,Y:] & y in Y implies ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) ) assume that A1: [:X,Y:] <> {} and A2: dom f = [:X,Y:] and A3: y in Y ; ::_thesis: ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) A4: dom (~ f) = [:Y,X:] by A2, FUNCT_4:46; X <> {} by A1, ZFMISC_1:90; then consider g being Function such that A5: ( (curry (~ f)) . y = g & dom g = X & rng g c= rng (~ f) ) and A6: for x being set st x in X holds g . x = (~ f) . (y,x) by A3, A4, Th29; take g ; ::_thesis: ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) rng (~ f) c= rng f by FUNCT_4:41; hence ( (curry' f) . y = g & dom g = X & rng g c= rng f ) by A5, XBOOLE_1:1; ::_thesis: for x being set st x in X holds g . x = f . (x,y) let x be set ; ::_thesis: ( x in X implies g . x = f . (x,y) ) assume A7: x in X ; ::_thesis: g . x = f . (x,y) then A8: g . x = (~ f) . (y,x) by A6; [y,x] in dom (~ f) by A3, A4, A7, ZFMISC_1:87; hence g . x = f . (x,y) by A8, FUNCT_4:43; ::_thesis: verum end; theorem :: FUNCT_5:33 for x being set for f being Function st x in dom (curry' f) holds (curry' f) . x is Function by Th30; theorem :: FUNCT_5:34 for x being set for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) proof let x be set ; ::_thesis: for f, g being Function st x in dom (curry' f) & g = (curry' f) . x holds ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) let f, g be Function; ::_thesis: ( x in dom (curry' f) & g = (curry' f) . x implies ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) ) A1: rng (~ f) c= rng f by FUNCT_4:41; assume A2: ( x in dom (curry' f) & g = (curry' f) . x ) ; ::_thesis: ( dom g = proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) then dom g = proj2 ((dom (~ f)) /\ [:{x},(proj2 (dom (~ f))):]) by Th31; then A3: dom g = proj2 ((dom (~ f)) /\ [:{x},(proj1 (dom f)):]) by Th17; thus A4: dom g c= proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) :: according to XBOOLE_0:def_10 ::_thesis: ( proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) c= dom g & dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom g or z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) ) assume z in dom g ; ::_thesis: z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) then consider y being set such that A5: [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A3, XTUPLE_0:def_13; [y,z] in [:{x},(proj1 (dom f)):] by A5, XBOOLE_0:def_4; then A6: [z,y] in [:(proj1 (dom f)),{x}:] by ZFMISC_1:88; [y,z] in dom (~ f) by A5, XBOOLE_0:def_4; then [z,y] in dom f by FUNCT_4:42; then [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A6, XBOOLE_0:def_4; hence z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) by XTUPLE_0:def_12; ::_thesis: verum end; thus proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) c= dom g ::_thesis: ( dom g c= proj1 (dom f) & rng g c= rng f & ( for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) ) ) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) or z in dom g ) assume z in proj1 ((dom f) /\ [:(proj1 (dom f)),{x}:]) ; ::_thesis: z in dom g then consider y being set such that A7: [z,y] in (dom f) /\ [:(proj1 (dom f)),{x}:] by XTUPLE_0:def_12; [z,y] in [:(proj1 (dom f)),{x}:] by A7, XBOOLE_0:def_4; then A8: [y,z] in [:{x},(proj1 (dom f)):] by ZFMISC_1:88; [z,y] in dom f by A7, XBOOLE_0:def_4; then [y,z] in dom (~ f) by FUNCT_4:42; then [y,z] in (dom (~ f)) /\ [:{x},(proj1 (dom f)):] by A8, XBOOLE_0:def_4; hence z in dom g by A3, XTUPLE_0:def_13; ::_thesis: verum end; ( dom g c= proj2 (dom (~ f)) & rng g c= rng (~ f) ) by A2, Th31; hence ( dom g c= proj1 (dom f) & rng g c= rng f ) by A1, Th17, XBOOLE_1:1; ::_thesis: for y being set st y in dom g holds ( g . y = f . (y,x) & [y,x] in dom f ) let y be set ; ::_thesis: ( y in dom g implies ( g . y = f . (y,x) & [y,x] in dom f ) ) assume A9: y in dom g ; ::_thesis: ( g . y = f . (y,x) & [y,x] in dom f ) then consider z being set such that A10: [y,z] in (dom f) /\ [:(proj1 (dom f)),{x}:] by A4, XTUPLE_0:def_12; [y,z] in [:(proj1 (dom f)),{x}:] by A10, XBOOLE_0:def_4; then A11: z = x by ZFMISC_1:106; [y,z] in dom f by A10, XBOOLE_0:def_4; then [z,y] in dom (~ f) by FUNCT_4:42; then (~ f) . (x,y) = f . (y,x) by A11, FUNCT_4:43; hence ( g . y = f . (y,x) & [y,x] in dom f ) by A2, A9, A10, A11, Th31, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th35: :: FUNCT_5:35 for X, Y being set for f being Function st dom f = [:X,Y:] holds ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) proof let X, Y be set ; ::_thesis: for f being Function st dom f = [:X,Y:] holds ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) let f be Function; ::_thesis: ( dom f = [:X,Y:] implies ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) ) assume A1: dom f = [:X,Y:] ; ::_thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) A2: now__::_thesis:_(_[:X,Y:]_<>_{}_implies_(_rng_(curry_f)_c=_Funcs_(Y,(rng_f))_&_rng_(curry'_f)_c=_Funcs_(X,(rng_f))_)_) assume A3: [:X,Y:] <> {} ; ::_thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) then A4: dom (curry f) = X by A1, Th24; thus rng (curry f) c= Funcs (Y,(rng f)) ::_thesis: rng (curry' f) c= Funcs (X,(rng f)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (curry f) or z in Funcs (Y,(rng f)) ) assume z in rng (curry f) ; ::_thesis: z in Funcs (Y,(rng f)) then consider x being set such that A5: x in dom (curry f) and A6: z = (curry f) . x by FUNCT_1:def_3; ex g being Function st ( (curry f) . x = g & dom g = Y & rng g c= rng f & ( for y being set st y in Y holds g . y = f . (x,y) ) ) by A1, A3, A4, A5, Th29; hence z in Funcs (Y,(rng f)) by A6, FUNCT_2:def_2; ::_thesis: verum end; A7: dom (curry' f) = Y by A1, A3, Th24; thus rng (curry' f) c= Funcs (X,(rng f)) ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (curry' f) or z in Funcs (X,(rng f)) ) assume z in rng (curry' f) ; ::_thesis: z in Funcs (X,(rng f)) then consider y being set such that A8: y in dom (curry' f) and A9: z = (curry' f) . y by FUNCT_1:def_3; ex g being Function st ( (curry' f) . y = g & dom g = X & rng g c= rng f & ( for x being set st x in X holds g . x = f . (x,y) ) ) by A1, A3, A7, A8, Th32; hence z in Funcs (X,(rng f)) by A9, FUNCT_2:def_2; ::_thesis: verum end; end; now__::_thesis:_(_dom_f_=_{}_implies_(_rng_(curry_f)_c=_Funcs_(Y,(rng_f))_&_rng_(curry'_f)_c=_Funcs_(X,(rng_f))_)_) assume A10: dom f = {} ; ::_thesis: ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) then ( X = {} or Y = {} ) by A1; then A11: [:Y,X:] = {} by ZFMISC_1:90; {} = dom (curry f) by A10, Def1, Th8; then A12: rng (curry f) = {} by RELAT_1:42; ( dom (~ f) = [:Y,X:] & dom (curry (~ f)) = proj1 (dom (~ f)) ) by A1, Def1, FUNCT_4:46; then rng (curry' f) = {} by A11, Th8, RELAT_1:42; hence ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) by A12, XBOOLE_1:2; ::_thesis: verum end; hence ( rng (curry f) c= Funcs (Y,(rng f)) & rng (curry' f) c= Funcs (X,(rng f)) ) by A1, A2; ::_thesis: verum end; theorem :: FUNCT_5:36 for f being Function holds ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) ) proof let f be Function; ::_thesis: ( rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) & rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) ) A1: rng (~ f) c= rng f by FUNCT_4:41; thus rng (curry f) c= PFuncs ((proj2 (dom f)),(rng f)) ::_thesis: rng (curry' f) c= PFuncs ((proj1 (dom f)),(rng f)) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng (curry f) or t in PFuncs ((proj2 (dom f)),(rng f)) ) assume t in rng (curry f) ; ::_thesis: t in PFuncs ((proj2 (dom f)),(rng f)) then consider z being set such that A2: z in dom (curry f) and A3: t = (curry f) . z by FUNCT_1:def_3; dom (curry f) = proj1 (dom f) by Def1; then consider g being Function such that A4: (curry f) . z = g and dom g = proj2 ((dom f) /\ [:{z},(proj2 (dom f)):]) and for y being set st y in dom g holds g . y = f . (z,y) by A2, Def1; ( dom g c= proj2 (dom f) & rng g c= rng f ) by A2, A4, Th31; hence t in PFuncs ((proj2 (dom f)),(rng f)) by A3, A4, PARTFUN1:def_3; ::_thesis: verum end; let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng (curry' f) or t in PFuncs ((proj1 (dom f)),(rng f)) ) assume t in rng (curry' f) ; ::_thesis: t in PFuncs ((proj1 (dom f)),(rng f)) then consider z being set such that A5: z in dom (curry' f) and A6: t = (curry' f) . z by FUNCT_1:def_3; dom (curry (~ f)) = proj1 (dom (~ f)) by Def1; then consider g being Function such that A7: (curry (~ f)) . z = g and dom g = proj2 ((dom (~ f)) /\ [:{z},(proj2 (dom (~ f))):]) and for y being set st y in dom g holds g . y = (~ f) . (z,y) by A5, Def1; rng g c= rng (~ f) by A5, A7, Th31; then A8: rng g c= rng f by A1, XBOOLE_1:1; dom g c= proj2 (dom (~ f)) by A5, A7, Th31; then dom g c= proj1 (dom f) by Th17; hence t in PFuncs ((proj1 (dom f)),(rng f)) by A6, A7, A8, PARTFUN1:def_3; ::_thesis: verum end; theorem Th37: :: FUNCT_5:37 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) holds ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= PFuncs (X,Y) holds ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) let f be Function; ::_thesis: ( rng f c= PFuncs (X,Y) implies ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) ) assume A1: rng f c= PFuncs (X,Y) ; ::_thesis: ( dom (uncurry f) c= [:(dom f),X:] & dom (uncurry' f) c= [:X,(dom f):] ) thus A2: dom (uncurry f) c= [:(dom f),X:] ::_thesis: dom (uncurry' f) c= [:X,(dom f):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (uncurry f) or x in [:(dom f),X:] ) assume x in dom (uncurry f) ; ::_thesis: x in [:(dom f),X:] then consider y being set , g being Function, z being set such that A3: x = [y,z] and A4: y in dom f and A5: g = f . y and A6: z in dom g by Def2; g in rng f by A4, A5, FUNCT_1:def_3; then g is PartFunc of X,Y by A1, PARTFUN1:46; then dom g c= X by RELAT_1:def_18; hence x in [:(dom f),X:] by A3, A4, A6, ZFMISC_1:87; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (uncurry' f) or x in [:X,(dom f):] ) assume x in dom (uncurry' f) ; ::_thesis: x in [:X,(dom f):] then ex y, z being set st ( x = [z,y] & [y,z] in dom (uncurry f) ) by FUNCT_4:def_2; hence x in [:X,(dom f):] by A2, ZFMISC_1:88; ::_thesis: verum end; theorem Th38: :: FUNCT_5:38 for x, y being set for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) proof let x, y be set ; ::_thesis: for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) let f, g be Function; ::_thesis: ( x in dom f & g = f . x & y in dom g implies ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) ) assume that A1: x in dom f and A2: g = f . x and A3: y in dom g ; ::_thesis: ( [x,y] in dom (uncurry f) & (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) thus A4: [x,y] in dom (uncurry f) by A1, A2, A3, Def2; ::_thesis: ( (uncurry f) . (x,y) = g . y & g . y in rng (uncurry f) ) ( [x,y] `1 = x & [x,y] `2 = y ) ; hence (uncurry f) . (x,y) = g . y by A2, A4, Def2; ::_thesis: g . y in rng (uncurry f) hence g . y in rng (uncurry f) by A4, FUNCT_1:def_3; ::_thesis: verum end; theorem :: FUNCT_5:39 for x, y being set for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [y,x] in dom (uncurry' f) & (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) proof let x, y be set ; ::_thesis: for f, g being Function st x in dom f & g = f . x & y in dom g holds ( [y,x] in dom (uncurry' f) & (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) let f, g be Function; ::_thesis: ( x in dom f & g = f . x & y in dom g implies ( [y,x] in dom (uncurry' f) & (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) ) assume A1: ( x in dom f & g = f . x & y in dom g ) ; ::_thesis: ( [y,x] in dom (uncurry' f) & (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) then [x,y] in dom (uncurry f) by Th38; hence A2: [y,x] in dom (uncurry' f) by FUNCT_4:42; ::_thesis: ( (uncurry' f) . (y,x) = g . y & g . y in rng (uncurry' f) ) (uncurry f) . (x,y) = g . y by A1, Th38; hence (uncurry' f) . (y,x) = g . y by A2, FUNCT_4:43; ::_thesis: g . y in rng (uncurry' f) hence g . y in rng (uncurry' f) by A2, FUNCT_1:def_3; ::_thesis: verum end; theorem Th40: :: FUNCT_5:40 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= PFuncs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) let f be Function; ::_thesis: ( rng f c= PFuncs (X,Y) implies ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) ) assume A1: rng f c= PFuncs (X,Y) ; ::_thesis: ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) thus A2: rng (uncurry f) c= Y ::_thesis: rng (uncurry' f) c= Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (uncurry f) or x in Y ) assume x in rng (uncurry f) ; ::_thesis: x in Y then consider y being set such that A3: y in dom (uncurry f) and A4: x = (uncurry f) . y by FUNCT_1:def_3; consider z being set , g being Function, t being set such that A5: y = [z,t] and A6: ( z in dom f & g = f . z ) and A7: t in dom g by A3, Def2; g in rng f by A6, FUNCT_1:def_3; then A8: ex g1 being Function st ( g = g1 & dom g1 c= X & rng g1 c= Y ) by A1, PARTFUN1:def_3; ( (uncurry f) . (z,t) = g . t & g . t in rng g ) by A6, A7, Th38, FUNCT_1:def_3; hence x in Y by A4, A5, A8; ::_thesis: verum end; rng (uncurry' f) c= rng (uncurry f) by FUNCT_4:41; hence rng (uncurry' f) c= Y by A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th41: :: FUNCT_5:41 for X, Y being set for f being Function st rng f c= Funcs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= Funcs (X,Y) holds ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) let f be Function; ::_thesis: ( rng f c= Funcs (X,Y) implies ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) ) A1: Funcs (X,Y) c= PFuncs (X,Y) by FUNCT_2:72; assume rng f c= Funcs (X,Y) ; ::_thesis: ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) then rng f c= PFuncs (X,Y) by A1, XBOOLE_1:1; hence ( rng (uncurry f) c= Y & rng (uncurry' f) c= Y ) by Th40; ::_thesis: verum end; theorem Th42: :: FUNCT_5:42 ( curry {} = {} & curry' {} = {} ) proof A1: dom (curry {}) = proj1 (dom {}) by Def1; hence curry {} = {} ; ::_thesis: curry' {} = {} thus curry' {} = {} by A1, Th1; ::_thesis: verum end; theorem Th43: :: FUNCT_5:43 ( uncurry {} = {} & uncurry' {} = {} ) proof A1: now__::_thesis:_not_dom_(uncurry_{})_<>_{} set t = the Element of dom (uncurry {}); assume dom (uncurry {}) <> {} ; ::_thesis: contradiction then ex x being set ex g being Function ex y being set st ( the Element of dom (uncurry {}) = [x,y] & x in dom {} & g = {} . x & y in dom g ) by Def2; hence contradiction ; ::_thesis: verum end; hence uncurry {} = {} ; ::_thesis: uncurry' {} = {} thus uncurry' {} = {} by A1, Th1, RELAT_1:41; ::_thesis: verum end; theorem Th44: :: FUNCT_5:44 for X, Y being set for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry f1 = curry f2 implies f1 = f2 ) assume that A1: dom f1 = [:X,Y:] and A2: dom f2 = [:X,Y:] and A3: curry f1 = curry f2 ; ::_thesis: f1 = f2 A4: now__::_thesis:_(_[:X,Y:]_<>_{}_implies_f1_=_f2_) assume [:X,Y:] <> {} ; ::_thesis: f1 = f2 now__::_thesis:_for_z_being_set_st_z_in_[:X,Y:]_holds_ f1_._z_=_f2_._z let z be set ; ::_thesis: ( z in [:X,Y:] implies f1 . z = f2 . z ) assume A5: z in [:X,Y:] ; ::_thesis: f1 . z = f2 . z then consider g1 being Function such that A6: (curry f1) . (z `1) = g1 and dom g1 = Y and rng g1 c= rng f1 and A7: for y being set st y in Y holds g1 . y = f1 . ((z `1),y) by A1, Th29, MCART_1:10; A8: z = [(z `1),(z `2)] by A5, MCART_1:21; A9: z `2 in Y by A5, MCART_1:10; then A10: f1 . ((z `1),(z `2)) = g1 . (z `2) by A7; ex g2 being Function st ( (curry f2) . (z `1) = g2 & dom g2 = Y & rng g2 c= rng f2 & ( for y being set st y in Y holds g2 . y = f2 . ((z `1),y) ) ) by A2, A5, Th29, MCART_1:10; then f2 . ((z `1),(z `2)) = g1 . (z `2) by A3, A9, A6; hence f1 . z = f2 . z by A8, A10; ::_thesis: verum end; hence f1 = f2 by A1, A2, FUNCT_1:2; ::_thesis: verum end; ( [:X,Y:] = {} implies ( f1 = {} & f2 = {} ) ) by A1, A2; hence f1 = f2 by A4; ::_thesis: verum end; theorem Th45: :: FUNCT_5:45 for X, Y being set for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( dom f1 = [:X,Y:] & dom f2 = [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2 ) assume that A1: dom f1 = [:X,Y:] and A2: dom f2 = [:X,Y:] and A3: curry' f1 = curry' f2 ; ::_thesis: f1 = f2 ( dom (~ f1) = [:Y,X:] & dom (~ f2) = [:Y,X:] ) by A1, A2, FUNCT_4:46; then A4: ~ f1 = ~ f2 by A3, Th44; ~ (~ f1) = f1 by A1, FUNCT_4:52; hence f1 = f2 by A2, A4, FUNCT_4:52; ::_thesis: verum end; theorem Th46: :: FUNCT_5:46 for X, Y being set for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 implies f1 = f2 ) assume that A1: rng f1 c= Funcs (X,Y) and A2: rng f2 c= Funcs (X,Y) and A3: X <> {} and A4: uncurry f1 = uncurry f2 ; ::_thesis: f1 = f2 A5: ( dom (uncurry f1) = [:(dom f1),X:] & dom (uncurry f2) = [:(dom f2),X:] ) by A1, A2, Th26; then ( dom f1 = {} implies dom f1 = dom f2 ) by A3, A4, ZFMISC_1:90; then A6: dom f1 = dom f2 by A3, A4, A5, ZFMISC_1:110; now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume A7: x in dom f1 ; ::_thesis: f1 . x = f2 . x then f1 . x in rng f1 by FUNCT_1:def_3; then consider g1 being Function such that A8: f1 . x = g1 and A9: dom g1 = X and rng g1 c= Y by A1, FUNCT_2:def_2; f2 . x in rng f2 by A6, A7, FUNCT_1:def_3; then consider g2 being Function such that A10: f2 . x = g2 and A11: dom g2 = X and rng g2 c= Y by A2, FUNCT_2:def_2; now__::_thesis:_for_y_being_set_st_y_in_X_holds_ g1_._y_=_g2_._y let y be set ; ::_thesis: ( y in X implies g1 . y = g2 . y ) A12: ( [x,y] `1 = x & [x,y] `2 = y ) ; assume A13: y in X ; ::_thesis: g1 . y = g2 . y then A14: [x,y] in dom (uncurry f2) by A4, A7, A8, A9, Def2; [x,y] in dom (uncurry f1) by A7, A8, A9, A13, Def2; then (uncurry f1) . [x,y] = g1 . y by A8, A12, Def2; hence g1 . y = g2 . y by A4, A10, A14, A12, Def2; ::_thesis: verum end; hence f1 . x = f2 . x by A8, A9, A10, A11, FUNCT_1:2; ::_thesis: verum end; hence f1 = f2 by A6, FUNCT_1:2; ::_thesis: verum end; theorem :: FUNCT_5:47 for X, Y being set for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry' f1 = uncurry' f2 implies f1 = f2 ) assume that A1: rng f1 c= Funcs (X,Y) and A2: rng f2 c= Funcs (X,Y) and A3: ( X <> {} & uncurry' f1 = uncurry' f2 ) ; ::_thesis: f1 = f2 dom (uncurry f1) = [:(dom f1),X:] by A1, Th26; then A4: uncurry f1 = ~ (~ (uncurry f1)) by FUNCT_4:52; dom (uncurry f2) = [:(dom f2),X:] by A2, Th26; hence f1 = f2 by A1, A2, A3, A4, Th46, FUNCT_4:52; ::_thesis: verum end; theorem Th48: :: FUNCT_5:48 for X, Y being set for f being Function st rng f c= Funcs (X,Y) & X <> {} holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= Funcs (X,Y) & X <> {} holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) let f be Function; ::_thesis: ( rng f c= Funcs (X,Y) & X <> {} implies ( curry (uncurry f) = f & curry' (uncurry' f) = f ) ) assume that A1: rng f c= Funcs (X,Y) and A2: X <> {} ; ::_thesis: ( curry (uncurry f) = f & curry' (uncurry' f) = f ) A3: dom (uncurry f) = [:(dom f),X:] by A1, Th26; A4: now__::_thesis:_(_dom_f_<>_{}_implies_curry_(uncurry_f)_=_f_) A5: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(curry_(uncurry_f))_._x let x be set ; ::_thesis: ( x in dom f implies f . x = (curry (uncurry f)) . x ) assume A6: x in dom f ; ::_thesis: f . x = (curry (uncurry f)) . x then consider h being Function such that A7: ( (curry (uncurry f)) . x = h & dom h = X & rng h c= rng (uncurry f) ) and A8: for y being set st y in X holds h . y = (uncurry f) . (x,y) by A2, A3, Th29; f . x in rng f by A6, FUNCT_1:def_3; then consider g being Function such that A9: ( f . x = g & dom g = X ) and rng g c= Y by A1, FUNCT_2:def_2; now__::_thesis:_for_y_being_set_st_y_in_X_holds_ g_._y_=_h_._y let y be set ; ::_thesis: ( y in X implies g . y = h . y ) assume A10: y in X ; ::_thesis: g . y = h . y then (uncurry f) . (x,y) = g . y by A6, A9, Th38; hence g . y = h . y by A8, A10; ::_thesis: verum end; hence f . x = (curry (uncurry f)) . x by A9, A7, FUNCT_1:2; ::_thesis: verum end; assume dom f <> {} ; ::_thesis: curry (uncurry f) = f then dom (curry (uncurry f)) = dom f by A2, A3, Th24; hence curry (uncurry f) = f by A5, FUNCT_1:2; ::_thesis: verum end; A11: now__::_thesis:_(_dom_f_=_{}_implies_curry_(uncurry_f)_=_f_) assume dom f = {} ; ::_thesis: curry (uncurry f) = f then ( dom (uncurry f) = {} & f = {} ) by A3, ZFMISC_1:90; hence curry (uncurry f) = f by Th42, RELAT_1:41; ::_thesis: verum end; hence curry (uncurry f) = f by A4; ::_thesis: curry' (uncurry' f) = f thus curry' (uncurry' f) = f by A3, A11, A4, FUNCT_4:52; ::_thesis: verum end; theorem :: FUNCT_5:49 for X, Y being set for f being Function st dom f = [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) proof let X, Y be set ; ::_thesis: for f being Function st dom f = [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) let f be Function; ::_thesis: ( dom f = [:X,Y:] implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) ) assume A1: dom f = [:X,Y:] ; ::_thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f ) A2: now__::_thesis:_(_dom_f_<>_{}_implies_(_uncurry_(curry_f)_=_f_&_uncurry'_(curry'_f)_=_f_)_) A3: rng (curry' f) c= Funcs (X,(rng f)) by A1, Th35; assume A4: dom f <> {} ; ::_thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f ) then X <> {} by A1, ZFMISC_1:90; then A5: curry' (uncurry' (curry' f)) = curry' f by A3, Th48; dom (curry' f) = Y by A1, A4, Th24; then A6: dom (uncurry' (curry' f)) = [:X,Y:] by A3, Th26; A7: rng (curry f) c= Funcs (Y,(rng f)) by A1, Th35; Y <> {} by A1, A4, ZFMISC_1:90; then A8: curry (uncurry (curry f)) = curry f by A7, Th48; dom (curry f) = X by A1, A4, Th24; then dom (uncurry (curry f)) = [:X,Y:] by A7, Th26; hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by A1, A8, A5, A6, Th44, Th45; ::_thesis: verum end; now__::_thesis:_(_dom_f_=_{}_implies_(_uncurry_(curry_f)_=_f_&_uncurry'_(curry'_f)_=_f_)_) assume dom f = {} ; ::_thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f ) then f = {} ; hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by Th42, Th43; ::_thesis: verum end; hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by A2; ::_thesis: verum end; theorem Th50: :: FUNCT_5:50 for X, Y being set for f being Function st dom f c= [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) proof let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds ( uncurry (curry f) = f & uncurry' (curry' f) = f ) let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) ) assume A1: dom f c= [:X,Y:] ; ::_thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f ) A2: now__::_thesis:_for_X,_Y_being_set_ for_f_being_Function_st_dom_f_c=_[:X,Y:]_holds_ uncurry_(curry_f)_=_f let X, Y be set ; ::_thesis: for f being Function st dom f c= [:X,Y:] holds uncurry (curry f) = f let f be Function; ::_thesis: ( dom f c= [:X,Y:] implies uncurry (curry f) = f ) assume A3: dom f c= [:X,Y:] ; ::_thesis: uncurry (curry f) = f A4: dom (uncurry (curry f)) = dom f proof thus dom (uncurry (curry f)) c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (uncurry (curry f)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (uncurry (curry f)) or x in dom f ) assume x in dom (uncurry (curry f)) ; ::_thesis: x in dom f then ex y being set ex g being Function ex z being set st ( x = [y,z] & y in dom (curry f) & g = (curry f) . y & z in dom g ) by Def2; hence x in dom f by Th31; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom (uncurry (curry f)) ) assume A5: x in dom f ; ::_thesis: x in dom (uncurry (curry f)) then A6: x = [(x `1),(x `2)] by A3, MCART_1:21; then reconsider g = (curry f) . (x `1) as Function by A5, Th19; ( x `2 in dom g & x `1 in dom (curry f) ) by A5, A6, Th19, Th20; hence x in dom (uncurry (curry f)) by A6, Th38; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(uncurry_(curry_f))_._x let x be set ; ::_thesis: ( x in dom f implies f . x = (uncurry (curry f)) . x ) assume A7: x in dom f ; ::_thesis: f . x = (uncurry (curry f)) . x then A8: x = [(x `1),(x `2)] by A3, MCART_1:21; then reconsider g = (curry f) . (x `1) as Function by A7, Th19; (uncurry (curry f)) . x = g . (x `2) by A4, A7, Def2; then f . ((x `1),(x `2)) = (uncurry (curry f)) . ((x `1),(x `2)) by A7, A8, Th20; hence f . x = (uncurry (curry f)) . x by A8; ::_thesis: verum end; hence uncurry (curry f) = f by A4, FUNCT_1:2; ::_thesis: verum end; hence uncurry (curry f) = f by A1; ::_thesis: uncurry' (curry' f) = f dom (~ f) c= [:Y,X:] by A1, FUNCT_4:45; then uncurry (curry (~ f)) = ~ f by A2; hence uncurry' (curry' f) = f by A1, FUNCT_4:52; ::_thesis: verum end; theorem Th51: :: FUNCT_5:51 for X, Y being set for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds ( curry (uncurry f) = f & curry' (uncurry' f) = f ) let f be Function; ::_thesis: ( rng f c= PFuncs (X,Y) & not {} in rng f implies ( curry (uncurry f) = f & curry' (uncurry' f) = f ) ) assume that A1: rng f c= PFuncs (X,Y) and A2: not {} in rng f ; ::_thesis: ( curry (uncurry f) = f & curry' (uncurry' f) = f ) A3: dom (curry (uncurry f)) = dom f proof dom (uncurry f) c= [:(dom f),X:] by A1, Th37; hence dom (curry (uncurry f)) c= dom f by Th25; :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom (curry (uncurry f)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom (curry (uncurry f)) ) assume A4: x in dom f ; ::_thesis: x in dom (curry (uncurry f)) then f . x in rng f by FUNCT_1:def_3; then consider g being Function such that A5: f . x = g and dom g c= X and rng g c= Y by A1, PARTFUN1:def_3; set y = the Element of dom g; g <> {} by A2, A4, A5, FUNCT_1:def_3; then A6: [x, the Element of dom g] in dom (uncurry f) by A4, A5, Th38; dom (curry (uncurry f)) = proj1 (dom (uncurry f)) by Def1; hence x in dom (curry (uncurry f)) by A6, XTUPLE_0:def_12; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(curry_(uncurry_f))_._x let x be set ; ::_thesis: ( x in dom f implies f . x = (curry (uncurry f)) . x ) assume A7: x in dom f ; ::_thesis: f . x = (curry (uncurry f)) . x then reconsider h = (curry (uncurry f)) . x as Function by A3, Th30; f . x in rng f by A7, FUNCT_1:def_3; then consider g being Function such that A8: f . x = g and dom g c= X and rng g c= Y by A1, PARTFUN1:def_3; A9: dom h = proj2 ((dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):]) by A3, A7, Th31; A10: dom h = dom g proof thus dom h c= dom g :: according to XBOOLE_0:def_10 ::_thesis: dom g c= dom h proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom h or z in dom g ) assume z in dom h ; ::_thesis: z in dom g then consider t being set such that A11: [t,z] in (dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):] by A9, XTUPLE_0:def_13; [t,z] in [:{x},(proj2 (dom (uncurry f))):] by A11, XBOOLE_0:def_4; then A12: t = x by ZFMISC_1:105; [t,z] in dom (uncurry f) by A11, XBOOLE_0:def_4; then consider x1 being set , g1 being Function, x2 being set such that A13: [t,z] = [x1,x2] and x1 in dom f and A14: ( g1 = f . x1 & x2 in dom g1 ) by Def2; t = x1 by A13, XTUPLE_0:1; hence z in dom g by A8, A13, A14, A12, XTUPLE_0:1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom g or y in dom h ) assume y in dom g ; ::_thesis: y in dom h then [x,y] in dom (uncurry f) by A7, A8, Th38; hence y in dom h by Th20; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_dom_h_holds_ h_._y_=_g_._y let y be set ; ::_thesis: ( y in dom h implies h . y = g . y ) assume A15: y in dom h ; ::_thesis: h . y = g . y hence h . y = (uncurry f) . (x,y) by A3, A7, Th31 .= g . y by A7, A8, A10, A15, Th38 ; ::_thesis: verum end; hence f . x = (curry (uncurry f)) . x by A8, A10, FUNCT_1:2; ::_thesis: verum end; hence A16: curry (uncurry f) = f by A3, FUNCT_1:2; ::_thesis: curry' (uncurry' f) = f dom (uncurry f) c= [:(dom f),X:] by A1, Th37; hence curry' (uncurry' f) = f by A16, FUNCT_4:52; ::_thesis: verum end; theorem :: FUNCT_5:52 for X, Y being set for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry f1 = curry f2 implies f1 = f2 ) assume that A1: dom f1 c= [:X,Y:] and A2: dom f2 c= [:X,Y:] ; ::_thesis: ( not curry f1 = curry f2 or f1 = f2 ) uncurry (curry f1) = f1 by A1, Th50; hence ( not curry f1 = curry f2 or f1 = f2 ) by A2, Th50; ::_thesis: verum end; theorem :: FUNCT_5:53 for X, Y being set for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( dom f1 c= [:X,Y:] & dom f2 c= [:X,Y:] & curry' f1 = curry' f2 implies f1 = f2 ) assume that A1: dom f1 c= [:X,Y:] and A2: dom f2 c= [:X,Y:] ; ::_thesis: ( not curry' f1 = curry' f2 or f1 = f2 ) uncurry' (curry' f1) = f1 by A1, Th50; hence ( not curry' f1 = curry' f2 or f1 = f2 ) by A2, Th50; ::_thesis: verum end; theorem :: FUNCT_5:54 for X, Y being set for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry f1 = uncurry f2 implies f1 = f2 ) assume that A1: rng f1 c= PFuncs (X,Y) and A2: rng f2 c= PFuncs (X,Y) and A3: not {} in rng f1 and A4: not {} in rng f2 ; ::_thesis: ( not uncurry f1 = uncurry f2 or f1 = f2 ) curry (uncurry f1) = f1 by A1, A3, Th51; hence ( not uncurry f1 = uncurry f2 or f1 = f2 ) by A2, A4, Th51; ::_thesis: verum end; theorem :: FUNCT_5:55 for X, Y being set for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds f1 = f2 proof let X, Y be set ; ::_thesis: for f1, f2 being Function st rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 holds f1 = f2 let f1, f2 be Function; ::_thesis: ( rng f1 c= PFuncs (X,Y) & rng f2 c= PFuncs (X,Y) & not {} in rng f1 & not {} in rng f2 & uncurry' f1 = uncurry' f2 implies f1 = f2 ) assume that A1: rng f1 c= PFuncs (X,Y) and A2: rng f2 c= PFuncs (X,Y) and A3: not {} in rng f1 and A4: not {} in rng f2 ; ::_thesis: ( not uncurry' f1 = uncurry' f2 or f1 = f2 ) curry' (uncurry' f1) = f1 by A1, A3, Th51; hence ( not uncurry' f1 = uncurry' f2 or f1 = f2 ) by A2, A4, Th51; ::_thesis: verum end; theorem Th56: :: FUNCT_5:56 for X, Y, Z being set st X c= Y holds Funcs (Z,X) c= Funcs (Z,Y) proof let X, Y, Z be set ; ::_thesis: ( X c= Y implies Funcs (Z,X) c= Funcs (Z,Y) ) assume A1: X c= Y ; ::_thesis: Funcs (Z,X) c= Funcs (Z,Y) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (Z,X) or x in Funcs (Z,Y) ) assume x in Funcs (Z,X) ; ::_thesis: x in Funcs (Z,Y) then consider f being Function such that A2: ( x = f & dom f = Z ) and A3: rng f c= X by FUNCT_2:def_2; rng f c= Y by A1, A3, XBOOLE_1:1; hence x in Funcs (Z,Y) by A2, FUNCT_2:def_2; ::_thesis: verum end; theorem Th57: :: FUNCT_5:57 for X being set holds Funcs ({},X) = {{}} proof let X be set ; ::_thesis: Funcs ({},X) = {{}} thus Funcs ({},X) c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= Funcs ({},X) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs ({},X) or x in {{}} ) assume x in Funcs ({},X) ; ::_thesis: x in {{}} then ex f being Function st ( x = f & dom f = {} & rng f c= X ) by FUNCT_2:def_2; then x = {} ; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in Funcs ({},X) ) A1: {} c= X by XBOOLE_1:2; assume x in {{}} ; ::_thesis: x in Funcs ({},X) then A2: x = {} by TARSKI:def_1; ( dom {} = {} & rng {} = {} ) ; hence x in Funcs ({},X) by A2, A1, FUNCT_2:def_2; ::_thesis: verum end; theorem :: FUNCT_5:58 for X, x being set holds ( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) ) proof let X, x be set ; ::_thesis: ( X, Funcs ({x},X) are_equipotent & card X = card (Funcs ({x},X)) ) deffunc H1( set ) -> Element of bool [:{x},{\$1}:] = {x} --> \$1; consider f being Function such that A1: ( dom f = X & ( for y being set st y in X holds f . y = H1(y) ) ) from FUNCT_1:sch_3(); A2: x in {x} by TARSKI:def_1; thus X, Funcs ({x},X) are_equipotent ::_thesis: card X = card (Funcs ({x},X)) proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = X & proj2 f = Funcs ({x},X) ) thus f is one-to-one ::_thesis: ( proj1 f = X & proj2 f = Funcs ({x},X) ) proof let y be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not y in proj1 f or not b1 in proj1 f or not f . y = f . b1 or y = b1 ) let z be set ; ::_thesis: ( not y in proj1 f or not z in proj1 f or not f . y = f . z or y = z ) assume ( y in dom f & z in dom f ) ; ::_thesis: ( not f . y = f . z or y = z ) then A3: ( f . y = {x} --> y & f . z = {x} --> z ) by A1; ({x} --> y) . x = y by A2, FUNCOP_1:7; hence ( not f . y = f . z or y = z ) by A2, A3, FUNCOP_1:7; ::_thesis: verum end; thus dom f = X by A1; ::_thesis: proj2 f = Funcs ({x},X) thus rng f c= Funcs ({x},X) :: according to XBOOLE_0:def_10 ::_thesis: Funcs ({x},X) c= proj2 f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs ({x},X) ) assume y in rng f ; ::_thesis: y in Funcs ({x},X) then consider z being set such that A4: ( z in dom f & y = f . z ) by FUNCT_1:def_3; A5: ( dom ({x} --> z) = {x} & rng ({x} --> z) = {z} ) by FUNCOP_1:8, FUNCOP_1:13; ( y = {x} --> z & {z} c= X ) by A1, A4, ZFMISC_1:31; hence y in Funcs ({x},X) by A5, FUNCT_2:def_2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Funcs ({x},X) or y in proj2 f ) assume y in Funcs ({x},X) ; ::_thesis: y in proj2 f then consider g being Function such that A6: y = g and A7: dom g = {x} and A8: rng g c= X by FUNCT_2:def_2; A9: g . x in {(g . x)} by TARSKI:def_1; A10: rng g = {(g . x)} by A7, FUNCT_1:4; then g = {x} --> (g . x) by A7, FUNCOP_1:9; then f . (g . x) = g by A1, A8, A10, A9; hence y in proj2 f by A1, A6, A8, A10, A9, FUNCT_1:def_3; ::_thesis: verum end; hence card X = card (Funcs ({x},X)) by CARD_1:5; ::_thesis: verum end; theorem Th59: :: FUNCT_5:59 for X, x being set holds Funcs (X,{x}) = {(X --> x)} proof let X, x be set ; ::_thesis: Funcs (X,{x}) = {(X --> x)} thus Funcs (X,{x}) c= {(X --> x)} :: according to XBOOLE_0:def_10 ::_thesis: {(X --> x)} c= Funcs (X,{x}) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Funcs (X,{x}) or y in {(X --> x)} ) assume y in Funcs (X,{x}) ; ::_thesis: y in {(X --> x)} then consider f being Function such that A1: y = f and A2: dom f = X and A3: rng f c= {x} by FUNCT_2:def_2; A4: now__::_thesis:_(_(_for_z_being_set_holds_not_z_in_X_)_implies_f_=_X_-->_x_) set z = the Element of X; A5: ( X <> {} implies the Element of X in X ) ; A6: dom ({} --> x) = {} ; assume for z being set holds not z in X ; ::_thesis: f = X --> x hence f = X --> x by A2, A5, A6; ::_thesis: verum end; now__::_thesis:_(_ex_z_being_set_st_z_in_X_implies_f_=_X_-->_x_) given z being set such that A7: z in X ; ::_thesis: f = X --> x f . z in rng f by A2, A7, FUNCT_1:def_3; then ( f . z = x & {(f . z)} c= rng f ) by A3, TARSKI:def_1, ZFMISC_1:31; then rng f = {x} by A3, XBOOLE_0:def_10; hence f = X --> x by A2, FUNCOP_1:9; ::_thesis: verum end; hence y in {(X --> x)} by A1, A4, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(X --> x)} or y in Funcs (X,{x}) ) assume y in {(X --> x)} ; ::_thesis: y in Funcs (X,{x}) then A8: y = X --> x by TARSKI:def_1; ( dom (X --> x) = X & rng (X --> x) c= {x} ) by FUNCOP_1:13; hence y in Funcs (X,{x}) by A8, FUNCT_2:def_2; ::_thesis: verum end; theorem Th60: :: FUNCT_5:60 for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) proof let X1, Y1, X2, Y2 be set ; ::_thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent implies ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) ) assume that A1: X1,Y1 are_equipotent and A2: X2,Y2 are_equipotent ; ::_thesis: ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) consider f1 being Function such that A3: f1 is one-to-one and A4: dom f1 = Y1 and A5: rng f1 = X1 by A1, WELLORD2:def_4; consider f2 being Function such that A6: f2 is one-to-one and A7: dom f2 = X2 and A8: rng f2 = Y2 by A2, WELLORD2:def_4; Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent proof A9: rng (f1 ") = Y1 by A3, A4, FUNCT_1:33; deffunc H1( Function) -> set = f2 * (\$1 * f1); consider F being Function such that A10: ( dom F = Funcs (X1,X2) & ( for g being Function st g in Funcs (X1,X2) holds F . g = H1(g) ) ) from FUNCT_5:sch_1(); take F ; :: according to WELLORD2:def_4 ::_thesis: ( F is one-to-one & proj1 F = Funcs (X1,X2) & proj2 F = Funcs (Y1,Y2) ) thus F is one-to-one ::_thesis: ( proj1 F = Funcs (X1,X2) & proj2 F = Funcs (Y1,Y2) ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 F or not b1 in proj1 F or not F . x = F . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y ) assume that A11: x in dom F and A12: y in dom F and A13: F . x = F . y ; ::_thesis: x = y consider g1 being Function such that A14: x = g1 and A15: dom g1 = X1 and A16: rng g1 c= X2 by A10, A11, FUNCT_2:def_2; A17: F . x = f2 * (g1 * f1) by A10, A11, A14; A18: ( rng (g1 * f1) c= X2 & dom (g1 * f1) = Y1 ) by A4, A5, A15, A16, RELAT_1:27, RELAT_1:28; consider g2 being Function such that A19: y = g2 and A20: dom g2 = X1 and A21: rng g2 c= X2 by A10, A12, FUNCT_2:def_2; A22: ( rng (g2 * f1) c= X2 & dom (g2 * f1) = Y1 ) by A4, A5, A20, A21, RELAT_1:27, RELAT_1:28; F . x = f2 * (g2 * f1) by A10, A12, A13, A19; then A23: g1 * f1 = g2 * f1 by A6, A7, A17, A18, A22, FUNCT_1:27; now__::_thesis:_for_z_being_set_st_z_in_X1_holds_ g1_._z_=_g2_._z let z be set ; ::_thesis: ( z in X1 implies g1 . z = g2 . z ) assume z in X1 ; ::_thesis: g1 . z = g2 . z then consider z9 being set such that A24: ( z9 in Y1 & f1 . z9 = z ) by A4, A5, FUNCT_1:def_3; thus g1 . z = (g1 * f1) . z9 by A4, A24, FUNCT_1:13 .= g2 . z by A4, A23, A24, FUNCT_1:13 ; ::_thesis: verum end; hence x = y by A14, A15, A19, A20, FUNCT_1:2; ::_thesis: verum end; thus dom F = Funcs (X1,X2) by A10; ::_thesis: proj2 F = Funcs (Y1,Y2) thus rng F c= Funcs (Y1,Y2) :: according to XBOOLE_0:def_10 ::_thesis: Funcs (Y1,Y2) c= proj2 F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in Funcs (Y1,Y2) ) assume x in rng F ; ::_thesis: x in Funcs (Y1,Y2) then consider y being set such that A25: y in dom F and A26: x = F . y by FUNCT_1:def_3; consider g being Function such that A27: y = g and A28: ( dom g = X1 & rng g c= X2 ) by A10, A25, FUNCT_2:def_2; ( dom (g * f1) = Y1 & rng (g * f1) c= X2 ) by A4, A5, A28, RELAT_1:27, RELAT_1:28; then A29: dom (f2 * (g * f1)) = Y1 by A7, RELAT_1:27; A30: rng (f2 * (g * f1)) c= Y2 by A8, RELAT_1:26; x = f2 * (g * f1) by A10, A25, A26, A27; hence x in Funcs (Y1,Y2) by A29, A30, FUNCT_2:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (Y1,Y2) or x in proj2 F ) assume x in Funcs (Y1,Y2) ; ::_thesis: x in proj2 F then consider g being Function such that A31: x = g and A32: dom g = Y1 and A33: rng g c= Y2 by FUNCT_2:def_2; A34: f2 * ((((f2 ") * g) * (f1 ")) * f1) = f2 * (((f2 ") * g) * ((f1 ") * f1)) by RELAT_1:36 .= (f2 * ((f2 ") * g)) * ((f1 ") * f1) by RELAT_1:36 .= ((f2 * (f2 ")) * g) * ((f1 ") * f1) by RELAT_1:36 .= ((id Y2) * g) * ((f1 ") * f1) by A6, A8, FUNCT_1:39 .= ((id Y2) * g) * (id Y1) by A3, A4, FUNCT_1:39 .= g * (id Y1) by A33, RELAT_1:53 .= x by A31, A32, RELAT_1:52 ; dom (f2 ") = Y2 by A6, A8, FUNCT_1:33; then A35: dom ((f2 ") * g) = Y1 by A32, A33, RELAT_1:27; rng (f2 ") = X2 by A6, A7, FUNCT_1:33; then rng ((f2 ") * g) c= X2 by RELAT_1:26; then A36: rng (((f2 ") * g) * (f1 ")) c= X2 by A9, A35, RELAT_1:28; dom (f1 ") = X1 by A3, A5, FUNCT_1:33; then dom (((f2 ") * g) * (f1 ")) = X1 by A9, A35, RELAT_1:27; then A37: ((f2 ") * g) * (f1 ") in dom F by A10, A36, FUNCT_2:def_2; then F . (((f2 ") * g) * (f1 ")) = f2 * ((((f2 ") * g) * (f1 ")) * f1) by A10; hence x in proj2 F by A37, A34, FUNCT_1:def_3; ::_thesis: verum end; hence ( Funcs (X1,X2), Funcs (Y1,Y2) are_equipotent & card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) by CARD_1:5; ::_thesis: verum end; theorem :: FUNCT_5:61 for X1, Y1, X2, Y2 being set st card X1 = card Y1 & card X2 = card Y2 holds card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) proof let X1, Y1, X2, Y2 be set ; ::_thesis: ( card X1 = card Y1 & card X2 = card Y2 implies card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) ) assume ( card X1 = card Y1 & card X2 = card Y2 ) ; ::_thesis: card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) then ( X1,Y1 are_equipotent & X2,Y2 are_equipotent ) by CARD_1:5; hence card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) by Th60; ::_thesis: verum end; theorem :: FUNCT_5:62 for X1, X2, X being set st X1 misses X2 holds ( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] ) proof let X1, X2, X be set ; ::_thesis: ( X1 misses X2 implies ( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] ) ) deffunc H1( Function) -> set = [(\$1 | X1),(\$1 | X2)]; consider f being Function such that A1: ( dom f = Funcs ((X1 \/ X2),X) & ( for g being Function st g in Funcs ((X1 \/ X2),X) holds f . g = H1(g) ) ) from FUNCT_5:sch_1(); assume A2: X1 misses X2 ; ::_thesis: ( Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent & card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] ) thus Funcs ((X1 \/ X2),X),[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent ::_thesis: card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = Funcs ((X1 \/ X2),X) & proj2 f = [:(Funcs (X1,X)),(Funcs (X2,X)):] ) thus f is one-to-one ::_thesis: ( proj1 f = Funcs ((X1 \/ X2),X) & proj2 f = [:(Funcs (X1,X)),(Funcs (X2,X)):] ) proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y ) assume that A3: x in dom f and A4: y in dom f ; ::_thesis: ( not f . x = f . y or x = y ) consider g2 being Function such that A5: y = g2 and A6: dom g2 = X1 \/ X2 and rng g2 c= X by A1, A4, FUNCT_2:def_2; A7: f . y = [(g2 | X1),(g2 | X2)] by A1, A4, A5; assume A8: f . x = f . y ; ::_thesis: x = y consider g1 being Function such that A9: x = g1 and A10: dom g1 = X1 \/ X2 and rng g1 c= X by A1, A3, FUNCT_2:def_2; A11: f . x = [(g1 | X1),(g1 | X2)] by A1, A3, A9; now__::_thesis:_for_x_being_set_st_x_in_X1_\/_X2_holds_ g1_._x_=_g2_._x let x be set ; ::_thesis: ( x in X1 \/ X2 implies g1 . x = g2 . x ) assume x in X1 \/ X2 ; ::_thesis: g1 . x = g2 . x then ( x in X1 or x in X2 ) by XBOOLE_0:def_3; then ( ( g1 . x = (g1 | X1) . x & g2 . x = (g2 | X1) . x ) or ( g1 . x = (g1 | X2) . x & g2 . x = (g2 | X2) . x ) ) by FUNCT_1:49; hence g1 . x = g2 . x by A11, A7, A8, XTUPLE_0:1; ::_thesis: verum end; hence x = y by A9, A10, A5, A6, FUNCT_1:2; ::_thesis: verum end; thus dom f = Funcs ((X1 \/ X2),X) by A1; ::_thesis: proj2 f = [:(Funcs (X1,X)),(Funcs (X2,X)):] thus rng f c= [:(Funcs (X1,X)),(Funcs (X2,X)):] :: according to XBOOLE_0:def_10 ::_thesis: [:(Funcs (X1,X)),(Funcs (X2,X)):] c= proj2 f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:(Funcs (X1,X)),(Funcs (X2,X)):] ) assume x in rng f ; ::_thesis: x in [:(Funcs (X1,X)),(Funcs (X2,X)):] then consider y being set such that A12: y in dom f and A13: x = f . y by FUNCT_1:def_3; consider g being Function such that A14: y = g and A15: dom g = X1 \/ X2 and A16: rng g c= X by A1, A12, FUNCT_2:def_2; rng (g | X2) c= rng g by RELAT_1:70; then A17: rng (g | X2) c= X by A16, XBOOLE_1:1; rng (g | X1) c= rng g by RELAT_1:70; then A18: rng (g | X1) c= X by A16, XBOOLE_1:1; dom (g | X2) = X2 by A15, RELAT_1:62, XBOOLE_1:7; then A19: g | X2 in Funcs (X2,X) by A17, FUNCT_2:def_2; dom (g | X1) = X1 by A15, RELAT_1:62, XBOOLE_1:7; then g | X1 in Funcs (X1,X) by A18, FUNCT_2:def_2; then [(g | X1),(g | X2)] in [:(Funcs (X1,X)),(Funcs (X2,X)):] by A19, ZFMISC_1:87; hence x in [:(Funcs (X1,X)),(Funcs (X2,X)):] by A1, A12, A13, A14; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Funcs (X1,X)),(Funcs (X2,X)):] or x in proj2 f ) assume A20: x in [:(Funcs (X1,X)),(Funcs (X2,X)):] ; ::_thesis: x in proj2 f then A21: x = [(x `1),(x `2)] by MCART_1:21; x `1 in Funcs (X1,X) by A20, MCART_1:10; then consider g1 being Function such that A22: x `1 = g1 and A23: dom g1 = X1 and A24: rng g1 c= X by FUNCT_2:def_2; x `2 in Funcs (X2,X) by A20, MCART_1:10; then consider g2 being Function such that A25: x `2 = g2 and A26: dom g2 = X2 and A27: rng g2 c= X by FUNCT_2:def_2; ( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & (rng g1) \/ (rng g2) c= X \/ X ) by A24, A27, FUNCT_4:17, XBOOLE_1:13; then A28: rng (g1 +* g2) c= X by XBOOLE_1:1; dom (g1 +* g2) = X1 \/ X2 by A23, A26, FUNCT_4:def_1; then A29: g1 +* g2 in dom f by A1, A28, FUNCT_2:def_2; then f . (g1 +* g2) = [((g1 +* g2) | X1),((g1 +* g2) | X2)] by A1 .= [((g1 +* g2) | X1),g2] by A26, FUNCT_4:23 .= x by A2, A21, A22, A23, A25, A26, FUNCT_4:33 ; hence x in proj2 f by A29, FUNCT_1:def_3; ::_thesis: verum end; hence card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] by CARD_1:5; ::_thesis: verum end; theorem :: FUNCT_5:63 for X, Y, Z being set holds ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) proof let X, Y, Z be set ; ::_thesis: ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) deffunc H1( Function) -> Function = curry \$1; consider f being Function such that A1: ( dom f = Funcs ([:X,Y:],Z) & ( for g being Function st g in Funcs ([:X,Y:],Z) holds f . g = H1(g) ) ) from FUNCT_5:sch_1(); A2: now__::_thesis:_(_[:X,Y:]_<>_{}_implies_(_Funcs_([:X,Y:],Z),_Funcs_(X,(Funcs_(Y,Z)))_are_equipotent_&_card_(Funcs_([:X,Y:],Z))_=_card_(Funcs_(X,(Funcs_(Y,Z))))_)_) assume A3: [:X,Y:] <> {} ; ::_thesis: ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) thus Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent ::_thesis: card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = Funcs ([:X,Y:],Z) & proj2 f = Funcs (X,(Funcs (Y,Z))) ) thus f is one-to-one ::_thesis: ( proj1 f = Funcs ([:X,Y:],Z) & proj2 f = Funcs (X,(Funcs (Y,Z))) ) proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A4: x1 in dom f and A5: x2 in dom f and A6: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider g2 being Function such that A7: x2 = g2 and A8: dom g2 = [:X,Y:] and rng g2 c= Z by A1, A5, FUNCT_2:def_2; A9: f . x2 = curry g2 by A1, A5, A7; consider g1 being Function such that A10: x1 = g1 and A11: dom g1 = [:X,Y:] and rng g1 c= Z by A1, A4, FUNCT_2:def_2; f . x1 = curry g1 by A1, A4, A10; hence x1 = x2 by A6, A10, A11, A7, A8, A9, Th44; ::_thesis: verum end; thus dom f = Funcs ([:X,Y:],Z) by A1; ::_thesis: proj2 f = Funcs (X,(Funcs (Y,Z))) thus rng f c= Funcs (X,(Funcs (Y,Z))) :: according to XBOOLE_0:def_10 ::_thesis: Funcs (X,(Funcs (Y,Z))) c= proj2 f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Funcs (X,(Funcs (Y,Z))) ) assume y in rng f ; ::_thesis: y in Funcs (X,(Funcs (Y,Z))) then consider x being set such that A12: x in dom f and A13: y = f . x by FUNCT_1:def_3; consider g being Function such that A14: x = g and A15: dom g = [:X,Y:] and A16: rng g c= Z by A1, A12, FUNCT_2:def_2; A17: dom (curry g) = X by A3, A15, Th24; ( rng (curry g) c= Funcs (Y,(rng g)) & Funcs (Y,(rng g)) c= Funcs (Y,Z) ) by A15, A16, Th35, Th56; then A18: rng (curry g) c= Funcs (Y,Z) by XBOOLE_1:1; y = curry g by A1, A12, A13, A14; hence y in Funcs (X,(Funcs (Y,Z))) by A17, A18, FUNCT_2:def_2; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Funcs (X,(Funcs (Y,Z))) or y in proj2 f ) assume y in Funcs (X,(Funcs (Y,Z))) ; ::_thesis: y in proj2 f then consider g being Function such that A19: y = g and A20: dom g = X and A21: rng g c= Funcs (Y,Z) by FUNCT_2:def_2; ( dom (uncurry g) = [:X,Y:] & rng (uncurry g) c= Z ) by A20, A21, Th26, Th41; then A22: uncurry g in Funcs ([:X,Y:],Z) by FUNCT_2:def_2; Y <> {} by A3, ZFMISC_1:90; then curry (uncurry g) = g by A21, Th48; then f . (uncurry g) = y by A1, A19, A22; hence y in proj2 f by A1, A22, FUNCT_1:def_3; ::_thesis: verum end; hence card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) by CARD_1:5; ::_thesis: verum end; now__::_thesis:_(_[:X,Y:]_=_{}_implies_(_Funcs_([:X,Y:],Z),_Funcs_(X,(Funcs_(Y,Z)))_are_equipotent_&_card_(Funcs_([:X,Y:],Z))_=_card_(Funcs_(X,(Funcs_(Y,Z))))_)_) assume A23: [:X,Y:] = {} ; ::_thesis: ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) then A24: Funcs ([:X,Y:],Z) = {{}} by Th57; A25: now__::_thesis:_(_Y_=_{}_implies_Funcs_([:X,Y:],Z),_Funcs_(X,(Funcs_(Y,Z)))_are_equipotent_) assume Y = {} ; ::_thesis: Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent then Funcs (Y,Z) = {{}} by Th57; then Funcs (X,(Funcs (Y,Z))) = {(X --> {})} by Th59; hence Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent by A24, CARD_1:28; ::_thesis: verum end; ( X = {} or Y = {} ) by A23; hence Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent by A24, A25, Th57; ::_thesis: card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ( X = {} implies Funcs (X,(Funcs (Y,Z))) = {{}} ) by Th57; hence card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) by A23, A25, Th57, CARD_1:5; ::_thesis: verum end; hence ( Funcs ([:X,Y:],Z), Funcs (X,(Funcs (Y,Z))) are_equipotent & card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) ) by A2; ::_thesis: verum end; theorem :: FUNCT_5:64 for Z, X, Y being set holds ( Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent & card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) proof let Z, X, Y be set ; ::_thesis: ( Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent & card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) deffunc H1( Function) -> set = [((pr1 (X,Y)) * \$1),((pr2 (X,Y)) * \$1)]; consider f being Function such that A1: ( dom f = Funcs (Z,[:X,Y:]) & ( for g being Function st g in Funcs (Z,[:X,Y:]) holds f . g = H1(g) ) ) from FUNCT_5:sch_1(); thus Funcs (Z,[:X,Y:]),[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent ::_thesis: card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = Funcs (Z,[:X,Y:]) & proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) thus f is one-to-one ::_thesis: ( proj1 f = Funcs (Z,[:X,Y:]) & proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A2: x1 in dom f and A3: x2 in dom f and A4: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider g1 being Function such that A5: x1 = g1 and A6: dom g1 = Z and A7: rng g1 c= [:X,Y:] by A1, A2, FUNCT_2:def_2; consider g2 being Function such that A8: x2 = g2 and A9: dom g2 = Z and A10: rng g2 c= [:X,Y:] by A1, A3, FUNCT_2:def_2; [((pr1 (X,Y)) * g1),((pr2 (X,Y)) * g1)] = f . x1 by A1, A2, A5 .= [((pr1 (X,Y)) * g2),((pr2 (X,Y)) * g2)] by A1, A3, A4, A8 ; then A11: ( (pr1 (X,Y)) * g1 = (pr1 (X,Y)) * g2 & (pr2 (X,Y)) * g1 = (pr2 (X,Y)) * g2 ) by XTUPLE_0:1; now__::_thesis:_for_x_being_set_st_x_in_Z_holds_ g1_._x_=_g2_._x let x be set ; ::_thesis: ( x in Z implies g1 . x = g2 . x ) assume A12: x in Z ; ::_thesis: g1 . x = g2 . x then A13: ((pr2 (X,Y)) * g1) . x = (pr2 (X,Y)) . (g1 . x) by A6, FUNCT_1:13; A14: g2 . x in rng g2 by A9, A12, FUNCT_1:def_3; then A15: g2 . x = [((g2 . x) `1),((g2 . x) `2)] by A10, MCART_1:21; A16: g1 . x in rng g1 by A6, A12, FUNCT_1:def_3; then A17: g1 . x = [((g1 . x) `1),((g1 . x) `2)] by A7, MCART_1:21; ( (g2 . x) `1 in X & (g2 . x) `2 in Y ) by A10, A14, MCART_1:10; then A18: ( (pr1 (X,Y)) . (((g2 . x) `1),((g2 . x) `2)) = (g2 . x) `1 & (pr2 (X,Y)) . (((g2 . x) `1),((g2 . x) `2)) = (g2 . x) `2 ) by FUNCT_3:def_4, FUNCT_3:def_5; ( (g1 . x) `1 in X & (g1 . x) `2 in Y ) by A7, A16, MCART_1:10; then A19: ( (pr1 (X,Y)) . (((g1 . x) `1),((g1 . x) `2)) = (g1 . x) `1 & (pr2 (X,Y)) . (((g1 . x) `1),((g1 . x) `2)) = (g1 . x) `2 ) by FUNCT_3:def_4, FUNCT_3:def_5; ( ((pr1 (X,Y)) * g1) . x = (pr1 (X,Y)) . (g1 . x) & ((pr1 (X,Y)) * g2) . x = (pr1 (X,Y)) . (g2 . x) ) by A6, A9, A12, FUNCT_1:13; hence g1 . x = g2 . x by A9, A11, A12, A13, A17, A15, A19, A18, FUNCT_1:13; ::_thesis: verum end; hence x1 = x2 by A5, A6, A8, A9, FUNCT_1:2; ::_thesis: verum end; thus dom f = Funcs (Z,[:X,Y:]) by A1; ::_thesis: proj2 f = [:(Funcs (Z,X)),(Funcs (Z,Y)):] thus rng f c= [:(Funcs (Z,X)),(Funcs (Z,Y)):] :: according to XBOOLE_0:def_10 ::_thesis: [:(Funcs (Z,X)),(Funcs (Z,Y)):] c= proj2 f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] ) assume x in rng f ; ::_thesis: x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] then consider y being set such that A20: y in dom f and A21: x = f . y by FUNCT_1:def_3; consider g being Function such that A22: y = g and A23: ( dom g = Z & rng g c= [:X,Y:] ) by A1, A20, FUNCT_2:def_2; A24: rng ((pr1 (X,Y)) * g) c= X ; A25: rng ((pr2 (X,Y)) * g) c= Y ; dom (pr2 (X,Y)) = [:X,Y:] by FUNCT_3:def_5; then dom ((pr2 (X,Y)) * g) = Z by A23, RELAT_1:27; then A26: (pr2 (X,Y)) * g in Funcs (Z,Y) by A25, FUNCT_2:def_2; dom (pr1 (X,Y)) = [:X,Y:] by FUNCT_3:def_4; then dom ((pr1 (X,Y)) * g) = Z by A23, RELAT_1:27; then A27: (pr1 (X,Y)) * g in Funcs (Z,X) by A24, FUNCT_2:def_2; x = [((pr1 (X,Y)) * g),((pr2 (X,Y)) * g)] by A1, A20, A21, A22; hence x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] by A27, A26, ZFMISC_1:87; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] or x in proj2 f ) assume A28: x in [:(Funcs (Z,X)),(Funcs (Z,Y)):] ; ::_thesis: x in proj2 f then A29: x = [(x `1),(x `2)] by MCART_1:21; x `2 in Funcs (Z,Y) by A28, MCART_1:10; then consider g2 being Function such that A30: x `2 = g2 and A31: dom g2 = Z and A32: rng g2 c= Y by FUNCT_2:def_2; x `1 in Funcs (Z,X) by A28, MCART_1:10; then consider g1 being Function such that A33: x `1 = g1 and A34: dom g1 = Z and A35: rng g1 c= X by FUNCT_2:def_2; ( rng <:g1,g2:> c= [:(rng g1),(rng g2):] & [:(rng g1),(rng g2):] c= [:X,Y:] ) by A35, A32, FUNCT_3:51, ZFMISC_1:96; then A36: rng <:g1,g2:> c= [:X,Y:] by XBOOLE_1:1; dom <:g1,g2:> = Z /\ Z by A34, A31, FUNCT_3:def_7; then A37: <:g1,g2:> in Funcs (Z,[:X,Y:]) by A36, FUNCT_2:def_2; ( (pr1 (X,Y)) * <:g1,g2:> = g1 & (pr2 (X,Y)) * <:g1,g2:> = g2 ) by A34, A35, A31, A32, FUNCT_3:52; then f . <:g1,g2:> = [g1,g2] by A1, A37; hence x in proj2 f by A1, A29, A33, A30, A37, FUNCT_1:def_3; ::_thesis: verum end; hence card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] by CARD_1:5; ::_thesis: verum end; theorem :: FUNCT_5:65 for x, y, X being set st x <> y holds ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) ) proof let x, y, X be set ; ::_thesis: ( x <> y implies ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) ) ) deffunc H1( Function) -> set = \$1 " {x}; consider f being Function such that A1: ( dom f = Funcs (X,{x,y}) & ( for g being Function st g in Funcs (X,{x,y}) holds f . g = H1(g) ) ) from FUNCT_5:sch_1(); assume A2: x <> y ; ::_thesis: ( Funcs (X,{x,y}), bool X are_equipotent & card (Funcs (X,{x,y})) = card (bool X) ) thus Funcs (X,{x,y}), bool X are_equipotent ::_thesis: card (Funcs (X,{x,y})) = card (bool X) proof deffunc H2( set ) -> set = x; take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = Funcs (X,{x,y}) & proj2 f = bool X ) thus f is one-to-one ::_thesis: ( proj1 f = Funcs (X,{x,y}) & proj2 f = bool X ) proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A3: x1 in dom f and A4: x2 in dom f and A5: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider g2 being Function such that A6: x2 = g2 and A7: dom g2 = X and A8: rng g2 c= {x,y} by A1, A4, FUNCT_2:def_2; A9: f . x2 = g2 " {x} by A1, A4, A6; consider g1 being Function such that A10: x1 = g1 and A11: dom g1 = X and A12: rng g1 c= {x,y} by A1, A3, FUNCT_2:def_2; A13: f . x1 = g1 " {x} by A1, A3, A10; now__::_thesis:_for_z_being_set_st_z_in_X_holds_ g1_._z_=_g2_._z let z be set ; ::_thesis: ( z in X implies g1 . z = g2 . z ) assume A14: z in X ; ::_thesis: g1 . z = g2 . z A15: now__::_thesis:_(_not_g1_._z_in_{x}_implies_g1_._z_=_g2_._z_) assume A16: not g1 . z in {x} ; ::_thesis: g1 . z = g2 . z then A17: g1 . z <> x by TARSKI:def_1; not z in g2 " {x} by A5, A13, A9, A16, FUNCT_1:def_7; then not g2 . z in {x} by A7, A14, FUNCT_1:def_7; then A18: g2 . z <> x by TARSKI:def_1; g1 . z in rng g1 by A11, A14, FUNCT_1:def_3; then A19: g1 . z = y by A12, A17, TARSKI:def_2; g2 . z in rng g2 by A7, A14, FUNCT_1:def_3; hence g1 . z = g2 . z by A8, A18, A19, TARSKI:def_2; ::_thesis: verum end; now__::_thesis:_(_g1_._z_in_{x}_implies_g1_._z_=_g2_._z_) assume A20: g1 . z in {x} ; ::_thesis: g1 . z = g2 . z then z in g2 " {x} by A5, A11, A13, A9, A14, FUNCT_1:def_7; then g2 . z in {x} by FUNCT_1:def_7; then g2 . z = x by TARSKI:def_1; hence g1 . z = g2 . z by A20, TARSKI:def_1; ::_thesis: verum end; hence g1 . z = g2 . z by A15; ::_thesis: verum end; hence x1 = x2 by A10, A11, A6, A7, FUNCT_1:2; ::_thesis: verum end; thus dom f = Funcs (X,{x,y}) by A1; ::_thesis: proj2 f = bool X thus rng f c= bool X :: according to XBOOLE_0:def_10 ::_thesis: bool X c= proj2 f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in bool X ) assume z in rng f ; ::_thesis: z in bool X then consider t being set such that A21: t in dom f and A22: z = f . t by FUNCT_1:def_3; consider g being Function such that A23: t = g and A24: dom g = X and rng g c= {x,y} by A1, A21, FUNCT_2:def_2; A25: g " {x} c= X by A24, RELAT_1:132; z = g " {x} by A1, A21, A22, A23; hence z in bool X by A25; ::_thesis: verum end; deffunc H3( set ) -> set = y; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in bool X or z in proj2 f ) defpred S1[ set ] means \$1 in z; consider g being Function such that A26: ( dom g = X & ( for t being set st t in X holds ( ( S1[t] implies g . t = H2(t) ) & ( not S1[t] implies g . t = H3(t) ) ) ) ) from PARTFUN1:sch_1(); assume A27: z in bool X ; ::_thesis: z in proj2 f A28: g " {x} = z proof thus g " {x} c= z :: according to XBOOLE_0:def_10 ::_thesis: z c= g " {x} proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in g " {x} or t in z ) assume A29: t in g " {x} ; ::_thesis: t in z then g . t in {x} by FUNCT_1:def_7; then A30: g . t = x by TARSKI:def_1; t in dom g by A29, FUNCT_1:def_7; hence t in z by A2, A26, A30; ::_thesis: verum end; let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in z or t in g " {x} ) assume A31: t in z ; ::_thesis: t in g " {x} then g . t = x by A27, A26; then g . t in {x} by TARSKI:def_1; hence t in g " {x} by A27, A26, A31, FUNCT_1:def_7; ::_thesis: verum end; rng g c= {x,y} proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng g or t in {x,y} ) assume t in rng g ; ::_thesis: t in {x,y} then ex v being set st ( v in dom g & t = g . v ) by FUNCT_1:def_3; then ( t = x or t = y ) by A26; hence t in {x,y} by TARSKI:def_2; ::_thesis: verum end; then A32: g in Funcs (X,{x,y}) by A26, FUNCT_2:def_2; then f . g = g " {x} by A1; hence z in proj2 f by A1, A32, A28, FUNCT_1:def_3; ::_thesis: verum end; hence card (Funcs (X,{x,y})) = card (bool X) by CARD_1:5; ::_thesis: verum end; theorem :: FUNCT_5:66 for x, y, X being set st x <> y holds ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] ) proof let x, y, X be set ; ::_thesis: ( x <> y implies ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] ) ) deffunc H1( Function) -> set = [(\$1 . x),(\$1 . y)]; consider f being Function such that A1: ( dom f = Funcs ({x,y},X) & ( for g being Function st g in Funcs ({x,y},X) holds f . g = H1(g) ) ) from FUNCT_5:sch_1(); assume A2: x <> y ; ::_thesis: ( Funcs ({x,y},X),[:X,X:] are_equipotent & card (Funcs ({x,y},X)) = card [:X,X:] ) thus Funcs ({x,y},X),[:X,X:] are_equipotent ::_thesis: card (Funcs ({x,y},X)) = card [:X,X:] proof defpred S1[ set ] means \$1 = x; take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = Funcs ({x,y},X) & proj2 f = [:X,X:] ) thus f is one-to-one ::_thesis: ( proj1 f = Funcs ({x,y},X) & proj2 f = [:X,X:] ) proof let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 ) assume that A3: x1 in dom f and A4: x2 in dom f and A5: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider g2 being Function such that A6: x2 = g2 and A7: dom g2 = {x,y} and rng g2 c= X by A1, A4, FUNCT_2:def_2; consider g1 being Function such that A8: x1 = g1 and A9: dom g1 = {x,y} and rng g1 c= X by A1, A3, FUNCT_2:def_2; A10: [(g1 . x),(g1 . y)] = f . x1 by A1, A3, A8 .= [(g2 . x),(g2 . y)] by A1, A4, A5, A6 ; now__::_thesis:_for_z_being_set_st_z_in_{x,y}_holds_ g1_._z_=_g2_._z let z be set ; ::_thesis: ( z in {x,y} implies g1 . z = g2 . z ) assume z in {x,y} ; ::_thesis: g1 . z = g2 . z then ( z = x or z = y ) by TARSKI:def_2; hence g1 . z = g2 . z by A10, XTUPLE_0:1; ::_thesis: verum end; hence x1 = x2 by A8, A9, A6, A7, FUNCT_1:2; ::_thesis: verum end; thus dom f = Funcs ({x,y},X) by A1; ::_thesis: proj2 f = [:X,X:] thus rng f c= [:X,X:] :: according to XBOOLE_0:def_10 ::_thesis: [:X,X:] c= proj2 f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in [:X,X:] ) assume z in rng f ; ::_thesis: z in [:X,X:] then consider t being set such that A11: t in dom f and A12: z = f . t by FUNCT_1:def_3; consider g being Function such that A13: t = g and A14: dom g = {x,y} and A15: rng g c= X by A1, A11, FUNCT_2:def_2; x in {x,y} by TARSKI:def_2; then A16: g . x in rng g by A14, FUNCT_1:def_3; y in {x,y} by TARSKI:def_2; then A17: g . y in rng g by A14, FUNCT_1:def_3; z = [(g . x),(g . y)] by A1, A11, A12, A13; hence z in [:X,X:] by A15, A16, A17, ZFMISC_1:87; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:X,X:] or z in proj2 f ) deffunc H2( set ) -> set = z `1 ; deffunc H3( set ) -> set = z `2 ; consider g being Function such that A18: ( dom g = {x,y} & ( for t being set st t in {x,y} holds ( ( S1[t] implies g . t = H2(t) ) & ( not S1[t] implies g . t = H3(t) ) ) ) ) from PARTFUN1:sch_1(); x in {x,y} by TARSKI:def_2; then A19: g . x = z `1 by A18; y in {x,y} by TARSKI:def_2; then A20: g . y = z `2 by A2, A18; assume A21: z in [:X,X:] ; ::_thesis: z in proj2 f then A22: z = [(z `1),(z `2)] by MCART_1:21; A23: ( z `1 in X & z `2 in X ) by A21, MCART_1:10; rng g c= X proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng g or t in X ) assume t in rng g ; ::_thesis: t in X then ex a being set st ( a in dom g & t = g . a ) by FUNCT_1:def_3; hence t in X by A23, A18; ::_thesis: verum end; then A24: g in Funcs ({x,y},X) by A18, FUNCT_2:def_2; then f . g = [(g . x),(g . y)] by A1; hence z in proj2 f by A1, A22, A24, A19, A20, FUNCT_1:def_3; ::_thesis: verum end; hence card (Funcs ({x,y},X)) = card [:X,X:] by CARD_1:5; ::_thesis: verum end; begin notation synonym op0 for 0 ; end; definition :: original: op0 redefine func op0 -> Element of 1; coherence op0 is Element of 1 by CARD_1:49, TARSKI:def_1; end; definition func op1 -> set equals :: FUNCT_5:def 5 0 .--> 0; coherence 0 .--> 0 is set ; func op2 -> set equals :: FUNCT_5:def 6 (0,0) :-> 0; coherence (0,0) :-> 0 is set ; end; :: deftheorem defines op1 FUNCT_5:def_5_:_ op1 = 0 .--> 0; :: deftheorem defines op2 FUNCT_5:def_6_:_ op2 = (0,0) :-> 0; definition :: original: op1 redefine func op1 -> UnOp of 1; coherence op1 is UnOp of 1 by CARD_1:49; :: original: op2 redefine func op2 -> BinOp of 1; coherence op2 is BinOp of 1 by CARD_1:49; end; definition let D be non empty set ; let X be set ; let E be non empty set ; let F be FUNCTION_DOMAIN of X,E; let f be Function of D,F; let d be Element of D; :: original: . redefine funcf . d -> Element of F; coherence f . d is Element of F proof thus f . d is Element of F ; ::_thesis: verum end; end; theorem Th1: :: FUNCT_5:67 for C, D, E being non empty set for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E)) proof let C, D, E be non empty set ; ::_thesis: for f being Function of [:C,D:],E holds curry f is Function of C,(Funcs (D,E)) let f be Function of [:C,D:],E; ::_thesis: curry f is Function of C,(Funcs (D,E)) A1: dom f = [:C,D:] by FUNCT_2:def_1; A2: rng (curry f) c= Funcs (D,E) proof A3: rng (curry f) c= Funcs (D,(rng f)) by A1, Th35; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (curry f) or x in Funcs (D,E) ) assume x in rng (curry f) ; ::_thesis: x in Funcs (D,E) then consider g being Function such that A4: x = g and A5: dom g = D and A6: rng g c= rng f by A3, FUNCT_2:def_2; rng g c= E by A6, XBOOLE_1:1; then g is Function of D,E by A5, FUNCT_2:def_1, RELSET_1:4; hence x in Funcs (D,E) by A4, FUNCT_2:8; ::_thesis: verum end; dom (curry f) = C by A1, Th24; hence curry f is Function of C,(Funcs (D,E)) by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th2: :: FUNCT_5:68 for D, C, E being non empty set for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E)) proof let D, C, E be non empty set ; ::_thesis: for f being Function of [:C,D:],E holds curry' f is Function of D,(Funcs (C,E)) let f be Function of [:C,D:],E; ::_thesis: curry' f is Function of D,(Funcs (C,E)) A1: dom f = [:C,D:] by FUNCT_2:def_1; A2: rng (curry' f) c= Funcs (C,E) proof A3: rng (curry' f) c= Funcs (C,(rng f)) by A1, Th35; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (curry' f) or x in Funcs (C,E) ) assume x in rng (curry' f) ; ::_thesis: x in Funcs (C,E) then consider g being Function such that A4: x = g and A5: dom g = C and A6: rng g c= rng f by A3, FUNCT_2:def_2; rng g c= E by A6, XBOOLE_1:1; then g is Function of C,E by A5, FUNCT_2:def_1, RELSET_1:4; hence x in Funcs (C,E) by A4, FUNCT_2:8; ::_thesis: verum end; dom (curry' f) = D by A1, Th24; hence curry' f is Function of D,(Funcs (C,E)) by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let C, D, E be non empty set ; let f be Function of [:C,D:],E; :: original: curry redefine func curry f -> Function of C,(Funcs (D,E)); coherence curry f is Function of C,(Funcs (D,E)) by Th1; :: original: curry' redefine func curry' f -> Function of D,(Funcs (C,E)); coherence curry' f is Function of D,(Funcs (C,E)) by Th2; end; theorem :: FUNCT_5:69 for C, D, E being non empty set for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d proof let C, D, E be non empty set ; ::_thesis: for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d let c be Element of C; ::_thesis: for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d let d be Element of D; ::_thesis: for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d let f be Function of [:C,D:],E; ::_thesis: f . (c,d) = ((curry f) . c) . d [c,d] in [:C,D:] ; then [c,d] in dom f by FUNCT_2:def_1; hence f . (c,d) = ((curry f) . c) . d by Th20; ::_thesis: verum end; theorem :: FUNCT_5:70 for C, D, E being non empty set for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c proof let C, D, E be non empty set ; ::_thesis: for c being Element of C for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c let c be Element of C; ::_thesis: for d being Element of D for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c let d be Element of D; ::_thesis: for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c let f be Function of [:C,D:],E; ::_thesis: f . (c,d) = ((curry' f) . d) . c [c,d] in [:C,D:] ; then [c,d] in dom f by FUNCT_2:def_1; hence f . (c,d) = ((curry' f) . d) . c by Th22; ::_thesis: verum end; definition let A, B, C be non empty set ; let f be Function of A,(Funcs (B,C)); :: original: uncurry redefine func uncurry f -> Function of [:A,B:],C; coherence uncurry f is Function of [:A,B:],C proof A1: rng f c= Funcs (B,C) ; then A2: rng (uncurry f) c= C by Th41; dom (uncurry f) = [:(dom f),B:] by A1, Th26 .= [:A,B:] by FUNCT_2:def_1 ; hence uncurry f is Function of [:A,B:],C by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; end; theorem :: FUNCT_5:71 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) holds curry (uncurry f) = f let f be Function of A,(Funcs (B,C)); ::_thesis: curry (uncurry f) = f rng f c= Funcs (B,C) ; hence curry (uncurry f) = f by Th48; ::_thesis: verum end; theorem :: FUNCT_5:72 for A, B, C being non empty set for f being Function of A,(Funcs (B,C)) for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b proof let A, B, C be non empty set ; ::_thesis: for f being Function of A,(Funcs (B,C)) for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let f be Function of A,(Funcs (B,C)); ::_thesis: for a being Element of A for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let a be Element of A; ::_thesis: for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b let b be Element of B; ::_thesis: (uncurry f) . (a,b) = (f . a) . b ( dom f = A & dom (f . a) = B ) by FUNCT_2:def_1; hence (uncurry f) . (a,b) = (f . a) . b by Th38; ::_thesis: verum end;