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₃( set ) -> set = [(($1 `1 ) `1 ),[(($1 `1 ) `2 ),($1 `2 )]];
consider f being Function such that
A1: ( dom f = [:[:X,Y:],Z:] & ( for x being set 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 & dom f = [:[:X,Y:],Z:] & rng f = [:X,[:Y,Z:]:] )
thus f is one-to-one :: thesis: ( dom f = [:[:X,Y:],Z:] & rng f = [:X,[:Y,Z:]:] )

proof

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

end;

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

proof

let x be set ; :: 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 set such that
A4: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
A5: ( y = [(y `1 ),(y `2 )] & y `1 in [:X,Y:] & y `2 in Z ) by A1, A4, MCART_1:10, MCART_1:23;
then A6: ( y `1 = [((y `1 ) `1 ),((y `1 ) `2 )] & (y `1 ) `1 in X & (y `1 ) `2 in Y & x = [((y `1 ) `1 ),[((y `1 ) `2 ),(y `2 )]] ) by A1, A4, MCART_1:10, MCART_1:23;
then [((y `1 ) `2 ),(y `2 )] in [:Y,Z:] by A5, ZFMISC_1:106;
hence x in [:X,[:Y,Z:]:] by A6, ZFMISC_1:106; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:X,[:Y,Z:]:] or x in rng f )
assume x in [:X,[:Y,Z:]:] ; :: thesis: x in rng f
then A7: ( x = [(x `1 ),(x `2 )] & x `1 in X & x `2 in [:Y,Z:] ) by MCART_1:10, MCART_1:23;
then A8: ( x `2 = [((x `2 ) `1 ),((x `2 ) `2 )] & (x `2 ) `1 in Y & (x `2 ) `2 in Z ) by MCART_1:10, MCART_1:23;
then A9: ( [(x `1 ),((x `2 ) `1 )] in [:X,Y:] & [(x `1 ),((x `2 ) `1 )] `1 = x `1 & [(x `1 ),((x `2 ) `1 )] `2 = (x `2 ) `1 ) by A7, MCART_1:7, ZFMISC_1:106;
then A10: ( [[(x `1 ),((x `2 ) `1 )],((x `2 ) `2 )] in [:[:X,Y:],Z:] & [[(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 ) by A8, MCART_1:7, ZFMISC_1:106;
then x = f . [[(x `1 ),((x `2 ) `1 )],((x `2 ) `2 )] by A1, A7, A8, A9;
hence x in rng f by A1, A10, FUNCT_1:def 5; :: thesis: verum

end;

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