let z1, z2 be quaternion number ; :: thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) by Lm36, Th66; :: thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )
assume z1 = z2 ; :: thesis: |.(z1 - z2).| = 0
hence |.(z1 - z2).| = 0 by Lm5, Lm33, Th65; :: thesis: verum