let a, n be Nat; :: thesis: ( a <> 0 implies n divides n |^ a )
assume a <> 0 ; :: thesis: n divides n |^ a
then consider b being Nat such that
A1: a = b + 1 by NAT_1:6;
reconsider b = b as Element of NAT by ORDINAL1:def 12;
n |^ 1 divides n |^ (b + 1) by NAT_1:12, NEWTON:89;
hence n divides n |^ a by A1; :: thesis: verum