let z be quaternion number ; :: thesis: |.z.| ^2 = Rea (z * (z *' ))
A1: |.z.| ^2 = ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) by Th1;
z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
then ( Rea (z *' ) = Rea z & Im1 (z *' ) = - (Im1 z) & Im2 (z *' ) = - (Im2 z) & Im3 (z *' ) = - (Im3 z) ) by QUATERNI:23;
then z * (z *' ) = [*(((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )),0 ,0 ,0 *] by QUATERN2:1;
hence |.z.| ^2 = Rea (z * (z *' )) by QUATERNI:23, A1; :: thesis: verum