theorem :: QUATERN3:5

for z being Quaternion st z is Real holds
z * <i> = [*0,(Rea z),0,0*]