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