A1: Rea (<j> " ) = 0 by QUATERNI:31, QUATERN2:27;
A2: Im1 (<j> " ) = 0 by QUATERNI:31, QUATERN2:27;
A3: Im2 (<j> " ) = - 1 by QUATERNI:31, QUATERN2:27, QUATERNI:70;
A4: Im3 (<j> " ) = 0 by QUATERNI:31, QUATERN2:27;
<j> " = [*(- 0 ),(- 0 ),(- 1),(- 0 )*] by A1, A2, A3, A4, QUATERNI:24
.= - <j> by QUATERN2:4 ;
hence <j> " = - <j> ; :: thesis: verum