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