let z1, z2, z3, z4 be Quaternion; ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
Im1 (((z1 - z2) - z3) + z4) = (Im1 ((z1 - z2) - z3)) + (Im1 z4)
by QUATERNI:36;
then
Im1 (((z1 - z2) - z3) + z4) = ((Im1 (z1 - z2)) - (Im1 z3)) + (Im1 z4)
by QUATERNI:42;
then A1:
Im1 (((z1 - z2) - z3) + z4) = (((Im1 z1) - (Im1 z2)) - (Im1 z3)) + (Im1 z4)
by QUATERNI:42;
Im2 (((z1 - z2) - z3) + z4) = (Im2 ((z1 - z2) - z3)) + (Im2 z4)
by QUATERNI:36;
then
Im2 (((z1 - z2) - z3) + z4) = ((Im2 (z1 - z2)) - (Im2 z3)) + (Im2 z4)
by QUATERNI:42;
then A2:
Im2 (((z1 - z2) - z3) + z4) = (((Im2 z1) - (Im2 z2)) - (Im2 z3)) + (Im2 z4)
by QUATERNI:42;
Im2 (((z4 - z3) - z2) + z1) = (Im2 ((z4 - z3) - z2)) + (Im2 z1)
by QUATERNI:36;
then
Im2 (((z4 - z3) - z2) + z1) = ((Im2 (z4 - z3)) - (Im2 z2)) + (Im2 z1)
by QUATERNI:42;
then A3:
Im2 (((z4 - z3) - z2) + z1) = (((Im2 z4) - (Im2 z3)) - (Im2 z2)) + (Im2 z1)
by QUATERNI:42;
Im1 (((z4 - z3) - z2) + z1) = (Im1 ((z4 - z3) - z2)) + (Im1 z1)
by QUATERNI:36;
then
Im1 (((z4 - z3) - z2) + z1) = ((Im1 (z4 - z3)) - (Im1 z2)) + (Im1 z1)
by QUATERNI:42;
then A4:
Im1 (((z4 - z3) - z2) + z1) = (((Im1 z4) - (Im1 z3)) - (Im1 z2)) + (Im1 z1)
by QUATERNI:42;
Im3 (((z4 - z3) - z2) + z1) = (Im3 ((z4 - z3) - z2)) + (Im3 z1)
by QUATERNI:36;
then
Im3 (((z4 - z3) - z2) + z1) = ((Im3 (z4 - z3)) - (Im3 z2)) + (Im3 z1)
by QUATERNI:42;
then A5:
Im3 (((z4 - z3) - z2) + z1) = (((Im3 z4) - (Im3 z3)) - (Im3 z2)) + (Im3 z1)
by QUATERNI:42;
Rea (((z4 - z3) - z2) + z1) = (Rea ((z4 - z3) - z2)) + (Rea z1)
by QUATERNI:36;
then
Rea (((z4 - z3) - z2) + z1) = ((Rea (z4 - z3)) - (Rea z2)) + (Rea z1)
by QUATERNI:42;
then A6:
Rea (((z4 - z3) - z2) + z1) = (((Rea z4) - (Rea z3)) - (Rea z2)) + (Rea z1)
by QUATERNI:42;
Im3 (((z1 - z2) - z3) + z4) = (Im3 ((z1 - z2) - z3)) + (Im3 z4)
by QUATERNI:36;
then
Im3 (((z1 - z2) - z3) + z4) = ((Im3 (z1 - z2)) - (Im3 z3)) + (Im3 z4)
by QUATERNI:42;
then A7:
Im3 (((z1 - z2) - z3) + z4) = (((Im3 z1) - (Im3 z2)) - (Im3 z3)) + (Im3 z4)
by QUATERNI:42;
Rea (((z1 - z2) - z3) + z4) = (Rea ((z1 - z2) - z3)) + (Rea z4)
by QUATERNI:36;
then
Rea (((z1 - z2) - z3) + z4) = ((Rea (z1 - z2)) - (Rea z3)) + (Rea z4)
by QUATERNI:42;
then
Rea (((z1 - z2) - z3) + z4) = (((Rea z1) - (Rea z2)) - (Rea z3)) + (Rea z4)
by QUATERNI:42;
hence
((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1
by A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; verum