theorem :: QUATERN2:50

for c being Quaternion holds
( Rea (c .|. c) = |.c.| ^2 & Im1 (c .|. c) = 0 & Im2 (c .|. c) = 0 & Im2 (c .|. c) = 0 )