let L be domRing; :: thesis: 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)) ) )
let z be FinSequence of the carrier of L; :: thesis: 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)) ) )
let f be NAT -valued FinSequence; :: thesis: 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)) ) )
let x be Element of the carrier of L; :: thesis: ( 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)) ) )
consider e being FinSequence of the carrier of L such that
A1: eval ((~ (Product (rpoly (f,z)))),x) = Product e and
A2: len e = len f and
A3: for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) by Th50;
A4: dom e = dom f by A2, FINSEQ_3:29;
thus ( x is_a_root_of ~ (Product (rpoly (f,z))) implies ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) ) :: thesis: ( ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) implies x is_a_root_of ~ (Product (rpoly (f,z))) )

proof

assume x is_a_root_of ~ (Product (rpoly (f,z))) ; :: thesis: ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) )
then consider i being Nat such that
A5: ( i in dom e & e . i = 0. L ) by A1, RING_2:2, POLYNOM5:def 7;
( 1 <= i & i <= len e ) by A5, FINSEQ_3:25;
then e . i = eval ((rpoly ((f /. i),(z /. i))),x) by A3;
hence ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) by A4, A5, POLYNOM5:def 7; :: thesis: verum

end;

given i being Nat such that A6: ( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) ; :: thesis: x is_a_root_of ~ (Product (rpoly (f,z)))
( 1 <= i & i <= len e ) by A6, A2, FINSEQ_3:25;
then A7: e . i = eval ((rpoly ((f /. i),(z /. i))),x) by A3;
Product e = 0. L by A7, A4, A6, RING_2:2, POLYNOM5:def 7;
hence x is_a_root_of ~ (Product (rpoly (f,z))) by A1, POLYNOM5:def 7; :: thesis: verum