theorem Th5: :: EC_PF_2:5

for n being Nat
for K being Ring st n >= 1 holds
(0. K) |^ n = 0. K