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

proof

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

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 )] & f . x = [(x `2 ),(x `1 )] & f . y = [(y `2 ),(y `1 )] ) by A1, MCART_1:23;
assume f . x = f . y ; :: thesis: x = y
then ( x `1 = y `1 & x `2 = y `2 ) by A2, ZFMISC_1:33;
hence x = y by A2; :: thesis: verum

end;

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

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:Y,X:] or x in rng f )
assume x in [:Y,X:] ; :: thesis: x in rng f
then A4: ( x = [(x `1 ),(x `2 )] & x `1 in Y & x `2 in X ) by MCART_1:10, MCART_1:23;
then ( [(x `2 ),(x `1 )] in [:X,Y:] & [(x `2 ),(x `1 )] `1 = x `2 & [(x `2 ),(x `1 )] `2 = x `1 ) by MCART_1:7, ZFMISC_1:106;
then ( f . [(x `2 ),(x `1 )] in rng f & f . [(x `2 ),(x `1 )] = x ) by A1, A4, FUNCT_1:def 5;
hence x in rng f ; :: thesis: verum

end;

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