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

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 A3: a in dom A0 ; :: thesis: omega -exponent (last A) c= omega -exponent (A . a)

0 in 1 by CARD_1:49, TARSKI:def 1;
then 0 in dom <%a0%> by AFINSQ_1:33;
then (len A0) + 0 in dom A by A2, AFINSQ_1:23;
then omega -exponent (A . (len A0)) in omega -exponent (A . a) by A3, ORDINAL5:def 11;
then omega -exponent a0 in omega -exponent (A . a) by A2, AFINSQ_1:36;
then omega -exponent (last A) in omega -exponent (A . a) by A2, AFINSQ_1:92;
hence omega -exponent (last A) c= omega -exponent (A . a) by ORDINAL1:def 2; :: thesis: verum

end;

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

then consider n being Nat such that
A4: ( n in dom <%a0%> & a = (len A0) + n ) ;
n in Segm 1 by A4, AFINSQ_1:33;
then n = 0 by CARD_1:49, TARSKI:def 1;
then A . a = a0 by A2, A4, AFINSQ_1:36
.= last A by A2, AFINSQ_1:92 ;
hence omega -exponent (last A) c= omega -exponent (A . a) ; :: thesis: verum

end;

end;