let A be Ordinal; :: thesis: ex n being Nat st A *^ (succ 1) = A +^ n
defpred S₂[ Ordinal] means ex n being Nat st $1 *^ 2 = $1 +^ n;
( {} +^ {} = {} & {} *^ 2 = {} ) by ORDINAL2:44, ORDINAL2:52;
then A1: S₂[ 0 ] ;
A2: for A being Ordinal st S₂[A] holds
S₂[ succ A]

proof

let A be Ordinal; :: thesis: ( S₂[A] implies S₂[ succ A] )
given n being Nat such that A3: A *^ 2 = A +^ n ; :: thesis: S₂[ succ A]
take n + 1 ; :: thesis: (succ A) *^ 2 = (succ A) +^ (n + 1)
(succ A) *^ 2 = (A *^ 2) +^ 2 by ORDINAL2:53
.= succ ((A *^ (succ 1)) +^ 1) by ORDINAL2:45
.= succ (succ (A +^ n)) by A3, ORDINAL2:48
.= succ (A +^ (succ n)) by ORDINAL2:45
.= succ (A +^ (n + 1)) by NAT_1:39
.= A +^ (succ (n + 1)) by ORDINAL2:45 ;
hence (succ A) *^ 2 = (succ A) +^ (n + 1) by Th28; :: thesis: verum

end;

A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₂[B] ) holds
S₂[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₂[B] ) implies S₂[A] )
assume that
A5: ( A <> {} & A is limit_ordinal ) and
A6: for B being Ordinal st B in A holds
S₂[B] ; :: thesis: S₂[A]
take 0 ; :: thesis: A *^ 2 = A +^ 0
deffunc H₁( Ordinal) -> set = $1 *^ 2;
consider phi being Ordinal-Sequence such that
A7: dom phi = A and
A8: for B being Ordinal st B in A holds
phi . B = H₁(B) from ORDINAL2:sch 3();
A9: A *^ 2 = union (sup phi) by A5, A7, A8, ORDINAL2:54
.= union (sup (rng phi)) by ORDINAL2:35 ;
thus A *^ 2 c= A +^ 0 :: according to XBOOLE_0:def 10 :: thesis: A +^ 0 c= A *^ 2

proof

let B be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not B in A *^ 2 or B in A +^ 0 )
assume B in A *^ 2 ; :: thesis: B in A +^ 0
then consider X being set such that
A10: ( B in X & X in sup (rng phi) ) by A9, TARSKI:def 4;
reconsider X = X as Ordinal by A10;
consider C being Ordinal such that
A11: ( C in rng phi & X c= C ) by A10, ORDINAL2:29;
consider x being set such that
A12: ( x in dom phi & C = phi . x ) by A11, FUNCT_1:def 5;
reconsider x = x as Ordinal by A12;
A13: ex n being Nat st x *^ 2 = x +^ n by A6, A7, A12;
C = x *^ 2 by A7, A8, A12;
then C in A by A5, A7, A12, A13, Th27;
then ( X in A & A +^ {} = A ) by A11, ORDINAL1:22, ORDINAL2:44;
hence B in A +^ 0 by A10, ORDINAL1:19; :: thesis: verum

end;

1 in succ 1 by ORDINAL1:10;
then ( A +^ 0 = A & A = A *^ 1 & 1 c= 2 ) by ORDINAL1:def 2, ORDINAL2:44, ORDINAL2:56;
hence A +^ 0 c= A *^ 2 by ORDINAL2:59; :: thesis: verum

end;

for A being Ordinal holds S₂[A] from ORDINAL2:sch 1(A1, A2, A4);
hence ex n being Nat st A *^ (succ 1) = A +^ n ; :: thesis: verum