theorem :: QUATERNI:38
for z1, z2 being Quaternion st Im1 z1 = 0 & Im1 z2 = 0 & Im2 z1 = 0 & Im2 z2 = 0 & Im3 z1 = 0 & Im3 z2 = 0 holds
( Rea (z1 * z2) = (Rea z1) * (Rea z2) & Im1 (z1 * z2) = ((Im2 z1) * (Im3 z2)) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((Im3 z1) * (Im1 z2)) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((Im1 z1) * (Im2 z2)) - ((Im2 z1) * (Im1 z2)) )