let z1, z2 be quaternion number ; :: thesis: ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " implies z1 = z2 )
assume A1: ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " ) ; :: thesis: z1 = z2
A3: ( Rea (z1 " ) = (Rea z1) / (|.z1.| ^2 ) & Im1 (z1 " ) = - ((Im1 z1) / (|.z1.| ^2 )) & Im2 (z1 " ) = - ((Im2 z1) / (|.z1.| ^2 )) & Im3 (z1 " ) = - ((Im3 z1) / (|.z1.| ^2 )) ) by QUATERN2:29;
A4: ( (Rea z1) / (|.z1.| ^2 ) = (Rea z2) / (|.z2.| ^2 ) & - ((Im1 z1) / (|.z1.| ^2 )) = - ((Im1 z2) / (|.z2.| ^2 )) & - ((Im2 z1) / (|.z1.| ^2 )) = - ((Im2 z2) / (|.z2.| ^2 )) & - ((Im3 z1) / (|.z1.| ^2 )) = - ((Im3 z2) / (|.z2.| ^2 )) ) by A1, A3, QUATERN2:29;
|.z1.| ^2 <> 0 by A1, XCMPLX_1:6;
then ( Rea z1 = Rea z2 & Im1 z1 = Im1 z2 & Im2 z1 = Im2 z2 & Im3 z1 = Im3 z2 ) by A4, A1, XCMPLX_1:53;
hence z1 = z2 by QUATERNI:25; :: thesis: verum