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