theorem :: QUATERN3:23

for z1 being Quaternion holds (<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*]