theorem :: QUATERN3:7

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