let z1, z2 be Quaternion; ( |.z1.| = |.z2.| & |.z1.| <> 0 & z1 " = z2 " implies z1 = z2 )
assume that
A1:
|.z1.| = |.z2.|
and
A2:
|.z1.| <> 0
and
A3:
z1 " = z2 "
; 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; verum