theorem Th49: :: ORDINAL3:49

for A, B being Ordinal st 1 in B & A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi