let A, B be Ordinal; :: thesis: for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
let x1, x2 be set ; :: thesis: ( x1 <> x2 implies ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) )
assume A1: x1 <> x2 ; :: thesis: ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
defpred S₁[ set ] means $1 in A;
deffunc H₂( set ) -> set = [$1,x1];
deffunc H₃( Ordinal) -> set = [($1 -^ A),x2];
consider f being Function such that
A2: dom f = A +^ B and
A3: for x being Ordinal st x in A +^ B holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₃(x) ) ) from FINSET_1:sch 1();
thus A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent :: thesis: card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:])

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = A +^ B & rng f = [:A,{x1}:] \/ [:B,{x2}:] )
thus f is one-to-one :: thesis: ( dom f = A +^ B & rng f = [:A,{x1}:] \/ [:B,{x2}:] )

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 A4: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then reconsider C1 = x, C2 = y as Ordinal by A2;

per cases ( ( x in A & y in A ) or ( not x in A & not y in A ) or ( x in A & not y in A ) or ( not x in A & y in A ) ) ;

suppose ( x in A & y in A ) ; :: thesis: x = y

then ( f . C1 = [x,x1] & f . C2 = [y,x1] & [x,x1] `1 = C1 ) by A2, A3, A4, MCART_1:7;
hence x = y by A4, MCART_1:7; :: thesis: verum

end;

suppose ( not x in A & not y in A ) ; :: thesis: x = y

then ( f . x = [(C1 -^ A),x2] & f . y = [(C2 -^ A),x2] & [(C1 -^ A),x2] `1 = C1 -^ A & [(C2 -^ A),x2] `1 = C2 -^ A & A c= C1 & A c= C2 ) by A2, A3, A4, MCART_1:7, ORDINAL1:26;
then ( C1 -^ A = C2 -^ A & C1 = A +^ (C1 -^ A) & C2 = A +^ (C2 -^ A) ) by A4, ORDINAL3:def 6;
hence x = y ; :: thesis: verum

end;

suppose ( x in A & not y in A ) ; :: thesis: x = y

then ( f . x = [x,x1] & f . y = [(C2 -^ A),x2] & [x,x1] `2 = x1 & x1 <> x2 ) by A1, A2, A3, A4, MCART_1:7;
hence x = y by A4, MCART_1:7; :: thesis: verum

end;

suppose ( not x in A & y in A ) ; :: thesis: x = y

then ( f . y = [y,x1] & f . x = [(C1 -^ A),x2] & [y,x1] `2 = x1 & x1 <> x2 ) by A1, A2, A3, A4, MCART_1:7;
hence x = y by A4, MCART_1:7; :: thesis: verum

end;

end;

end;

thus dom f = A +^ B by A2; :: thesis: rng f = [:A,{x1}:] \/ [:B,{x2}:]
thus rng f c= [:A,{x1}:] \/ [:B,{x2}:] :: according to XBOOLE_0:def 10 :: thesis: [:A,{x1}:] \/ [:B,{x2}:] c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in [:A,{x1}:] \/ [:B,{x2}:] )
assume x in rng f ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]
then consider y being set such that
A6: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
A7: ( x1 in {x1} & x2 in {x2} ) by TARSKI:def 1;
reconsider C = y as Ordinal by A2, A6;

per cases ( y in A or not y in A ) ;

suppose y in A ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]

then ( x = [C,x1] & [C,x1] in [:A,{x1}:] ) by A2, A3, A6, A7, ZFMISC_1:106;
hence x in [:A,{x1}:] \/ [:B,{x2}:] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not y in A ; :: thesis: x in [:A,{x1}:] \/ [:B,{x2}:]

then A8: ( x = [(C -^ A),x2] & A c= C ) by A2, A3, A6, ORDINAL1:26;
then A +^ (C -^ A) = C by ORDINAL3:def 6;
then C -^ A in B by A2, A6, ORDINAL3:25;
then [(C -^ A),x2] in [:B,{x2}:] by A7, ZFMISC_1:106;
hence x in [:A,{x1}:] \/ [:B,{x2}:] by A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:A,{x1}:] \/ [:B,{x2}:] or x in rng f )
assume A9: x in [:A,{x1}:] \/ [:B,{x2}:] ; :: thesis: x in rng f

A10: now

assume x in [:A,{x1}:] ; :: thesis: x in rng f
then consider y, z being set such that
A11: ( y in A & z in {x1} & x = [y,z] ) by ZFMISC_1:103;
A13: A c= A +^ B by ORDINAL3:27;
then ( y in A +^ B & z = x1 ) by A11, TARSKI:def 1;
then x = f . y by A3, A11;
hence x in rng f by A2, A11, A13, FUNCT_1:def 5; :: thesis: verum

end;

now

assume x in [:B,{x2}:] ; :: thesis: x in rng f
then consider y, z being set such that
A14: ( y in B & z in {x2} & x = [y,z] ) by ZFMISC_1:103;
reconsider y = y as Ordinal by A14;
A c= A +^ y by ORDINAL3:27;
then A15: ( A +^ y = A +^ y & A +^ y in A +^ B & not A +^ y in A & (A +^ y) -^ A = y & z = x2 ) by A14, ORDINAL1:7, ORDINAL2:49, ORDINAL3:65, TARSKI:def 1;
then x = f . (A +^ y) by A3, A14;
hence x in rng f by A2, A15, FUNCT_1:def 5; :: thesis: verum

end;

hence x in rng f by A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;

hence card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) by CARD_1:21; :: thesis: verum