let X, Y be set ; :: thesis: [:X,Y:],[:(card X),Y:] are_equipotent
consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def 2, WELLORD2:def 4;
deffunc H₃( object ) -> object = [(f . ($1 `1)),($1 `2)];
consider g being Function such that
A4: ( dom g = [:X,Y:] & ( for x being object 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, y be object ; :: according to FUNCT_1:def 4 :: 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, XTUPLE_0:1;
( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A4, A5, MCART_1:21;
hence x = y by A1, A2, A6, A8; :: 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 object ; :: 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 object such that
A9: x in dom g and
A10: y = g . x by FUNCT_1:def 3;
x `1 in X by A4, A9, MCART_1:10;
then A11: f . (x `1) in card X by A2, A3, FUNCT_1:def 3;
( 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:87; :: thesis: verum

end;

let y be object ; :: 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 object such that
A13: x in X and
A14: y `1 = f . x by A2, A3, FUNCT_1:def 3;
A15: y = [(y `1),(y `2)] by A12, MCART_1:21;
A16: y `2 in Y by A12, MCART_1:10;
then A17: [x,(y `2)] in [:X,Y:] by A13, ZFMISC_1:87;
( [x,(y `2)] `1 = x & [x,(y `2)] `2 = y `2 ) ;
then g . [x,(y `2)] = y by A4, A15, A14, A16, A13, ZFMISC_1:87;
hence y in proj2 g by A4, A17, FUNCT_1:def 3; :: thesis: verum