:: 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;