theorem Th11: :: POLYRED:11

for X being set
for L being non empty associative multLoopStr_0
for p being Series of X,L
for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)