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 A1: omega -exponent (A . 0) in omega -exponent c ; :: thesis: <%c%> ^ A is Cantor-normal-form
set B = <%c%> ^ A;
A2: ( dom <%c%> = 1 & <%c%> . 0 = c ) by AFINSQ_1:def 4;
then A3: dom (<%c%> ^ A) = 1 +^ (dom A) by ORDINAL4:def 1;

hereby :: according to ORDINAL5:def 11 :: thesis: for a, b being Ordinal 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; :: thesis: ( a in dom (<%c%> ^ A) implies (<%c%> ^ A) . b₁ is Cantor-component )
assume A4: a in dom (<%c%> ^ A) ; :: thesis: (<%c%> ^ A) . b₁ is Cantor-component

per cases ( a in 1 or ex b being Ordinal st
( b in dom A & a = 1 +^ b ) ) by A3, A4, ORDINAL3:38;

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

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

end;

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

then consider b being Ordinal such that
A6: ( b in dom A & a = 1 +^ b ) ;
(<%c%> ^ A) . a = A . b by A2, A6, ORDINAL4:def 1;
hence (<%c%> ^ A) . a is Cantor-component by A6, Def11; :: thesis: verum

end;

end;

end;

let a, b be Ordinal; :: thesis: ( a in b & b in dom (<%c%> ^ A) implies omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) )
assume A7: ( 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 A8: 1 c= a by ORDINAL1:16;
then A9: ( 1 in b & a in dom (<%c%> ^ A) & (1 +^ (dom A)) -^ 1 = dom A ) by A7, ORDINAL1:10, ORDINAL1:12, ORDINAL3:52;
then A10: ( b -^ 1 in dom A & a -^ 1 in dom A & a -^ 1 in b -^ 1 ) by A8, A3, A7, ORDINAL3:53;
( b = 1 +^ (b -^ 1) & a = 1 +^ (a -^ 1) ) by A8, A9, ORDINAL3:51, ORDINAL3:def 5;
then ( (<%c%> ^ A) . a = A . (a -^ 1) & (<%c%> ^ A) . b = A . (b -^ 1) ) by A2, A10, ORDINAL4:def 1;
hence omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by A10, Def11; :: thesis: verum

end;

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

then A11: ( (<%c%> ^ A) . a = <%c%> . a & a = 0 ) by A2, ORDINAL3:15, ORDINAL4:def 1, TARSKI:def 1;
then A12: succ 0 c= b by A7, ORDINAL1:21;
then b -^ 1 in (1 +^ (dom A)) -^ 1 by A3, A7, ORDINAL3:53;
then A13: ( b -^ 1 in dom A & b = 1 +^ (b -^ 1) ) by A12, ORDINAL3:52, ORDINAL3:def 5;
then A14: (<%c%> ^ A) . b = A . (b -^ 1) by A2, ORDINAL4:def 1;
( 0 in dom A & ( b -^ 1 = 0 or 0 in b -^ 1 ) ) by ORDINAL3:8;
then ( omega -exponent (A . 0) = omega -exponent (A . (b -^ 1)) or omega -exponent (A . (b -^ 1)) in omega -exponent (A . 0) ) by A13, Def11;
hence omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by A1, A11, A14, ORDINAL1:10; :: thesis: verum

end;

end;