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