let A be Ordinal; :: thesis: ( A is limit_ordinal implies A *^ (succ 1) = A )
consider n being Nat such that
A1: A *^ 2 = A +^ n by Th71;
assume A is limit_ordinal ; :: thesis: A *^ (succ 1) = A
then A2: A +^ n is limit_ordinal by A1, ORDINAL3:40;
now :: thesis: not n <> 0
assume n <> 0 ; :: thesis: contradiction
then consider k being Nat such that
A3: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
Segm n = succ (Segm k) by A3, NAT_1:38;
then A +^ n = succ (A +^ k) by ORDINAL2:28;
hence contradiction by A2, ORDINAL1:29; :: thesis: verum
end;
hence A *^ (succ 1) = A by A1, ORDINAL2:27; :: thesis: verum