let A, B, C be Ordinal; :: thesis: ( C <> 0 & A in B implies A *^ C in B *^ C )
A1: 0 c= C ;
defpred S₁[ Ordinal] means ( A in $1 implies A *^ C in $1 *^ C );
assume C <> 0 ; :: thesis: ( not A in B or A *^ C in B *^ C )
then A2: 0 c< C by A1;
then A3: 0 in C by ORDINAL1:11;
A4: for B being Ordinal st ( for D being Ordinal st D in B holds
S₁[D] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( ( for D being Ordinal st D in B holds
S₁[D] ) implies S₁[B] )
assume that
A5: for D being Ordinal st D in B & A in D holds
A *^ C in D *^ C and
A6: A in B ; :: thesis: A *^ C in B *^ C

A7: now :: thesis: ( ex D being Ordinal st B = succ D implies A *^ C in B *^ C )

given D being Ordinal such that A8: B = succ D ; :: thesis: A *^ C in B *^ C

A9: now :: thesis: ( A in D implies A *^ C in B *^ C )

assume A in D ; :: thesis: A *^ C in B *^ C
then A10: A *^ C in D *^ C by A5, A8, ORDINAL1:6;
A11: (D *^ C) +^ 0 in (D *^ C) +^ C by A2, Th32, ORDINAL1:11;
( (D *^ C) +^ C = (succ D) *^ C & (D *^ C) +^ 0 = D *^ C ) by Th27, Th36;
hence A *^ C in B *^ C by A8, A10, A11, ORDINAL1:10; :: thesis: verum

end;

now :: thesis: ( not A in D implies A *^ C in B *^ C )

A12: (A *^ C) +^ 0 = A *^ C by Th27;
assume A13: not A in D ; :: thesis: A *^ C in B *^ C
( A c< D iff ( A c= D & A <> D ) ) ;
then (A *^ C) +^ 0 in (D *^ C) +^ C by A3, A6, A8, A13, Th32, ORDINAL1:11, ORDINAL1:22;
hence A *^ C in B *^ C by A8, A12, Th36; :: thesis: verum

end;

hence A *^ C in B *^ C by A9; :: thesis: verum

end;

now :: thesis: ( ( for D being Ordinal holds B <> succ D ) implies A *^ C in B *^ C )

A14: ( (A *^ C) +^ 0 = A *^ C & (A *^ C) +^ 0 in (A *^ C) +^ C ) by A2, Th27, Th32, ORDINAL1:11;
A15: (succ A) *^ C = (A *^ C) +^ C by Th36;
deffunc H₁( Ordinal) -> Ordinal = $1 *^ C;
consider fi being Ordinal-Sequence such that
A16: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
assume for D being Ordinal holds B <> succ D ; :: thesis: A *^ C in B *^ C
then A17: B is limit_ordinal by ORDINAL1:29;
then A18: succ A in B by A6, ORDINAL1:28;
then fi . (succ A) = (succ A) *^ C by A16;
then (succ A) *^ C in rng fi by A16, A18, FUNCT_1:def 3;
then A19: (succ A) *^ C c= union (sup (rng fi)) by Th19, ZFMISC_1:74;
B *^ C = union (sup fi) by A6, A17, A16, Th37
.= union (sup (rng fi)) ;
hence A *^ C in B *^ C by A19, A14, A15; :: thesis: verum

end;

hence A *^ C in B *^ C by A7; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A4);
hence ( not A in B or A *^ C in B *^ C ) ; :: thesis: verum