let A be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds
<%c%> ^ A is Cantor-normal-form
let c be Cantor-component Ordinal; :: thesis: ( omega -exponent (A . 0) in omega -exponent c implies <%c%> ^ A is Cantor-normal-form )
assume A0: omega -exponent (A . 0) in omega -exponent c ; :: thesis: <%c%> ^ A is Cantor-normal-form
set B = <%c%> ^ A;
A1: ( dom <%c%> = 1 & <%c%> . 0 = c ) by AFINSQ_1:def 5;
then A2: dom (<%c%> ^ A) = 1 +^ (dom A) by ORDINAL4:def 1;

hereby :: according to ORDINAL5:def 11 :: thesis: for a, b being ordinal number st a in b & b in dom (<%c%> ^ A) holds
omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)

let a be ordinal number ; :: thesis: ( a in dom (<%c%> ^ A) implies (<%c%> ^ A) . b₁ is Cantor-component )
assume A3: a in dom (<%c%> ^ A) ; :: thesis: (<%c%> ^ A) . b₁ is Cantor-component

per cases ( a in 1 or ex b being ordinal number st
( b in dom A & a = 1 +^ b ) ) by A2, A3, ORDINAL3:42;

suppose A4: a in 1 ; :: thesis: (<%c%> ^ A) . b₁ is Cantor-component

then a = 0 by ORDINAL3:18, TARSKI:def 1;
hence (<%c%> ^ A) . a is Cantor-component by A1, A4, ORDINAL4:def 1; :: thesis: verum

end;

suppose ex b being ordinal number st
( b in dom A & a = 1 +^ b ) ; :: thesis: (<%c%> ^ A) . b₁ is Cantor-component

then consider b being ordinal number such that
A5: ( b in dom A & a = 1 +^ b ) ;
(<%c%> ^ A) . a = A . b by A1, A5, ORDINAL4:def 1;
hence (<%c%> ^ A) . a is Cantor-component by A5, CNF; :: thesis: verum

end;

end;

end;

let a, b be ordinal number ; :: thesis: ( a in b & b in dom (<%c%> ^ A) implies omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) )
assume A6: ( a in b & b in dom (<%c%> ^ A) ) ; :: thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)

per cases ( not a in 1 or a in 1 ) ;

suppose not a in 1 ; :: thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)

then B1: 1 c= a by ORDINAL1:26;
then B2: ( 1 in b & a in dom (<%c%> ^ A) & (1 +^ (dom A)) -^ 1 = dom A ) by A6, ORDINAL1:19, ORDINAL1:22, ORDINAL3:65;
then B3: ( b -^ 1 in dom A & a -^ 1 in dom A & a -^ 1 in b -^ 1 ) by B1, A2, A6, ORDINAL3:66;
( b = 1 +^ (b -^ 1) & a = 1 +^ (a -^ 1) ) by B1, B2, ORDINAL3:60, ORDINAL3:def 6;
then ( (<%c%> ^ A) . a = A . (a -^ 1) & (<%c%> ^ A) . b = A . (b -^ 1) ) by A1, B3, ORDINAL4:def 1;
hence omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by B3, CNF; :: thesis: verum

end;

suppose a in 1 ; :: thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)

then C1: ( (<%c%> ^ A) . a = <%c%> . a & a = 0 ) by A1, TARSKI:def 1, ORDINAL3:18, ORDINAL4:def 1;
then C2: succ 0 c= b by A6, ORDINAL1:33;
then b -^ 1 in (1 +^ (dom A)) -^ 1 by A2, A6, ORDINAL3:66;
then C3: ( b -^ 1 in dom A & b = 1 +^ (b -^ 1) ) by C2, ORDINAL3:def 6, ORDINAL3:65;
then C4: (<%c%> ^ A) . b = A . (b -^ 1) by A1, ORDINAL4:def 1;
( 0 in dom A & ( b -^ 1 = 0 or 0 in b -^ 1 ) ) by ORDINAL3:10;
then ( omega -exponent (A . 0) = omega -exponent (A . (b -^ 1)) or omega -exponent (A . (b -^ 1)) in omega -exponent (A . 0) ) by C3, CNF;
hence omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by A0, A1, C1, C4, ORDINAL1:19; :: thesis: verum

end;

end;