let z1, z2 be Quaternion; :: thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) by Lm38, Th59; :: thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )
assume z1 = z2 ; :: thesis: |.(z1 - z2).| = 0
then z1 - z2 = [*((Rea z1) - (Rea z1)),((Im1 z1) - (Im1 z1)),((Im2 z1) - (Im2 z1)),((Im3 z1) - (Im3 z1))*] by Lm36
.= 0 by Lm6 ;
hence |.(z1 - z2).| = 0 by Th58; :: thesis: verum