theorem :: QUATERN2:42

for z being Element of R_Quaternion st z *' = 0. R_Quaternion holds
z = 0. R_Quaternion