let c, d be Cantor-component Ordinal; :: thesis: ( omega -exponent d in omega -exponent c implies <%c,d%> is Cantor-normal-form )
assume omega -exponent d in omega -exponent c ; :: thesis: <%c,d%> is Cantor-normal-form
then omega -exponent (<%d%> . 0) in omega -exponent (last ({} ^ <%c%>)) by AFINSQ_1:92;
then <%c%> ^ <%d%> is Cantor-normal-form by Th33;
hence <%c,d%> is Cantor-normal-form by AFINSQ_1:def 5; :: thesis: verum