theorem :: QUATERN3:49

for z1, z2 being Quaternion st |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " holds
z1 = z2