theorem :: QUATERNI:27

for z being Quaternion st z = 0 holds
((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0