let n, k be Nat; :: thesis: ( n |^|^ k = 0 implies n = 0 )
assume A1: n |^|^ k = 0 ; :: thesis: n = 0
then k <> 0 by ORDINAL5:13;
then consider j being Nat such that
A2: k = j + 1 by NAT_1:6;
n |^|^ (j + 1) = n |^|^ (Segm (j + 1))
.= n |^|^ (succ (Segm j)) by NAT_1:38
.= exp (n,(n |^|^ j)) by ORDINAL5:14
.= n |^ (n |^|^ j) ;
hence n = 0 by A1, A2; :: thesis: verum