theorem Th5: :: EUCLID:8

for n being Nat
for x being Element of REAL n st |.x.| = 0 holds
x = 0* n