theorem Th37: :: ORDINAL2:37

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