for z3, z being Quaternion st z is Real holds
z + z3 = ((((Rea z) + (Rea z3)) + ((Im1 z3) * <i>)) + ((Im2 z3) * <j>)) + ((Im3 z3) * <k>)