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