theorem :: QUATERNI:28

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