theorem :: QUATERN3:20

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