let z1, z2, z3, z4 be Quaternion; :: thesis: ((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; :: thesis: verum