defpred S₁[ Ordinal] means ( $1 in W implies $1 *^ B1 in W );
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume that
A2: for C being Ordinal st C in A & C in W holds
C *^ B1 in W and
A3: A in W ; :: thesis: A *^ B1 in W
[:A,B1:] in W by A3, CLASSES2:61;
then A4: card [:A,B1:] in card W by CLASSES2:1;
A5: A *^ B1 c= W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A *^ B1 or x in W )
A6: B1 c= W by ORDINAL1:def 2;
assume A7: x in A *^ B1 ; :: thesis: x in W
then reconsider B = x as Ordinal ;
B1 <> {} by A7, ORDINAL2:38;
then consider C, D being Ordinal such that
A8: B = (C *^ B1) +^ D and
A9: D in B1 by ORDINAL3:47;
C *^ B1 c= B by A8, ORDINAL3:24;
then C *^ B1 in A *^ B1 by A7, ORDINAL1:12;
then A10: C in A by ORDINAL3:34;
A c= W by A3, ORDINAL1:def 2;
then reconsider CB = C *^ B1, D = D as Ordinal of W by A2, A9, A6, A10;
x = CB +^ D by A8;
hence x in W ; :: thesis: verum

end;

card (A *^ B1) = card [:A,B1:] by CARD_2:11;
hence A *^ B1 in W by A4, A5, CLASSES1:1; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
hence A1 *^ B1 is Ordinal of W ; :: thesis: verum