let z be quaternion number ; :: thesis: ( z ~ = 0 implies z = 0 )
assume z ~ = 0 ; :: thesis: z = 0
then |.z.| = 0 by SQUARE_1:82;
hence z = 0 by QUATERNI:66; :: thesis: verum