theorem :: QUATERNI:40

for z being Quaternion holds
( Rea (z * z) = ((((Rea z) ^2) - ((Im1 z) ^2)) - ((Im2 z) ^2)) - ((Im3 z) ^2) & Im1 (z * z) = 2 * ((Rea z) * (Im1 z)) & Im2 (z * z) = 2 * ((Rea z) * (Im2 z)) & Im3 (z * z) = 2 * ((Rea z) * (Im3 z)) )