for z being Element of R_Quaternion st |.z.| = 0 holds
z = 0. R_Quaternion by Th39, QUATERNI:66;