let n be natural number ; :: thesis: for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp omega ,(e |^|^ (n + 1))
let e be epsilon Ordinal; :: thesis: ( 0 in n implies e |^|^ (n + 2) = exp omega ,(e |^|^ (n + 1)) )
assume A0: 0 in n ; :: thesis: e |^|^ (n + 2) = exp omega ,(e |^|^ (n + 1))
0 in e by ORDINAL3:10;
then ( omega in e & e c= e |^|^ n ) by A0, Th6, Th21;
then A1: omega c= e |^|^ n by ORDINAL1:def 2;
thus e |^|^ (n + 2) = e |^|^ ((n + 1) + 1)
.= e |^|^ (succ (n + 1)) by NAT_1:39
.= exp e,(e |^|^ (n + 1)) by Th1
.= exp (exp omega ,e),(e |^|^ (n + 1)) by EPSILON
.= exp omega ,((e |^|^ (n + 1)) *^ e) by ORDINAL4:31
.= exp omega ,((e |^|^ (succ n)) *^ e) by NAT_1:39
.= exp omega ,((exp e,(e |^|^ n)) *^ e) by Th1
.= exp omega ,((exp e,(e |^|^ n)) *^ (exp e,1)) by ORDINAL2:63
.= exp omega ,(exp e,(1 +^ (e |^|^ n))) by ORDINAL4:30
.= exp omega ,(exp e,(e |^|^ n)) by A1, CARD_3:116
.= exp omega ,(e |^|^ (succ n)) by Th1
.= exp omega ,(e |^|^ (n + 1)) by NAT_1:39 ; :: thesis: verum