theorem Th84: :: ORDINAL7:71

for A, B being finite Ordinal-Sequence st A ^ B is Cantor-normal-form holds
(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)