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₅( set ) -> set = [($1 `2 ),($1 `1 )];
consider f being Function such that
A1: ( dom f = [:X1,X2:] \/ [:Y1,Y2:] & ( for x being set 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 & dom f = [:X1,X2:] \/ [:Y1,Y2:] & rng f = [:X2,X1:] \/ [:Y2,Y1:] )
thus f is one-to-one :: thesis: ( dom f = [:X1,X2:] \/ [:Y1,Y2:] & rng f = [:X2,X1:] \/ [:Y2,Y1:] )

proof

let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in dom f or not b₁ in dom f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A2: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then ( ( x1 in [:X1,X2:] or x1 in [:Y1,Y2:] ) & f . x1 = [(x1 `2 ),(x1 `1 )] & ( x2 in [:X1,X2:] or x2 in [:Y1,Y2:] ) & f . x2 = [(x2 `2 ),(x2 `1 )] ) by A1, XBOOLE_0:def 3;
then ( x1 = [(x1 `1 ),(x1 `2 )] & x2 = [(x2 `1 ),(x2 `2 )] & x1 `1 = x2 `1 & x1 `2 = x2 `2 ) by A2, MCART_1:23, ZFMISC_1:33;
hence x1 = x2 ; :: thesis: verum

end;

thus dom f = [:X1,X2:] \/ [:Y1,Y2:] by A1; :: thesis: rng 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= rng f

proof

let x be set ; :: 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 set such that
A3: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
( y in [:X1,X2:] or y in [:Y1,Y2:] ) by A1, A3, XBOOLE_0:def 3;
then ( ( ( y `1 in X1 & y `2 in X2 ) or ( y `1 in Y1 & y `2 in Y2 ) ) & x = [(y `2 ),(y `1 )] ) by A1, A3, MCART_1:10;
then ( x in [:X2,X1:] or x in [:Y2,Y1:] ) by ZFMISC_1:106;
hence x in [:X2,X1:] \/ [:Y2,Y1:] by XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

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