let X, Y be set ; :: thesis: ( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
deffunc H3( object ) -> object = [($1 `2),($1 `1)];
consider f being Function such that
A1: ( dom f = [:X,Y:] & ( for x being object st x in [:X,Y:] holds
f . x = H3(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, 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 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:21;
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, XTUPLE_0:1;
hence x = y by A3, A5, A4, XTUPLE_0:1; :: 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 object ; :: 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 object such that
A6: y in dom f and
A7: x = f . y by FUNCT_1:def 3;
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:87; :: thesis: verum
end;
let x be object ; :: 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 ) ;
assume A10: x in [:Y,X:] ; :: thesis: x in proj2 f
then A11: x = [(x `1),(x `2)] by MCART_1:21;
A12: ( x `1 in Y & x `2 in X ) by A10, MCART_1:10;
then [(x `2),(x `1)] in [:X,Y:] by ZFMISC_1:87;
then f . [(x `2),(x `1)] in rng f by A1, FUNCT_1:def 3;
hence x in proj2 f by A1, A11, A12, A9, ZFMISC_1:87; :: thesis: verum
end;
hence card [:X,Y:] = card [:Y,X:] by CARD_1:5; :: thesis: verum