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;
{} +^ {} = {} by ORDINAL2:27;
then A1: S₁[ 0 ] by ORDINAL2:35;
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:36
.= succ ((A *^ (succ 1)) +^ 1) by ORDINAL2:28
.= succ (succ (A +^ n)) by A3, ORDINAL2:31
.= succ (A +^ (succ (Segm n))) by ORDINAL2:28
.= succ (A +^ (Segm (n + 1))) by NAT_1:38
.= A +^ (succ (n + 1)) by ORDINAL2:28 ;
hence (succ A) *^ 2 = (succ A) +^ (n + 1) by Th70; :: thesis: verum

end;

A4: for A being Ordinal st A <> 0 & 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 <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: 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
A8: dom phi = A and
A9: for B being Ordinal st B in A holds
phi . B = H₅(B) from ORDINAL2:sch 3();
A10: A *^ 2 = union (sup phi) by A5, A6, A8, A9, ORDINAL2:37
.= union (sup (rng phi)) by ORDINAL2:26 ;
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
A11: B in X and
A12: X in sup (rng phi) by A10, TARSKI:def 4;
reconsider X = X as Ordinal by A12;
consider C being Ordinal such that
A13: C in rng phi and
A14: X c= C by A12, ORDINAL2:21;
consider x being object such that
A15: x in dom phi and
A16: C = phi . x by A13, FUNCT_1:def 3;
reconsider x = x as Ordinal by A15;
A17: ex n being Nat st x *^ 2 = x +^ n by A7, A8, A15;
C = x *^ 2 by A8, A9, A15, A16;
then A18: C in A by A6, A8, A15, A17, Th69;
A +^ {} = A by ORDINAL2:27;
hence B in A +^ 0 by A11, A14, A18, ORDINAL1:10; :: thesis: verum

end;

A19: 1 in succ 1 by ORDINAL1:6;
A20: A +^ 0 = A by ORDINAL2:27;
A21: A = A *^ 1 by ORDINAL2:39;
1 c= 2 by A19, ORDINAL1:def 2;
hence A +^ 0 c= A *^ 2 by A20, A21, ORDINAL2:42; :: 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