let n be Nat; for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
let e be epsilon Ordinal; ( 0 in n implies e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1))) )
assume A1:
0 in n
; e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
0 in e
by ORDINAL3:8;
then
( omega in e & e c= e |^|^ n )
by A1, Th23, Th37;
then A2:
omega c= e |^|^ n
by ORDINAL1:def 2;
thus e |^|^ (n + 2) =
e |^|^ (Segm ((n + 1) + 1))
.=
e |^|^ (succ (Segm (n + 1)))
by NAT_1:38
.=
exp (e,(e |^|^ (n + 1)))
by Th14
.=
exp ((exp (omega,e)),(e |^|^ (n + 1)))
by Def5
.=
exp (omega,((e |^|^ (Segm (n + 1))) *^ e))
by ORDINAL4:31
.=
exp (omega,((e |^|^ (succ (Segm n))) *^ e))
by NAT_1:38
.=
exp (omega,((exp (e,(e |^|^ n))) *^ e))
by Th14
.=
exp (omega,((exp (e,(e |^|^ n))) *^ (exp (e,1))))
by ORDINAL2:46
.=
exp (omega,(exp (e,(1 +^ (e |^|^ n)))))
by ORDINAL4:30
.=
exp (omega,(exp (e,(e |^|^ n))))
by A2, CARD_2:74
.=
exp (omega,(e |^|^ (succ (Segm n))))
by Th14
.=
exp (omega,(e |^|^ (Segm (n + 1))))
by NAT_1:38
.=
exp (omega,(e |^|^ (n + 1)))
; verum