let z1, z2 be quaternion number ; :: thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) by Lm39, Th66; :: 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 Lm37
.= 0 by Lm7 ;
hence |.(z1 - z2).| = 0 by Th65; :: thesis: verum