let c, d, e be Cantor-component Ordinal; ( 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
; <%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; verum