theorem Th31: :: QUATERN2:31

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