theorem Th8: :: EC_PF_2:8

for K being Abelian AddGroup
for a1, a2, a3, a4, a5 being Element of K holds
( ((a1 + a2) + a3) + a4 = a1 + ((a2 + a3) + a4) & (((a1 + a2) + a3) + a4) + a5 = a1 + (((a2 + a3) + a4) + a5) )