theorem :: ORDINAL4:26

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