for L being non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )