let A, B be Ordinal; :: thesis: ( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
defpred S1[ object , object ] means ex O1, O2 being Ordinal st
( O1 = $1 `1 & O2 = $1 `2 & $2 = (O1 *^ B) +^ O2 );
A1: for x being object st x in [:A,B:] holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in [:A,B:] implies ex y being object st S1[x,y] )
assume x in [:A,B:] ; :: thesis: ex y being object st S1[x,y]
then ( x `1 in A & x `2 in B ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Ordinal ;
take (x1 *^ B) +^ x2 ; :: thesis: S1[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
A2: ( dom f = [:A,B:] & ( for x being object st x in [:A,B:] holds
S1[x,f . x] ) ) from CLASSES1:sch 1(A1);
 A3: [:A,B:],A *^ B are_equipotent
proof
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = [:A,B:] & proj2 f = A *^ B )
thus f is one-to-one :: thesis: ( proj1 f = [:A,B:] & proj2 f = A *^ B )
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 A4: ( x in dom f & y in dom f ) ; :: thesis: ( not f . x = f . y or x = y )
then A5: ( x `2 in B & y `2 in B ) by A2, MCART_1:10;
( x `1 in A & y `1 in A ) by A2, A4, MCART_1:10;
then reconsider x1 = x `1 , y1 = y `1 as Ordinal ;
assume A6: f . x = f . y ; :: thesis: x = y
A7: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A2, A4, MCART_1:21;
A8: ( ex O1, O2 being Ordinal st
( O1 = x `1 & O2 = x `2 & f . x = (O1 *^ B) +^ O2 ) & ex O3, O4 being Ordinal st
( O3 = y `1 & O4 = y `2 & f . y = (O3 *^ B) +^ O4 ) ) by A2, A4;
then x1 = y1 by A5, A6, ORDINAL3:48;
hence x = y by A7, A5, A8, A6, ORDINAL3:48; :: thesis: verum
end;
thus dom f = [:A,B:] by A2; :: thesis: proj2 f = A *^ B
thus rng f c= A *^ B :: according to XBOOLE_0:def 10 :: thesis: A *^ B c= proj2 f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in A *^ B )
A9: 1 *^ B = B by ORDINAL2:39;
assume y in rng f ; :: thesis: y in A *^ B
then consider x being object such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 3;
consider x1, x2 being Ordinal such that
A12: x1 = x `1 and
A13: ( x2 = x `2 & f . x = (x1 *^ B) +^ x2 ) by A2, A10;
x1 +^ 1 = succ x1 by ORDINAL2:31;
then A14: (x1 *^ B) +^ (1 *^ B) = (succ x1) *^ B by ORDINAL3:46;
succ x1 c= A by A12, A2, A10, MCART_1:10, ORDINAL1:21;
then A15: (x1 *^ B) +^ (1 *^ B) c= A *^ B by A14, ORDINAL2:41;
y in (x1 *^ B) +^ (1 *^ B) by A11, A13, A9, A2, A10, MCART_1:10, ORDINAL2:32;
hence y in A *^ B by A15; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A *^ B or y in proj2 f )
assume A16: y in A *^ B ; :: thesis: y in proj2 f
then reconsider C = y as Ordinal ;
A17: ( C = ((C div^ B) *^ B) +^ (C mod^ B) & [(C div^ B),(C mod^ B)] `1 = C div^ B ) by ORDINAL3:65;
( C div^ B in A & C mod^ B in B ) by A16, ORDINAL3:67;
then A18: [(C div^ B),(C mod^ B)] in [:A,B:] by ZFMISC_1:87;
then ( [(C div^ B),(C mod^ B)] `2 = C mod^ B & ex O1, O2 being Ordinal st
( 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 A2;
hence y in proj2 f by A2, A18, A17, FUNCT_1:def 3; :: 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 A3, CARD_1:5; :: thesis: verum