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