let a be Ordinal; :: thesis: ( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) )

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: ( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) )

hence ( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) ) by ORDINAL2:4; :: thesis: verum

end;

suppose a <> 0 ; :: thesis: ( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) )

then consider A0 being Cantor-normal-form Ordinal-Sequence, a0 being Cantor-component Ordinal such that
A2: CantorNF a = A0 ^ <%a0%> by Th29;

hereby :: thesis: ( not 0 in rng (omega -exponent (CantorNF a)) implies a is limit_ordinal )

assume A3: a is limit_ordinal ; :: thesis: not 0 in rng (omega -exponent (CantorNF a))
omega -exponent (last (CantorNF a)) <> 0

proof

assume omega -exponent (last (CantorNF a)) = 0 ; :: thesis: contradiction
then omega -exponent a0 = 0 by A2, AFINSQ_1:92;
then a0 = (omega -leading_coeff a0) *^ (exp (omega,0)) by Th59
.= (omega -leading_coeff a0) *^ 1 by ORDINAL2:43
.= omega -leading_coeff a0 by ORDINAL2:39 ;
then A6: Sum^ (CantorNF a) = (Sum^ A0) +^ (omega -leading_coeff a0) by A2, ORDINAL5:54;
then A7: Sum^ A0 c= a by ORDINAL3:24;
Sum^ A0 <> a

proof

assume Sum^ A0 = a ; :: thesis: contradiction
then (Sum^ A0) +^ 0 = (Sum^ A0) +^ (omega -leading_coeff a0) by A6, ORDINAL2:27;
hence contradiction by ORDINAL3:21; :: thesis: verum

end;

then Sum^ A0 in a by A7, XBOOLE_0:def 8, ORDINAL1:11;
then (Sum^ A0) +^ (omega -leading_coeff a0) in a by A3, CARD_2:70;
hence contradiction by A6; :: thesis: verum

end;

hence not 0 in rng (omega -exponent (CantorNF a)) by Th51; :: thesis: verum

end;

assume A8: not 0 in rng (omega -exponent (CantorNF a)) ; :: thesis: a is limit_ordinal

now :: thesis: for b being Ordinal st b in a holds
succ b in a

let b be Ordinal; :: thesis: ( b in a implies succ b in a )
assume b in a ; :: thesis: succ b in a
then A9: succ b in succ a by ORDINAL3:3;
not succ b = a

proof

assume succ b = a ; :: thesis: contradiction
then A10: a = b (+) 1 by Th90;
set E1 = omega -exponent (CantorNF b);
set E2 = omega -exponent (CantorNF 1);
set L1 = omega -leading_coeff (CantorNF b);
set L2 = omega -leading_coeff (CantorNF 1);
consider C being Cantor-normal-form Ordinal-Sequence such that
A11: ( b (+) 1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF 1))) ) and
for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF 1))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF 1))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF 1)) . (((omega -exponent (CantorNF 1)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF 1))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF 1)) . (((omega -exponent (CantorNF 1)) ") . (omega -exponent (C . d)))) ) ) by Def5;
omega -exponent (CantorNF 1) = omega -exponent <%1%> by Th71
.= <%(omega -exponent 1)%> by Th46
.= <%0%> by Th21 ;
then rng (omega -exponent (CantorNF 1)) = {0} by AFINSQ_1:33;
then 0 in rng (omega -exponent (CantorNF 1)) by TARSKI:def 1;
hence contradiction by A8, A10, A11, XBOOLE_1:7, TARSKI:def 3; :: thesis: verum

end;

hence succ b in a by A9, ORDINAL1:8; :: thesis: verum

end;

hence a is limit_ordinal by ORDINAL1:28; :: thesis: verum

end;

end;