let z1 be quaternion number ; :: thesis: (<i> * z1) + (z1 * <i> ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0 ,0 *]
set z = <i> ;
A2: <i> * z1 = [*(- (Im1 z1)),(Rea z1),(- (Im3 z1)),(Im2 z1)*] by QUATERN2:1, QUATERNI:30;
A3: z1 * <i> = [*(- (Im1 z1)),(Rea z1),(Im3 z1),(- (Im2 z1))*] by QUATERN2:1, QUATERNI:30;
A4: ( Rea (<i> * z1) = - (Im1 z1) & Im1 (<i> * z1) = Rea z1 & Im2 (<i> * z1) = - (Im3 z1) & Im3 (<i> * z1) = Im2 z1 ) by A2, QUATERNI:23;
A5: ( Rea (z1 * <i> ) = - (Im1 z1) & Im1 (z1 * <i> ) = Rea z1 & Im2 (z1 * <i> ) = Im3 z1 & Im3 (z1 * <i> ) = - (Im2 z1) ) by A3, QUATERNI:23;
(<i> * z1) + (z1 * <i> ) = ((((- (Im1 z1)) + (- (Im1 z1))) + (((Rea z1) + (Rea z1)) * <i> )) + (((- (Im3 z1)) + (Im3 z1)) * <j> )) + (((Im2 z1) + (- (Im2 z1))) * <k> ) by A4, A5, QUATERNI:def 22;
hence (<i> * z1) + (z1 * <i> ) = [*(- (2 * (Im1 z1))),(2 * (Rea z1)),0 ,0 *] by QUATERN2:1; :: thesis: verum