let A be Cantor-normal-form Ordinal-Sequence; :: thesis: ( 0 in rng (omega -exponent A) iff ( A <> {} & omega -exponent (last A) = 0 ) )

hereby :: thesis: ( A <> {} & omega -exponent (last A) = 0 implies 0 in rng (omega -exponent A) )

assume 0 in rng (omega -exponent A) ; :: thesis: ( A <> {} & omega -exponent (last A) = 0 )
then consider x being object such that
A1: ( x in dom (omega -exponent A) & (omega -exponent A) . x = 0 ) by FUNCT_1:def 3;
thus A2: A <> {} by A1; :: thesis: omega -exponent (last A) = 0
A3: x in dom A by A1, Def1;
then omega -exponent (last A) c= omega -exponent (A . x) by A2, Th31;
then omega -exponent (last A) c= 0 by A1, A3, Def1;
hence omega -exponent (last A) = 0 ; :: thesis: verum

end;

assume A4: ( A <> {} & omega -exponent (last A) = 0 ) ; :: thesis: 0 in rng (omega -exponent A)
then consider A0 being Cantor-normal-form Ordinal-Sequence, a0 being Cantor-component Ordinal such that
A5: A = A0 ^ <%a0%> by Th29;
0 in 1 by CARD_1:49, TARSKI:def 1;
then 0 in dom <%a0%> by AFINSQ_1:33;
then A6: (len A0) + 0 in dom A by A5, AFINSQ_1:23;
then A7: len A0 in dom (omega -exponent A) by Def1;
0 = omega -exponent a0 by A4, A5, AFINSQ_1:92
.= omega -exponent (A . (len A0)) by A5, AFINSQ_1:36
.= (omega -exponent A) . (len A0) by A6, Def1 ;
hence 0 in rng (omega -exponent A) by A7, FUNCT_1:3; :: thesis: verum