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