let C, A, B be Ordinal; :: thesis: ( C <> {} & A in B implies A *^ C in B *^ C )
assume A1: C <> {} ; :: thesis: ( not A in B or A *^ C in B *^ C )
{} c= C ;
then B2: {} c< C by A1, XBOOLE_0:def 8;
then A2: {} in C by ORDINAL1:21;
defpred S₁[ Ordinal] means ( A in $1 implies A *^ C in $1 *^ C );
A3: 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
A4: for D being Ordinal st D in B & A in D holds
A *^ C in D *^ C and
A5: A in B ; :: thesis: A *^ C in B *^ C

A6: now

given D being Ordinal such that A7: B = succ D ; :: thesis: A *^ C in B *^ C
A8: D in B by A7, ORDINAL1:10;

A9: now

A10: ( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def 8;
assume not A in D ; :: thesis: A *^ C in B *^ C
then ( (A *^ C) +^ {} = A *^ C & (A *^ C) +^ {} in (D *^ C) +^ C & (D *^ C) +^ C = (succ D) *^ C ) by A2, A5, A7, A10, Th44, Th49, Th53, ORDINAL1:21, ORDINAL1:34;
hence A *^ C in B *^ C by A7; :: thesis: verum

end;

now

assume A in D ; :: thesis: A *^ C in B *^ C
then ( A *^ C in D *^ C & (D *^ C) +^ C = (succ D) *^ C & (D *^ C) +^ {} = D *^ C & (D *^ C) +^ {} in (D *^ C) +^ C ) by A2, A4, A8, Th44, Th49, Th53;
hence A *^ C in B *^ C by A7, ORDINAL1:19; :: thesis: verum

end;

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

end;

now

assume for D being Ordinal holds B <> succ D ; :: thesis: A *^ C in B *^ C
then A11: B is limit_ordinal by ORDINAL1:42;
deffunc H₁( Ordinal) -> Ordinal = $1 *^ C;
consider fi being Ordinal-Sequence such that
A12: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A13: B *^ C = union (sup fi) by A5, A11, A12, Th54
.= union (sup (rng fi)) ;
A14: succ A in B by A5, A11, ORDINAL1:41;
then fi . (succ A) = (succ A) *^ C by A12;
then (succ A) *^ C in rng fi by A12, A14, FUNCT_1:def 5;
then A15: (succ A) *^ C c= union (sup (rng fi)) by Th27, ZFMISC_1:92;
( (A *^ C) +^ {} = A *^ C & (A *^ C) +^ {} in (A *^ C) +^ C & (succ A) *^ C = (A *^ C) +^ C ) by B2, Th44, Th49, Th53, ORDINAL1:21;
hence A *^ C in B *^ C by A13, A15; :: thesis: verum

end;

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

end;

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