theorem Th24: :: ORDINAL7:11

for A, B being finite Ordinal-Sequence holds Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)