theorem :: QUATERN2:32

for r being Quaternion st r <> 0 holds
(r ") * r = 1