theorem Th11: :: EC_PF_2:11

for K being Ring
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) )