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 Th114;
assume A is limit_ordinal ; :: thesis: A *^ (succ 1) = A
then A2: A +^ n is limit_ordinal by A1, ORDINAL3:48;

now

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 13;
n = succ k by A3, NAT_1:39;
then A +^ n = succ (A +^ k) by ORDINAL2:45;
hence contradiction by A2, ORDINAL1:42; :: thesis: verum

end;

hence A *^ (succ 1) = A by A1, ORDINAL2:44; :: thesis: verum