theorem Th41: :: ORDINAL7:28

for A being finite Ordinal-Sequence
for b being Ordinal st ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b)