theorem :: QUATERN3:22

for z1 being Quaternion holds (<k> * z1) - (z1 * <k>) = [*0,(- (2 * (Im2 z1))),(2 * (Im1 z1)),0*]