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 & proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )
thus f is one-to-one :: thesis: ( proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )

proof

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

end;

thus dom f = [:X,Y:] by A1; :: thesis: proj2 f = [:Y,X:]
thus rng f c= [:Y,X:] :: according to XBOOLE_0:def 10 :: thesis: [:Y,X:] c= proj2 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
A6: y in dom f and
A7: x = f . y by FUNCT_1:def 5;
A8: y `2 in Y by A1, A6, MCART_1:10;
( x = [(y `2 ),(y `1 )] & y `1 in X ) by A1, A6, A7, MCART_1:10;
hence x in [:Y,X:] by A8, ZFMISC_1:106; :: thesis: verum

end;

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

end;

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