theorem :: QUATERNI:32
for z1, z2, z3, z4 being Quaternion holds
( Rea (((z1 + z2) + z3) + z4) = (((Rea z1) + (Rea z2)) + (Rea z3)) + (Rea z4) & Im1 (((z1 + z2) + z3) + z4) = (((Im1 z1) + (Im1 z2)) + (Im1 z3)) + (Im1 z4) & Im2 (((z1 + z2) + z3) + z4) = (((Im2 z1) + (Im2 z2)) + (Im2 z3)) + (Im2 z4) & Im3 (((z1 + z2) + z3) + z4) = (((Im3 z1) + (Im3 z2)) + (Im3 z3)) + (Im3 z4) )