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 Th11;
A2: z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by QUATERNI:43;
A3: ( Im2 (z *' ) = - (Im2 z) & Im3 (z *' ) = - (Im3 z) ) by A2, QUATERNI:23;
A4: ( Rea (z *' ) = Rea z & Im1 (z *' ) = - (Im1 z) ) by A2, QUATERNI:23;
A5: z * (z *' ) = [*(((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 )),0 ,0 ,0 *] by A4, A3, QUATERN2:1;
thus |.z.| ^2 = Rea (z * (z *' )) by A1, A5, QUATERNI:23; :: thesis: verum