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