let X be set ; :: thesis: for f being Function holds Funcs (Union (disjoin f)),X, product (Funcs f,X) are_equipotent
let f be Function; :: thesis: Funcs (Union (disjoin f)),X, product (Funcs f,X) are_equipotent
defpred 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]

proof

let x be set ; :: thesis: ( x in Funcs (Union (disjoin f)),X implies ex z being set st S₁[x,z] )
deffunc H₁( set ) -> set = {} ;
defpred S₂[ set ] means f . $1 = {} ;
assume x in Funcs (Union (disjoin f)),X ; :: thesis: ex z being set st S₁[x,z]
then consider g being Function such that
A2: ( x = g & dom g = Union (disjoin f) & 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: verum

end;

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

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 F or not b₁ in proj1 F or not F . x = F . b₁ or x = b₁ )
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 A4: ( x in dom F & y in dom F & F . x = F . y ) ; :: thesis: x = y
then A5: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, FUNCT_2:def 2;
A6: ex f2 being Function st
( y = f2 & dom f2 = Union (disjoin f) & rng f2 c= X ) by A3, A4, FUNCT_2:def 2;
consider g1, h1 being Function such that
A7: ( x = g1 & F . x = h1 & dom h1 = dom f & ( 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
A8: ( y = g2 & F . y = h2 & dom h2 = dom f & ( 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, A4;

now

let z be set ; :: thesis: ( z in Union (disjoin f) implies g1 . z = g2 . z )
assume A9: z in Union (disjoin f) ; :: thesis: g1 . z = g2 . z
then A10: ( z `2 in dom f & z `1 in f . (z `2 ) & z = [(z `1 ),(z `2 )] ) by CARD_3:33;
then A11: ( h1 . (z `2 ) = (curry' g1) . (z `2 ) & h2 . (z `2 ) = (curry' g2) . (z `2 ) ) by A7, A8;
then reconsider g'1 = h1 . (z `2 ), g'2 = h2 . (z `2 ) as Function by A4, A6, A7, A8, A9, A10, FUNCT_5:28;
( g1 . (z `1 ),(z `2 ) = g'1 . (z `1 ) & g2 . (z `1 ),(z `2 ) = g'2 . (z `1 ) ) by A5, A6, A7, A8, A9, A10, A11, FUNCT_5:29;
hence g1 . z = g2 . z by A4, A7, A8, A10; :: thesis: verum

end;

hence x = y by A5, A6, A7, A8, FUNCT_1:9; :: thesis: verum

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in product (Funcs f,X) )
assume y in rng F ; :: thesis: y in product (Funcs f,X)
then consider x being set such that
A12: ( x in dom F & y = F . x ) by FUNCT_1:def 5;
consider g, h being Function such that
A13: ( x = g & F . x = 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 ) ) ) ) by A3, A12;
A14: dom h = dom (Funcs f,X) by A13, Def8;
A15: ex f1 being Function st
( x = f1 & dom f1 = Union (disjoin f) & rng f1 c= X ) by A3, A12, FUNCT_2:def 2;

now

let z be set ; :: thesis: ( z in dom (Funcs f,X) implies h . z in (Funcs f,X) . z )
assume z in dom (Funcs f,X) ; :: thesis: h . z in (Funcs f,X) . z
then A16: z in dom f by Def8;
then A17: (Funcs f,X) . z = Funcs (f . z),X by Def8;

A18: now

assume f . z = {} ; :: thesis: h . z in (Funcs f,X) . z
then ( h . z = {} & (Funcs f,X) . z = {{} } ) by A13, A16, A17, FUNCT_5:64;
hence h . z in (Funcs f,X) . z by TARSKI:def 1; :: thesis: verum

end;

now

assume A19: f . z <> {} ; :: thesis: h . z in (Funcs f,X) . z
consider a being Element of f . z;
( [a,z] `1 = a & [a,z] `2 = z ) by MCART_1:7;
then A20: [a,z] in Union (disjoin f) by A16, A19, CARD_3:33;
then reconsider k = (curry' g) . z as Function by A13, A15, FUNCT_5:28;
A21: ( h . z = k & z in dom (curry' g) ) by A13, A15, A16, A19, A20, FUNCT_5:28;
then rng k c= rng g by FUNCT_5:41;
then A22: rng k c= X by A13, A15, XBOOLE_1:1;
A23: dom k = proj1 ((dom g) /\ [:(proj1 (dom g)),{z}:]) by A21, FUNCT_5:41;
dom k = f . z

proof

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

proof

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

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in f . z or b in dom k )
assume A25: b in f . z ; :: thesis: b in dom k
( [b,z] `1 = b & [b,z] `2 = z ) by MCART_1:7;
then A26: [b,z] in dom g by A13, A15, A16, A25, CARD_3:33;
then ( b in proj1 (dom g) & z in {z} ) by RELAT_1:def 4, TARSKI:def 1;
then [b,z] in [:(proj1 (dom g)),{z}:] by ZFMISC_1:106;
then [b,z] in (dom g) /\ [:(proj1 (dom g)),{z}:] by A26, XBOOLE_0:def 4;
hence b in dom k by A23, RELAT_1:def 4; :: thesis: verum

end;

hence h . z in (Funcs f,X) . z by A17, A21, A22, FUNCT_2:def 2; :: thesis: verum

end;

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

end;

hence y in product (Funcs f,X) by A12, A13, A14, CARD_3:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (Funcs f,X) or x in proj2 F )
assume x in product (Funcs f,X) ; :: thesis: x in proj2 F
then consider s being Function such that
A27: ( x = s & dom s = dom (Funcs f,X) & ( for z being set st z in dom (Funcs f,X) holds
s . z in (Funcs f,X) . z ) ) by CARD_3:def 5;
A28: dom s = dom f by A27, Def8;
A29: uncurry' s = ~ (uncurry s) by FUNCT_5:def 6;
A30: dom (uncurry' s) = Union (disjoin f)

proof

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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in dom (uncurry' s) or z in Union (disjoin f) )
assume A31: z in dom (uncurry' s) ; :: thesis: z in Union (disjoin f)
then consider z1, z2 being set such that
A32: z = [z1,z2] by A29, Th11;
[z2,z1] in dom (uncurry s) by A29, A31, A32, FUNCT_4:43;
then consider a being set , u being Function, b being set such that
A33: ( [z2,z1] = [a,b] & a in dom s & u = s . a & b in dom u ) by FUNCT_5:def 4;
A34: ( u in (Funcs f,X) . a & (Funcs f,X) . a = Funcs (f . a),X & z `1 = z1 & z `2 = z2 & [a,b] `1 = a & [a,b] `2 = b & [z2,z1] `1 = z2 & [z2,z1] `2 = z1 ) by A27, A28, A32, A33, Def8, MCART_1:7;
then ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) by A33, FUNCT_2:def 2;
hence z in Union (disjoin f) by A28, A32, A33, A34, CARD_3:33; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Union (disjoin f) or z in dom (uncurry' s) )
assume z in Union (disjoin f) ; :: thesis: z in dom (uncurry' s)
then A35: ( z `2 in dom f & z `1 in f . (z `2 ) & z = [(z `1 ),(z `2 )] ) by CARD_3:33;
then ( s . (z `2 ) in (Funcs f,X) . (z `2 ) & (Funcs f,X) . (z `2 ) = Funcs (f . (z `2 )),X ) by A27, A28, 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 A28, A35, FUNCT_5:46; :: thesis: verum

end;

rng (uncurry' s) c= X

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in rng (uncurry' s) or d in X )
assume d in rng (uncurry' s) ; :: thesis: d in X
then consider z being set such that
A36: ( z in dom (uncurry' s) & d = (uncurry' s) . z ) by FUNCT_1:def 5;
consider z1, z2 being set such that
A37: z = [z1,z2] by A29, A36, Th11;
[z2,z1] in dom (uncurry s) by A29, A36, A37, FUNCT_4:43;
then consider a being set , u being Function, b being set such that
A38: ( [z2,z1] = [a,b] & a in dom s & u = s . a & b in dom u ) by FUNCT_5:def 4;
( u in (Funcs f,X) . a & (Funcs f,X) . a = Funcs (f . a),X & z `1 = z1 & z `2 = z2 & [a,b] `1 = a & [a,b] `2 = b & [z2,z1] `1 = z2 & (uncurry' s) . b,a = u . b & [z2,z1] `2 = z1 ) by A27, A28, A37, A38, Def8, FUNCT_5:46, MCART_1:7;
then ( d in rng u & ex j being Function st
( u = j & dom j = f . z2 & rng j c= X ) ) by A36, A37, A38, FUNCT_1:def 5, FUNCT_2:def 2;
hence d in X ; :: thesis: verum

end;

then A39: uncurry' s in dom F by A3, A30, FUNCT_2:def 2;
then consider g, h being Function such that
A40: ( uncurry' s = g & F . (uncurry' s) = 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 ) ) ) ) by A3;

now

let z be set ; :: thesis: ( z in dom f implies s . z = h . z )
assume A41: z in dom f ; :: thesis: s . z = h . z
then ( s . z in (Funcs f,X) . z & (Funcs f,X) . z = Funcs (f . z),X ) by A27, A28, Def8;
then consider v being Function such that
A42: ( s . z = v & dom v = f . z & rng v c= X ) by FUNCT_2:def 2;
A43: ( f . z = {} implies ( s . z = {} & h . z = {} ) ) by A40, A41, A42;

now

assume A44: f . z <> {} ; :: thesis: s . z = h . z
consider a being Element of f . z;
A45: [a,z] in dom (uncurry' s) by A28, A41, A42, A44, FUNCT_5:46;
then reconsider j = (curry' (uncurry' s)) . z as Function by FUNCT_5:28;
A46: ( j = (curry (~ (uncurry' s))) . z & ~ (uncurry' s) = uncurry s ) by Th13, FUNCT_5:def 5;
then A47: [z,a] in dom (uncurry s) by A45, FUNCT_4:43;
A48: dom j = dom v

proof

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

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in dom j or b in dom v )
assume b in dom j ; :: thesis: b in dom v
then [z,b] in dom (uncurry s) by A46, A47, Lm4;
then consider a1 being set , g1 being Function, a2 being set such that
A49: ( [z,b] = [a1,a2] & a1 in dom s & g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def 4;
( z = a1 & b = a2 ) by A49, ZFMISC_1:33;
hence b in dom v by A42, A49; :: thesis: verum

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in dom v or b in dom j )
assume b in dom v ; :: thesis: b in dom j
then [z,b] in dom (uncurry s) by A28, A41, A42, FUNCT_5:45;
hence b in dom j by A46, FUNCT_5:27; :: thesis: verum

end;

now

let b be set ; :: thesis: ( b in f . z implies j . b = v . b )
assume b in f . z ; :: thesis: j . b = v . b
then A50: [z,b] in dom (uncurry s) by A42, A46, A47, A48, Lm4;
then consider a1 being set , g1 being Function, a2 being set such that
A51: ( [z,b] = [a1,a2] & a1 in dom s & g1 = s . a1 & a2 in dom g1 ) by FUNCT_5:def 4;
( z = a1 & b = a2 & j . b = (uncurry s) . z,b ) by A46, A50, A51, FUNCT_5:27, ZFMISC_1:33;
hence j . b = v . b by A42, A51, FUNCT_5:45; :: thesis: verum

end;

then ( v = j & h . z = j ) by A40, A41, A42, A44, A48, FUNCT_1:9;
hence s . z = h . z by A42; :: thesis: verum

end;

hence s . z = h . z by A43; :: thesis: verum

end;

then h = s by A28, A40, FUNCT_1:9;
hence x in proj2 F by A27, A39, A40, FUNCT_1:def 5; :: thesis: verum