let X1, X2, Y1, Y2 be set ; :: thesis: ( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
deffunc H₅( object ) -> object = [($1 `2),($1 `1)];
consider f being Function such that
A1: ( dom f = [:X1,X2:] \/ [:Y1,Y2:] & ( for x being object st x in [:X1,X2:] \/ [:Y1,Y2:] holds
f . x = H₅(x) ) ) from FUNCT_1:sch 3();
thus [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent :: thesis: card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:])

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = [:X1,X2:] \/ [:Y1,Y2:] & proj2 f = [:X2,X1:] \/ [:Y2,Y1:] )
thus f is one-to-one :: thesis: ( proj1 f = [:X1,X2:] \/ [:Y1,Y2:] & proj2 f = [:X2,X1:] \/ [:Y2,Y1:] )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f . x1 = f . x2 ; :: thesis: x1 = x2
( x1 in [:X1,X2:] or x1 in [:Y1,Y2:] ) by A1, A2, XBOOLE_0:def 3;
then A5: x1 = [(x1 `1),(x1 `2)] by MCART_1:21;
( x2 in [:X1,X2:] or x2 in [:Y1,Y2:] ) by A1, A3, XBOOLE_0:def 3;
then A6: x2 = [(x2 `1),(x2 `2)] by MCART_1:21;
A7: ( f . x1 = [(x1 `2),(x1 `1)] & f . x2 = [(x2 `2),(x2 `1)] ) by A1, A2, A3;
then x1 `1 = x2 `1 by A4, XTUPLE_0:1;
hence x1 = x2 by A4, A7, A5, A6, XTUPLE_0:1; :: thesis: verum

end;

thus dom f = [:X1,X2:] \/ [:Y1,Y2:] by A1; :: thesis: proj2 f = [:X2,X1:] \/ [:Y2,Y1:]
thus rng f c= [:X2,X1:] \/ [:Y2,Y1:] :: according to XBOOLE_0:def 10 :: thesis: [:X2,X1:] \/ [:Y2,Y1:] c= proj2 f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in [:X2,X1:] \/ [:Y2,Y1:] )
assume x in rng f ; :: thesis: x in [:X2,X1:] \/ [:Y2,Y1:]
then consider y being object such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def 3;
( y in [:X1,X2:] or y in [:Y1,Y2:] ) by A1, A8, XBOOLE_0:def 3;
then A10: ( ( y `1 in X1 & y `2 in X2 ) or ( y `1 in Y1 & y `2 in Y2 ) ) by MCART_1:10;
x = [(y `2),(y `1)] by A1, A8, A9;
then ( x in [:X2,X1:] or x in [:Y2,Y1:] ) by A10, ZFMISC_1:87;
hence x in [:X2,X1:] \/ [:Y2,Y1:] by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:X2,X1:] \/ [:Y2,Y1:] or x in proj2 f )
A11: ( [(x `2),(x `1)] `1 = x `2 & [(x `2),(x `1)] `2 = x `1 ) ;
assume x in [:X2,X1:] \/ [:Y2,Y1:] ; :: thesis: x in proj2 f
then A12: ( x in [:X2,X1:] or x in [:Y2,Y1:] ) by XBOOLE_0:def 3;
then ( ( x `1 in X2 & x `2 in X1 ) or ( x `1 in Y2 & x `2 in Y1 ) ) by MCART_1:10;
then ( [(x `2),(x `1)] in [:X1,X2:] or [(x `2),(x `1)] in [:Y1,Y2:] ) by ZFMISC_1:87;
then A13: [(x `2),(x `1)] in [:X1,X2:] \/ [:Y1,Y2:] by XBOOLE_0:def 3;
x = [(x `1),(x `2)] by A12, MCART_1:21;
then f . [(x `2),(x `1)] = x by A1, A13, A11;
hence x in proj2 f by A1, A13, FUNCT_1:def 3; :: thesis: verum

end;

hence card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) by CARD_1:5; :: thesis: verum