theorem :: QUATERNI:33

for z1 being Quaternion
for x being Real st z1 = x holds
( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 )