let X be set ; :: thesis:
let f be Function; :: thesis:
defpred S₁[ set , set ] means ex g, h being Function st
( $1 = g & $2 = h & dom h = dom f & ( for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) ) );
A1: for x being set st x in Funcs ((Union (disjoin f)),X) holds
ex z being set st S₁[x,z]

defpred S₂[ set ] means f . $1 = {} ;
deffunc H₁( set ) -> set = {} ;
let x be set ; :: thesis:
assume x in Funcs ((Union (disjoin f)),X) ; :: thesis:
then consider g being Function such that
A2: x = g and
dom g = Union (disjoin f) and
rng g c= X by FUNCT_2:def 2;
deffunc H₂( set ) -> set = (curry' g) . $1;
ex h being Function st
( dom h = dom f & ( for y being set st y in dom f holds
( ( S₂[y] implies h . y = H₁(y) ) & ( not S₂[y] implies h . y = H₂(y) ) ) ) ) from PARTFUN1:sch 1();
hence ex z being set st S₁[x,z] by A2; :: thesis:

end;

consider F being Function such that
A3: ( dom F = Funcs ((Union (disjoin f)),X) & ( for x being set st x in Funcs ((Union (disjoin f)),X) holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A1);
take F ; :: according to WELLORD2:def 4 :: thesis:
thus F is one-to-one :: thesis:

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis:
let y be set ; :: thesis:
assume that
A4: x in dom F and
A5: y in dom F and
A6: F . x = F . y ; :: thesis:
A7: ex f2 being Function st
( y = f2 & dom f2 = Union (disjoin f) & rng f2 c= X ) by A3, A5, FUNCT_2:def 2;
consider g1, h1 being Function such that
A8: x = g1 and
A9: F . x = h1 and
dom h1 = dom f and
A10: for y being set st y in dom f holds
( ( f . y = {} implies h1 . y = {} ) & ( f . y <> {} implies h1 . y = (curry' g1) . y ) ) by A3, A4;
consider g2, h2 being Function such that
A11: y = g2 and
A12: F . y = h2 and
dom h2 = dom f and
A13: for y being set st y in dom f holds
( ( f . y = {} implies h2 . y = {} ) & ( f . y <> {} implies h2 . y = (curry' g2) . y ) ) by A3, A5;
A14: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A4, FUNCT_2:def 2;

now

let z be set ; :: thesis:
assume A15: z in Union (disjoin f) ; :: thesis:
then A16: z = [(z `1),(z `2)] by CARD_3:33;
A17: ( z `2 in dom f & z `1 in f . (z `2) ) by A15, CARD_3:33;
then A18: h2 . (z `2) = (curry' g2) . (z `2) by A13;
then reconsider g91 = h1 . (z `2), g92 = h2 . (z `2) as Function by A6, A7, A9, A11, A12, A15, A16, FUNCT_5:28;
A19: g2 . ((z `1),(z `2)) = g92 . (z `1) by A7, A11, A15, A16, A18, FUNCT_5:29;
h1 . (z `2) = (curry' g1) . (z `2) by A10, A17;
then g1 . ((z `1),(z `2)) = g91 . (z `1) by A14, A8, A15, A16, FUNCT_5:29;
hence g1 . z = g2 . z by A6, A9, A12, A16, A19; :: thesis:

end;

hence x = y by A14, A7, A8, A11, FUNCT_1:9; :: thesis:

end;

thus dom F = Funcs ((Union (disjoin f)),X) by A3; :: thesis:
thus rng F c= product (Funcs (f,X)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng F ; :: thesis:
then consider x being set such that
A20: x in dom F and
A21: y = F . x by FUNCT_1:def 5;
consider g, h being Function such that
A22: x = g and
A23: F . x = h and
A24: dom h = dom f and
A25: for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3, A20;
A26: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A20, FUNCT_2:def 2;

A27: now

let z be set ; :: thesis:
assume z in dom (Funcs (f,X)) ; :: thesis:
then A28: z in dom f by Def8;
then A29: (Funcs (f,X)) . z = Funcs ((f . z),X) by Def8;

A30: now

consider a being Element of f . z;
assume A31: f . z <> {} ; :: thesis:
( [a,z] `1 = a & [a,z] `2 = z ) by MCART_1:7;
then A32: [a,z] in Union (disjoin f) by A28, A31, CARD_3:33;
then reconsider k = (curry' g) . z as Function by A22, A26, FUNCT_5:28;
A33: z in dom (curry' g) by A22, A26, A32, FUNCT_5:28;
then rng k c= rng g by FUNCT_5:41;
then A34: rng k c= X by A22, A26, XBOOLE_1:1;
A35: dom k = proj1 ((dom g) /\ [:(proj1 (dom g)),{z}:]) by A33, FUNCT_5:41;
A36: dom k = f . z

proof

thus dom k c= f . z :: according to XBOOLE_0:def 10 :: thesis:

proof

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in dom k ; :: thesis:
then consider c being set such that
A37: [b,c] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A35, RELAT_1:def 4;
[b,c] in [:(proj1 (dom g)),{z}:] by A37, XBOOLE_0:def 4;
then A38: c in {z} by ZFMISC_1:106;
A39: ( [b,c] `1 = b & [b,c] `2 = c ) by MCART_1:7;
[b,c] in dom g by A37, XBOOLE_0:def 4;
then b in f . c by A22, A26, A39, CARD_3:33;
hence b in f . z by A38, TARSKI:def 1; :: thesis:

end;

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume A40: b in f . z ; :: thesis:
A41: z in {z} by TARSKI:def 1;
( [b,z] `1 = b & [b,z] `2 = z ) by MCART_1:7;
then A42: [b,z] in dom g by A22, A26, A28, A40, CARD_3:33;
then b in proj1 (dom g) by RELAT_1:def 4;
then [b,z] in [:(proj1 (dom g)),{z}:] by A41, ZFMISC_1:106;
then [b,z] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A42, XBOOLE_0:def 4;
hence b in dom k by A35, RELAT_1:def 4; :: thesis:

end;

h . z = k by A25, A28, A31;
hence h . z in (Funcs (f,X)) . z by A29, A34, A36, FUNCT_2:def 2; :: thesis:

end;

now

assume f . z = {} ; :: thesis:
then ( h . z = {} & (Funcs (f,X)) . z = {{}} ) by A25, A28, A29, FUNCT_5:64;
hence h . z in (Funcs (f,X)) . z by TARSKI:def 1; :: thesis:

end;

hence h . z in (Funcs (f,X)) . z by A30; :: thesis:

end;

dom h = dom (Funcs (f,X)) by A24, Def8;
hence y in product (Funcs (f,X)) by A21, A23, A27, CARD_3:def 5; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in product (Funcs (f,X)) ; :: thesis:
then consider s being Function such that
A43: x = s and
A44: dom s = dom (Funcs (f,X)) and
A45: for z being set st z in dom (Funcs (f,X)) holds
s . z in (Funcs (f,X)) . z by CARD_3:def 5;
A46: dom s = dom f by A44, Def8;
A47: uncurry' s = ~ (uncurry s) by FUNCT_5:def 6;
A48: dom (uncurry' s) = Union (disjoin f)

proof

thus dom (uncurry' s) c= Union (disjoin f) :: according to XBOOLE_0:def 10 :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A49: z in dom (uncurry' s) ; :: thesis:
then consider z1, z2 being set such that
A50: z = [z1,z2] by A47, Th11;
A51: ( z `1 = z1 & z `2 = z2 ) by A50, MCART_1:7;
[z2,z1] in dom (uncurry s) by A47, A49, A50, FUNCT_4:43;
then consider a being set , u being Function, b being set such that
A52: [z2,z1] = [a,b] and
A53: a in dom s and
A54: u = s . a and
A55: b in dom u by FUNCT_5:def 4;
A56: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) by MCART_1:7;
( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A53, A54, Def8;
then A57: ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) by A52, A56, FUNCT_2:def 2;
( [a,b] `2 = b & [z2,z1] `2 = z1 ) by MCART_1:7;
hence z in Union (disjoin f) by A46, A50, A52, A53, A55, A51, A56, A57, CARD_3:33; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A58: z in Union (disjoin f) ; :: thesis:
then A59: ( z `1 in f . (z `2) & z = [(z `1),(z `2)] ) by CARD_3:33;
A60: z `2 in dom f by A58, CARD_3:33;
then ( s . (z `2) in (Funcs (f,X)) . (z `2) & (Funcs (f,X)) . (z `2) = Funcs ((f . (z `2)),X) ) by A44, A45, A46, Def8;
then ex j being Function st
( s . (z `2) = j & dom j = f . (z `2) & rng j c= X ) by FUNCT_2:def 2;
hence z in dom (uncurry' s) by A46, A60, A59, FUNCT_5:46; :: thesis:

end;

rng (uncurry' s) c= X

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume d in rng (uncurry' s) ; :: thesis:
then consider z being set such that
A61: z in dom (uncurry' s) and
A62: d = (uncurry' s) . z by FUNCT_1:def 5;
consider z1, z2 being set such that
A63: z = [z1,z2] by A47, A61, Th11;
[z2,z1] in dom (uncurry s) by A47, A61, A63, FUNCT_4:43;
then consider a being set , u being Function, b being set such that
A64: [z2,z1] = [a,b] and
A65: ( a in dom s & u = s . a ) and
A66: b in dom u by FUNCT_5:def 4;
A67: ( [a,b] `1 = a & [z2,z1] `1 = z2 ) by MCART_1:7;
( u in (Funcs (f,X)) . a & (Funcs (f,X)) . a = Funcs ((f . a),X) ) by A44, A45, A46, A65, Def8;
then A68: ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) by A64, A67, FUNCT_2:def 2;
A69: ( [a,b] `2 = b & [z2,z1] `2 = z1 ) by MCART_1:7;
(uncurry' s) . (b,a) = u . b by A65, A66, FUNCT_5:46;
then d in rng u by A62, A63, A64, A66, A67, A69, FUNCT_1:def 5;
hence d in X by A68; :: thesis:

end;

then A70: uncurry' s in dom F by A3, A48, FUNCT_2:def 2;
then consider g, h being Function such that
A71: uncurry' s = g and
A72: F . (uncurry' s) = h and
A73: dom h = dom f and
A74: for y being set st y in dom f holds
( ( f . y = {} implies h . y = {} ) & ( f . y <> {} implies h . y = (curry' g) . y ) ) by A3;

now

let z be set ; :: thesis:
assume A75: z in dom f ; :: thesis:
then ( s . z in (Funcs (f,X)) . z & (Funcs (f,X)) . z = Funcs ((f . z),X) ) by A44, A45, A46, Def8;
then consider v being Function such that
A76: s . z = v and
A77: dom v = f . z and
rng v c= X by FUNCT_2:def 2;

A78: now

consider a being Element of f . z;
assume A79: f . z <> {} ; :: thesis:
then A80: [a,z] in dom (uncurry' s) by A46, A75, A76, A77, FUNCT_5:46;
then reconsider j = (curry' (uncurry' s)) . z as Function by FUNCT_5:28;
A81: j = (curry (~ (uncurry' s))) . z by FUNCT_5:def 5;
A82: ~ (uncurry' s) = uncurry s by Th13;
then A83: [z,a] in dom (uncurry s) by A80, FUNCT_4:43;
A84: dom j = dom v

proof

thus dom j c= dom v :: according to XBOOLE_0:def 10 :: thesis:

proof

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in dom j ; :: thesis:
then [z,b] in dom (uncurry s) by A81, A82, A83, Lm4;
then consider a1 being set , g1 being Function, a2 being set such that
A85: [z,b] = [a1,a2] and
a1 in dom s and
A86: ( g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def 4;
z = a1 by A85, ZFMISC_1:33;
hence b in dom v by A76, A85, A86, ZFMISC_1:33; :: thesis:

end;

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in dom v ; :: thesis:
then [z,b] in dom (uncurry s) by A46, A75, A76, FUNCT_5:45;
hence b in dom j by A81, A82, FUNCT_5:27; :: thesis:

end;

now

let b be set ; :: thesis:
assume b in f . z ; :: thesis:
then A87: [z,b] in dom (uncurry s) by A77, A81, A82, A83, A84, Lm4;
then consider a1 being set , g1 being Function, a2 being set such that
A88: [z,b] = [a1,a2] and
A89: ( a1 in dom s & g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def 4;
A90: j . b = (uncurry s) . (z,b) by A81, A82, A87, FUNCT_5:27;
( z = a1 & b = a2 ) by A88, ZFMISC_1:33;
hence j . b = v . b by A76, A89, A90, FUNCT_5:45; :: thesis:

end;

then v = j by A77, A84, FUNCT_1:9;
hence s . z = h . z by A71, A74, A75, A76, A79; :: thesis:

end;

( f . z = {} implies ( s . z = {} & h . z = {} ) ) by A74, A75, A76, A77;
hence s . z = h . z by A78; :: thesis:

end;

then h = s by A46, A73, FUNCT_1:9;
hence x in proj2 F by A43, A70, A72, FUNCT_1:def 5; :: thesis: