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_3:116
.=
exp (omega,((exp (e,omega)) *^ (exp (e,1))))
by ORDINAL4:30
.=
exp (omega,((exp (e,omega)) *^ e))
by ORDINAL2:63
.=
exp ((exp (omega,e)),(exp (e,omega)))
by ORDINAL4:31
.=
exp (e,(exp (e,omega)))
by EPSILON
; verum