let n be Nat; :: thesis: ( n > 0 implies 0 |^ n = 0 )
assume n > 0 ; :: thesis: 0 |^ n = 0
then n >= 0 + 1 by NAT_1:13;
hence 0 |^ n = 0 by NEWTON:11; :: thesis: verum