theorem :: QUATERN3:19

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