theorem :: QUATERN2:12

for r being Quaternion holds 0q * r = 0