let z1, z2, z3, z4 be quaternion number ; ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
A1:
Im1 (((z1 - z2) - z3) + z4) = (Im1 ((z1 - z2) - z3)) + (Im1 z4)
by QUATERNI:36;
A2:
Im1 (((z1 - z2) - z3) + z4) = ((Im1 (z1 - z2)) - (Im1 z3)) + (Im1 z4)
by A1, QUATERNI:42;
A3:
Im1 (((z1 - z2) - z3) + z4) = (((Im1 z1) - (Im1 z2)) - (Im1 z3)) + (Im1 z4)
by A2, QUATERNI:42;
A4:
Im2 (((z1 - z2) - z3) + z4) = (Im2 ((z1 - z2) - z3)) + (Im2 z4)
by QUATERNI:36;
A5:
Im2 (((z1 - z2) - z3) + z4) = ((Im2 (z1 - z2)) - (Im2 z3)) + (Im2 z4)
by A4, QUATERNI:42;
A6:
Im2 (((z1 - z2) - z3) + z4) = (((Im2 z1) - (Im2 z2)) - (Im2 z3)) + (Im2 z4)
by A5, QUATERNI:42;
A7:
Im2 (((z4 - z3) - z2) + z1) = (Im2 ((z4 - z3) - z2)) + (Im2 z1)
by QUATERNI:36;
A8:
Im2 (((z4 - z3) - z2) + z1) = ((Im2 (z4 - z3)) - (Im2 z2)) + (Im2 z1)
by A7, QUATERNI:42;
A9:
Im2 (((z4 - z3) - z2) + z1) = (((Im2 z4) - (Im2 z3)) - (Im2 z2)) + (Im2 z1)
by A8, QUATERNI:42;
A10:
Im1 (((z4 - z3) - z2) + z1) = (Im1 ((z4 - z3) - z2)) + (Im1 z1)
by QUATERNI:36;
A11:
Im1 (((z4 - z3) - z2) + z1) = ((Im1 (z4 - z3)) - (Im1 z2)) + (Im1 z1)
by A10, QUATERNI:42;
A12:
Im1 (((z4 - z3) - z2) + z1) = (((Im1 z4) - (Im1 z3)) - (Im1 z2)) + (Im1 z1)
by A11, QUATERNI:42;
A13:
Im3 (((z4 - z3) - z2) + z1) = (Im3 ((z4 - z3) - z2)) + (Im3 z1)
by QUATERNI:36;
A14:
Im3 (((z4 - z3) - z2) + z1) = ((Im3 (z4 - z3)) - (Im3 z2)) + (Im3 z1)
by A13, QUATERNI:42;
A15:
Im3 (((z4 - z3) - z2) + z1) = (((Im3 z4) - (Im3 z3)) - (Im3 z2)) + (Im3 z1)
by A14, QUATERNI:42;
A16:
Rea (((z4 - z3) - z2) + z1) = (Rea ((z4 - z3) - z2)) + (Rea z1)
by QUATERNI:36;
A17:
Rea (((z4 - z3) - z2) + z1) = ((Rea (z4 - z3)) - (Rea z2)) + (Rea z1)
by A16, QUATERNI:42;
A18:
Rea (((z4 - z3) - z2) + z1) = (((Rea z4) - (Rea z3)) - (Rea z2)) + (Rea z1)
by A17, QUATERNI:42;
A19:
Im3 (((z1 - z2) - z3) + z4) = (Im3 ((z1 - z2) - z3)) + (Im3 z4)
by QUATERNI:36;
A20:
Im3 (((z1 - z2) - z3) + z4) = ((Im3 (z1 - z2)) - (Im3 z3)) + (Im3 z4)
by A19, QUATERNI:42;
A21:
Im3 (((z1 - z2) - z3) + z4) = (((Im3 z1) - (Im3 z2)) - (Im3 z3)) + (Im3 z4)
by A20, QUATERNI:42;
A22:
Rea (((z1 - z2) - z3) + z4) = (Rea ((z1 - z2) - z3)) + (Rea z4)
by QUATERNI:36;
A23:
Rea (((z1 - z2) - z3) + z4) = ((Rea (z1 - z2)) - (Rea z3)) + (Rea z4)
by A22, QUATERNI:42;
A24:
Rea (((z1 - z2) - z3) + z4) = (((Rea z1) - (Rea z2)) - (Rea z3)) + (Rea z4)
by A23, QUATERNI:42;
thus
((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
by A24, A3, A6, A21, A18, A12, A9, A15, QUATERNI:25; verum