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