let n be Nat; :: thesis: ( not n is zero implies n is Cantor-component )
assume A1: not n is zero ; :: thesis: n is Cantor-component
n = n *^ 1 by ORDINAL2:39
.= n *^ (exp (omega,0)) by ORDINAL2:43 ;
hence n is Cantor-component by A1; :: thesis: verum