let a be Ordinal; :: thesis: for n being non zero Nat holds CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>
let n be non zero Nat; :: thesis: CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>
Sum^ <%(n *^ (exp (omega,a)))%> = n *^ (exp (omega,a)) by ORDINAL5:53;
hence CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%> ; :: thesis: verum