let m be Power of n; :: thesis: not m is zero
consider l being non zero Nat such that
A: m = n |^ l by defpower;
0 + 1 < l + 1 by XREAL_1:6;
then 1 <= l by NAT_1:13;
then n |^ 1 <= n |^ l by NAT_6:1;
hence not m is zero by A; :: thesis: verum