let e be epsilon Ordinal; exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))
thus exp (omega,(exp (e,omega))) =
exp (omega,(exp (e,(1 +^ omega))))
by CARD_2:74
.=
exp (omega,((exp (e,omega)) *^ (exp (e,1))))
by ORDINAL4:30
.=
exp (omega,((exp (e,omega)) *^ e))
by ORDINAL2:46
.=
exp ((exp (omega,e)),(exp (e,omega)))
by ORDINAL4:31
.=
exp (e,(exp (e,omega)))
by Def5
; verum