theorem Th56: :: ORDINAL5:56

for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A