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