theorem Th5: :: EC_PF_2:5

for n being Nat
for K being Field
for a1 being Element of K st a1 = 0. K & n > 1 holds
a1 |^ n = 0. K