let c, d, e be Cantor-component Ordinal; :: thesis: ( omega -exponent d in omega -exponent c & omega -exponent e in omega -exponent d implies <%c,d,e%> is Cantor-normal-form )
assume that
A1: omega -exponent d in omega -exponent c and
A2: omega -exponent e in omega -exponent d ; :: thesis: <%c,d,e%> is Cantor-normal-form
A3: <%d,e%> is Cantor-normal-form by A2, Th35;
omega -exponent (<%d,e%> . 0) in omega -exponent (last ({} ^ <%c%>)) by A1, AFINSQ_1:92;
then <%c%> ^ <%d,e%> is Cantor-normal-form by A3, Th33;
hence <%c,d,e%> is Cantor-normal-form by AFINSQ_1:37; :: thesis: verum