theorem :: QUATERN3:18

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