1 *^ (exp (omega,a)) = exp (omega,a) by ORDINAL2:39;
hence <%(exp (omega,a)),m%> is Cantor-normal-form by Lm8; :: thesis: verum