for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>