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