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