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