theorem Th45: :: ORDINAL7:32

for A, B being Cantor-normal-form Ordinal-Sequence st Sum^ A = Sum^ B holds
A = B