let a be non empty Ordinal; 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; 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%>
; verum