let z1, z, z2 be quaternion number ; :: thesis: ( z1 - z = z2 - z implies z1 = z2 )
assume A1: z1 - z = z2 - z ; :: thesis: z1 = z2
A2: ( Rea (z1 - z) = (Rea z1) - (Rea z) & Im1 (z1 - z) = (Im1 z1) - (Im1 z) & Im2 (z1 - z) = (Im2 z1) - (Im2 z) & Im3 (z1 - z) = (Im3 z1) - (Im3 z) ) by QUATERNI:42;
( Rea (z2 - z) = (Rea z2) - (Rea z) & Im1 (z2 - z) = (Im1 z2) - (Im1 z) & Im2 (z2 - z) = (Im2 z2) - (Im2 z) & Im3 (z2 - z) = (Im3 z2) - (Im3 z) ) by QUATERNI:42;
hence z1 = z2 by QUATERNI:25, A1, A2; :: thesis: verum