let z1, z2 be Quaternion; :: thesis: ( z1 - z2 = 0 implies z1 = z2 )
assume A1: z1 - z2 = 0 ; :: thesis: z1 = z2
A2: Rea (z1 - z2) = (Rea z1) - (Rea z2) by Th35;
A3: Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) by Th35;
A4: Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) by Th35;
A5: Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) by Th35;
A6: Rea (z1 - z2) = 0 by A1, Lm6, Th16;
A7: Im1 (z1 - z2) = 0 by A1, Lm6, Th16;
A8: Im2 (z1 - z2) = 0 by A1, Lm6, Th16;
Im3 (z1 - z2) = 0 by A1, Lm6, Th16;
hence z1 = z2 by A2, A3, A4, A5, A6, A7, A8, Th18; :: thesis: verum