theorem Th27: :: ORDINAL7:14

for A being finite Ordinal-Sequence
for a being Ordinal holds Sum^ (A | a) c= Sum^ A