for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))