let z1 be Quaternion; :: thesis: (<j> * z1) - (z1 * <j>) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*]
set z = <j> ;
A1: <j> * z1 = (((((((Rea <j>) * (Rea z1)) - ((Im1 <j>) * (Im1 z1))) - ((Im2 <j>) * (Im2 z1))) - ((Im3 <j>) * (Im3 z1))) + ((((((Rea <j>) * (Im1 z1)) + ((Im1 <j>) * (Rea z1))) + ((Im2 <j>) * (Im3 z1))) - ((Im3 <j>) * (Im2 z1))) * <i>)) + ((((((Rea <j>) * (Im2 z1)) + ((Im2 <j>) * (Rea z1))) + ((Im3 <j>) * (Im1 z1))) - ((Im1 <j>) * (Im3 z1))) * <j>)) + ((((((Rea <j>) * (Im3 z1)) + ((Im3 <j>) * (Rea z1))) + ((Im1 <j>) * (Im2 z1))) - ((Im2 <j>) * (Im1 z1))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(Im3 z1),(Rea z1),(- (Im1 z1))*] by QUATERN2:1, QUATERNI:31 ;
z1 * <j> = (((((((Rea z1) * (Rea <j>)) - ((Im1 z1) * (Im1 <j>))) - ((Im2 z1) * (Im2 <j>))) - ((Im3 z1) * (Im3 <j>))) + ((((((Rea z1) * (Im1 <j>)) + ((Im1 z1) * (Rea <j>))) + ((Im2 z1) * (Im3 <j>))) - ((Im3 z1) * (Im2 <j>))) * <i>)) + ((((((Rea z1) * (Im2 <j>)) + ((Im2 z1) * (Rea <j>))) + ((Im3 z1) * (Im1 <j>))) - ((Im1 z1) * (Im3 <j>))) * <j>)) + ((((((Rea z1) * (Im3 <j>)) + ((Im3 z1) * (Rea <j>))) + ((Im1 z1) * (Im2 <j>))) - ((Im2 z1) * (Im1 <j>))) * <k>) by QUATERNI:93
.= [*(- (Im2 z1)),(- (Im3 z1)),(Rea z1),(Im1 z1)*] by QUATERN2:1, QUATERNI:31 ;
then (<j> * z1) - (z1 * <j>) = [*((- (Im2 z1)) - (- (Im2 z1))),((Im3 z1) - (- (Im3 z1))),((Rea z1) - (Rea z1)),((- (Im1 z1)) - (Im1 z1))*] by A1, QUATERN2:5
.= [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ;
hence (<j> * z1) - (z1 * <j>) = [*0,(2 * (Im3 z1)),0,(- (2 * (Im1 z1)))*] ; :: thesis: verum