let X, Y, Z be set ; :: thesis: ( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
deffunc H₃( object ) -> object = [(($1 `1) `1),[(($1 `1) `2),($1 `2)]];
consider f being Function such that
A1: ( dom f = [:[:X,Y:],Z:] & ( for x being object st x in [:[:X,Y:],Z:] holds
f . x = H₃(x) ) ) from FUNCT_1:sch 3();
thus [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent :: thesis: card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:]

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = [:[:X,Y:],Z:] & proj2 f = [:X,[:Y,Z:]:] )
thus f is one-to-one :: thesis: ( proj1 f = [:[:X,Y:],Z:] & proj2 f = [:X,[:Y,Z:]:] )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A2: x in dom f and
A3: y in dom f ; :: thesis: ( not f . x = f . y or x = y )
assume A4: f . x = f . y ; :: thesis: x = y
A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A1, A2, A3, MCART_1:21;
x `1 in [:X,Y:] by A1, A2, MCART_1:10;
then A6: x `1 = [((x `1) `1),((x `1) `2)] by MCART_1:21;
A7: ( f . x = [((x `1) `1),[((x `1) `2),(x `2)]] & f . y = [((y `1) `1),[((y `1) `2),(y `2)]] ) by A1, A2, A3;
then A8: (x `1) `1 = (y `1) `1 by A4, XTUPLE_0:1;
y `1 in [:X,Y:] by A1, A3, MCART_1:10;
then A9: y `1 = [((y `1) `1),((y `1) `2)] by MCART_1:21;
A10: [((x `1) `2),(x `2)] = [((y `1) `2),(y `2)] by A7, A4, XTUPLE_0:1;
then (x `1) `2 = (y `1) `2 by XTUPLE_0:1;
hence x = y by A5, A8, A10, A6, A9, XTUPLE_0:1; :: thesis: verum

end;

thus dom f = [:[:X,Y:],Z:] by A1; :: thesis: proj2 f = [:X,[:Y,Z:]:]
thus rng f c= [:X,[:Y,Z:]:] :: according to XBOOLE_0:def 10 :: thesis: [:X,[:Y,Z:]:] c= proj2 f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in [:X,[:Y,Z:]:] )
assume x in rng f ; :: thesis: x in [:X,[:Y,Z:]:]
then consider y being object such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def 3;
A13: y `1 in [:X,Y:] by A1, A11, MCART_1:10;
then A14: (y `1) `2 in Y by MCART_1:10;
y `2 in Z by A1, A11, MCART_1:10;
then A15: [((y `1) `2),(y `2)] in [:Y,Z:] by A14, ZFMISC_1:87;
A16: (y `1) `1 in X by A13, MCART_1:10;
x = [((y `1) `1),[((y `1) `2),(y `2)]] by A1, A11, A12;
hence x in [:X,[:Y,Z:]:] by A16, A15, ZFMISC_1:87; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:X,[:Y,Z:]:] or x in proj2 f )
A17: ( [(x `1),((x `2) `1)] `1 = x `1 & [(x `1),((x `2) `1)] `2 = (x `2) `1 ) ;
A18: ( [[(x `1),((x `2) `1)],((x `2) `2)] `1 = [(x `1),((x `2) `1)] & [[(x `1),((x `2) `1)],((x `2) `2)] `2 = (x `2) `2 ) ;
assume A19: x in [:X,[:Y,Z:]:] ; :: thesis: x in proj2 f
then A20: x `2 in [:Y,Z:] by MCART_1:10;
then A21: (x `2) `1 in Y by MCART_1:10;
A22: (x `2) `2 in Z by A20, MCART_1:10;
x `1 in X by A19, MCART_1:10;
then A23: [(x `1),((x `2) `1)] in [:X,Y:] by A21, ZFMISC_1:87;
then A24: [[(x `1),((x `2) `1)],((x `2) `2)] in [:[:X,Y:],Z:] by A22, ZFMISC_1:87;
A25: x `2 = [((x `2) `1),((x `2) `2)] by A20, MCART_1:21;
x = [(x `1),(x `2)] by A19, MCART_1:21;
then x = f . [[(x `1),((x `2) `1)],((x `2) `2)] by A1, A25, A17, A23, A18, A22, ZFMISC_1:87;
hence x in proj2 f by A1, A24, FUNCT_1:def 3; :: thesis: verum

end;

hence card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] by CARD_1:5; :: thesis: verum