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