let A be Ordinal; ex n being Nat st A *^ (succ 1) = A +^ n
defpred S1[ Ordinal] means ex n being Nat st $1 *^ 2 = $1 +^ n;
{} +^ {} = {}
by ORDINAL2:27;
then A1:
S1[ 0 ]
by ORDINAL2:35;
A2:
for A being Ordinal st S1[A] holds
S1[ succ A]
A4:
for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be
Ordinal;
( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that A5:
A <> 0
and A6:
A is
limit_ordinal
and A7:
for
B being
Ordinal st
B in A holds
S1[
B]
;
S1[A]
take
0
;
A *^ 2 = A +^ 0
deffunc H5(
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 = H5(
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
XBOOLE_0:def 10 A +^ 0 c= A *^ 2proof
let B be
Ordinal;
ORDINAL1:def 5 ( not B in A *^ 2 or B in A +^ 0 )
assume
B in A *^ 2
;
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;
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;
verum
end;
for A being Ordinal holds S1[A]
from ORDINAL2:sch 1(A1, A2, A4);
hence
ex n being Nat st A *^ (succ 1) = A +^ n
; verum