A1: now :: thesis: for a being Ordinal st a in dom <%c%> holds
<%c%> . a is Cantor-component
let a be Ordinal; :: thesis: ( a in dom <%c%> implies <%c%> . a is Cantor-component )
assume a in dom <%c%> ; :: thesis: <%c%> . a is Cantor-component
then a in Segm 1 by AFINSQ_1:33;
then a = 0 by CARD_1:49, TARSKI:def 1;
hence <%c%> . a is Cantor-component ; :: thesis: verum
end;
now :: thesis: for a, b being Ordinal st a in b & b in dom <%c%> holds
omega -exponent (<%c%> . b) in omega -exponent (<%c%> . a)
let a, b be Ordinal; :: thesis: ( a in b & b in dom <%c%> implies omega -exponent (<%c%> . b) in omega -exponent (<%c%> . a) )
assume A2: ( a in b & b in dom <%c%> ) ; :: thesis: omega -exponent (<%c%> . b) in omega -exponent (<%c%> . a)
then b in Segm 1 by AFINSQ_1:33;
hence omega -exponent (<%c%> . b) in omega -exponent (<%c%> . a) by A2, CARD_1:49, TARSKI:def 1; :: thesis: verum
end;
hence <%c%> is Cantor-normal-form by A1, ORDINAL5:def 11; :: thesis: verum