theorem :: EC_PF_2:9

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