theorem :: ORDINAL5:69

for a being Ordinal ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A