A1: Im3 (<k> ") = - ((Im3 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= - 1 by QUATERNI:31 ;
A2: Im2 (<k> ") = - ((Im2 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
A3: Im1 (<k> ") = - ((Im1 <k>) / (|.<k>.| ^2)) by QUATERN2:29
.= 0 by QUATERNI:31 ;
Rea (<k> ") = (Rea <k>) / (|.<k>.| ^2) by QUATERN2:29
.= 0 by QUATERNI:31 ;
then <k> " = [*(- 0),(- 0),(- 0),(- jj)*] by A3, A2, A1, QUATERNI:24
.= - <k> by QUATERN2:4 ;
hence <k> " = - <k> ; :: thesis: verum