theorem Th52: :: NUMBER19:52

for L being domRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for x being Element of the carrier of L holds
( x is_a_root_of ~ (Product (rpoly (f,z))) iff ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) )