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

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

A9: now

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

end;

now

A12: (A *^ C) +^ {} = A *^ C by Th44;
assume A13: not A in D ; :: thesis: A *^ C in B *^ C
( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def 8;
then (A *^ C) +^ {} in (D *^ C) +^ C by A3, A6, A8, A13, Th49, ORDINAL1:21, ORDINAL1:34;
hence A *^ C in B *^ C by A8, A12, Th53; :: thesis: verum

end;

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

end;

now

A14: ( (A *^ C) +^ {} = A *^ C & (A *^ C) +^ {} in (A *^ C) +^ C ) by A2, Th44, Th49, ORDINAL1:21;
A15: (succ A) *^ C = (A *^ C) +^ C by Th53;
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:42;
then A18: succ A in B by A6, ORDINAL1:41;
then fi . (succ A) = (succ A) *^ C by A16;
then (succ A) *^ C in rng fi by A16, A18, FUNCT_1:def 5;
then A19: (succ A) *^ C c= union (sup (rng fi)) by Th27, ZFMISC_1:92;
B *^ C = union (sup fi) by A6, A17, A16, Th54
.= 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