let n be non zero Nat; :: thesis: CantorNF n = <%n%>
Sum^ <%n%> = n by ORDINAL5:53;
hence CantorNF n = <%n%> ; :: thesis: verum