let A, B be Ordinal; :: thesis: ( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
defpred S₁[ set , set ] means ex O1, O2 being Ordinal st
( O1 = $1 `1 & O2 = $1 `2 & $2 = (O1 *^ B) +^ O2 );
A2: for x being set st x in [:A,B:] holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in [:A,B:] implies ex y being set st S₁[x,y] )
assume x in [:A,B:] ; :: thesis: ex y being set st S₁[x,y]
then ( x = [(x `1 ),(x `2 )] & x `1 in A & x `2 in B ) by MCART_1:10, MCART_1:23;
then reconsider x1 = x `1 , x2 = x `2 as Ordinal ;
take (x1 *^ B) +^ x2 ; :: thesis: S₁[x,(x1 *^ B) +^ x2]
take x1 ; :: thesis: ex O2 being Ordinal st
( x1 = x `1 & O2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ O2 )
take x2 ; :: thesis: ( x1 = x `1 & x2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ x2 )
thus ( x1 = x `1 & x2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ x2 ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = [:A,B:] & ( for x being set st x in [:A,B:] holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
A4: [:A,B:],A *^ B are_equipotent

proof

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = [:A,B:] & rng f = A *^ B )
thus f is one-to-one :: thesis: ( dom f = [:A,B:] & rng f = A *^ B )

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 A5: ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
then A6: ( x = [(x `1 ),(x `2 )] & y = [(y `1 ),(y `2 )] & x `1 in A & x `2 in B & y `1 in A & y `2 in B ) by A3, MCART_1:10, MCART_1:23;
then reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Ordinal ;
consider O1, O2 being Ordinal such that
A7: ( O1 = x `1 & O2 = x `2 & f . x = (O1 *^ B) +^ O2 ) by A3, A5;
consider O3, O4 being Ordinal such that
A8: ( O3 = y `1 & O4 = y `2 & f . y = (O3 *^ B) +^ O4 ) by A3, A5;
assume f . x = f . y ; :: thesis: x = y
then ( x1 = y1 & x2 = y2 ) by A6, A7, A8, ORDINAL3:56;
hence x = y by A6; :: thesis: verum

end;

thus dom f = [:A,B:] by A3; :: thesis: rng f = A *^ B
thus rng f c= A *^ B :: according to XBOOLE_0:def 10 :: thesis: A *^ B c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in A *^ B )
assume y in rng f ; :: thesis: y in A *^ B
then consider x being set such that
A9: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
A10: ( x `1 in A & x `2 in B ) by A3, A9, MCART_1:10;
consider x1, x2 being Ordinal such that
A11: ( x1 = x `1 & x2 = x `2 & f . x = (x1 *^ B) +^ x2 ) by A3, A9;
( y = (x1 *^ B) +^ x2 & 1 *^ B = B & x1 +^ 1 = succ x1 ) by A9, A11, ORDINAL2:48, ORDINAL2:56;
then A12: ( y in (x1 *^ B) +^ (1 *^ B) & (x1 *^ B) +^ (1 *^ B) = (succ x1) *^ B & succ x1 c= A ) by A10, A11, ORDINAL1:33, ORDINAL2:49, ORDINAL3:54;
then (x1 *^ B) +^ (1 *^ B) c= A *^ B by ORDINAL2:58;
hence y in A *^ B by A12; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A *^ B or y in rng f )
assume A13: y in A *^ B ; :: thesis: y in rng f
then reconsider C = y as Ordinal ;
A14: ( C = ((C div^ B) *^ B) +^ (C mod^ B) & C div^ B in A & C mod^ B in B ) by A13, ORDINAL3:78, ORDINAL3:80;
then A15: ( [(C div^ B),(C mod^ B)] in [:A,B:] & [(C div^ B),(C mod^ B)] `1 = C div^ B & [(C div^ B),(C mod^ B)] `2 = C mod^ B & C div^ B = C div^ B & C mod^ B = C mod^ B ) by MCART_1:7, ZFMISC_1:106;
then consider O1, O2 being Ordinal such that
A16: ( O1 = [(C div^ B),(C mod^ B)] `1 & O2 = [(C div^ B),(C mod^ B)] `2 & f . [(C div^ B),(C mod^ B)] = (O1 *^ B) +^ O2 ) by A3;
thus y in rng f by A3, A14, A15, A16, FUNCT_1:def 5; :: thesis: verum

end;

hence A *^ B,[:A,B:] are_equipotent ; :: thesis: card (A *^ B) = card [:A,B:]
thus card (A *^ B) = card [:A,B:] by A4, CARD_1:21; :: thesis: verum