let A be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: for a being object st a in dom A holds
omega -exponent (A . a) c= omega -exponent (A . 0)
let a be object ; :: thesis: ( a in dom A implies omega -exponent (A . a) c= omega -exponent (A . 0) )
assume A1: a in dom A ; :: thesis: omega -exponent (A . a) c= omega -exponent (A . 0)
consider a0 being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A2: A = <%a0%> ^ A0 by ORDINAL5:67;

per cases ( a in dom <%a0%> or ex n being Nat st
( n in dom A0 & a = (len <%a0%>) + n ) ) by A1, A2, AFINSQ_1:20;

suppose a in dom <%a0%> ; :: thesis: omega -exponent (A . a) c= omega -exponent (A . 0)

then a in Segm 1 by AFINSQ_1:33;
hence omega -exponent (A . a) c= omega -exponent (A . 0) by CARD_1:49, TARSKI:def 1; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom A0 & a = (len <%a0%>) + n ) ; :: thesis: omega -exponent (A . a) c= omega -exponent (A . 0)

then consider n being Nat such that
A3: ( n in dom A0 & a = (len <%a0%>) + n ) ;
reconsider n1 = a as Nat by A3;
n1 = n + 1 by A3, AFINSQ_1:34;
then 0 in Segm n1 by NAT_1:44;
then A4: 0 in n1 ;
n1 in dom A by A2, A3, AFINSQ_1:23;
hence omega -exponent (A . a) c= omega -exponent (A . 0) by A4, ORDINAL5:def 11, ORDINAL1:def 2; :: thesis: verum

end;

end;