theorem :: ORDINAL5:67

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