theorem Th10: :: EC_PF_2:10

for K being comRing
for a1, a2, a3, a4 being Element of K holds
( ((a1 * a2) * a3) * a4 = ((a4 * a2) * a3) * a1 & ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2 )