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