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 H₁( 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 = H₁(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 8 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
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 ZFMISC_1:33;

now

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:23;
A14: g2 . x in rng g2 by A9, A12, FUNCT_1:def 5;
then A15: g2 . x = [((g2 . x) `1 ),((g2 . x) `2 )] by A10, MCART_1:23;
A16: g1 . x in rng g1 by A6, A12, FUNCT_1:def 5;
then A17: g1 . x = [((g1 . x) `1 ),((g1 . x) `2 )] by A7, MCART_1:23;
( (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 5, FUNCT_3:def 6;
( (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 5, FUNCT_3:def 6;
( ((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:23;
hence g1 . x = g2 . x by A9, A11, A12, A13, A17, A15, A19, A18, FUNCT_1:23; :: thesis: verum

end;

hence x1 = x2 by A5, A6, A8, A9, FUNCT_1:9; :: 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 5;
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;
( rng ((pr1 X,Y) * g) c= rng (pr1 X,Y) & rng (pr1 X,Y) c= X ) by FUNCT_3:59, RELAT_1:45;
then A24: rng ((pr1 X,Y) * g) c= X by XBOOLE_1:1;
( rng ((pr2 X,Y) * g) c= rng (pr2 X,Y) & rng (pr2 X,Y) c= Y ) by FUNCT_3:61, RELAT_1:45;
then A25: rng ((pr2 X,Y) * g) c= Y by XBOOLE_1:1;
dom (pr2 X,Y) = [:X,Y:] by FUNCT_3:def 6;
then dom ((pr2 X,Y) * g) = Z by A23, RELAT_1:46;
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 5;
then dom ((pr1 X,Y) * g) = Z by A23, RELAT_1:46;
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:106; :: 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:23;
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:71, ZFMISC_1:119;
then A36: rng <:g1,g2:> c= [:X,Y:] by XBOOLE_1:1;
dom <:g1,g2:> = Z /\ Z by A34, A31, FUNCT_3:def 8;
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:72;
then f . <:g1,g2:> = [g1,g2] by A1, A37;
hence x in proj2 f by A1, A29, A33, A30, A37, FUNCT_1:def 5; :: thesis: verum

end;

hence card (Funcs Z,[:X,Y:]) = card [:(Funcs Z,X),(Funcs Z,Y):] by CARD_1:21; :: thesis: verum