theorem :: QUATERN3:6

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