for z3, z being Quaternion st z is Real holds
z * z3 = [*((Rea z) * (Rea z3)),((Rea z) * (Im1 z3)),((Rea z) * (Im2 z3)),((Rea z) * (Im3 z3))*]