let X, Y be set ; :: thesis: [:X,Y:],[:(card X),Y:] are_equipotent
X, card X are_equipotent by CARD_1:def 5;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
deffunc H₃( set ) -> set = [(f . ($1 `1 )),($1 `2 )];
consider g being Function such that
A4: ( dom g = [:X,Y:] & ( for x being set st x in [:X,Y:] holds
g . x = H₃(x) ) ) from FUNCT_1:sch 3();
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & proj1 g = [:X,Y:] & proj2 g = [:(card X),Y:] )
thus g is one-to-one :: thesis: ( proj1 g = [:X,Y:] & proj2 g = [:(card X),Y:] )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume A5: ( x in dom g & y in dom g ) ; :: thesis: ( not g . x = g . y or x = y )
then A6: ( x `1 in X & y `1 in X ) by A4, MCART_1:10;
assume A7: g . x = g . y ; :: thesis: x = y
( g . x = [(f . (x `1 )),(x `2 )] & g . y = [(f . (y `1 )),(y `2 )] ) by A4, A5;
then A8: ( f . (x `1 ) = f . (y `1 ) & x `2 = y `2 ) by A7, ZFMISC_1:33;
( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] ) by A4, A5, MCART_1:23;
hence x = y by A1, A2, A6, A8, FUNCT_1:def 8; :: thesis: verum

end;

thus dom g = [:X,Y:] by A4; :: thesis: proj2 g = [:(card X),Y:]
thus rng g c= [:(card X),Y:] :: according to XBOOLE_0:def 10 :: thesis: [:(card X),Y:] c= proj2 g

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in [:(card X),Y:] )
assume y in rng g ; :: thesis: y in [:(card X),Y:]
then consider x being set such that
A9: x in dom g and
A10: y = g . x by FUNCT_1:def 5;
x `1 in X by A4, A9, MCART_1:10;
then A11: f . (x `1 ) in card X by A2, A3, FUNCT_1:def 5;
( y = [(f . (x `1 )),(x `2 )] & x `2 in Y ) by A4, A9, A10, MCART_1:10;
hence y in [:(card X),Y:] by A11, ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in [:(card X),Y:] or y in proj2 g )
assume A12: y in [:(card X),Y:] ; :: thesis: y in proj2 g
then y `1 in card X by MCART_1:10;
then consider x being set such that
A13: x in X and
A14: y `1 = f . x by A2, A3, FUNCT_1:def 5;
A15: y = [(y `1 ),(y `2 )] by A12, MCART_1:23;
y `2 in Y by A12, MCART_1:10;
then A16: [x,(y `2 )] in [:X,Y:] by A13, ZFMISC_1:106;
( [x,(y `2 )] `1 = x & [x,(y `2 )] `2 = y `2 ) by MCART_1:7;
then g . [x,(y `2 )] = y by A4, A15, A14, A16;
hence y in proj2 g by A4, A16, FUNCT_1:def 5; :: thesis: verum