let e be epsilon Ordinal; :: thesis: 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 ; :: thesis: verum