theorem :: QUATERN3:21

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