theorem Th29: :: ORDINAL2:29

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 = A +^ C ) holds
A +^ B = sup fi