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