theorem Th5: :: POLYNOM2:6

for L being non empty associative commutative doubleLoopStr
for a being Element of L
for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Product q = a * (Product p)