let L be non degenerated comRing; :: thesis: for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for i being Nat st i in dom f & f . i <> 0 holds
z /. i is_a_root_of ~ (Product (rpoly (f,z)))
let z be FinSequence of the carrier of L; :: thesis: for f being NAT -valued FinSequence
for i being Nat st i in dom f & f . i <> 0 holds
z /. i is_a_root_of ~ (Product (rpoly (f,z)))
let f be NAT -valued FinSequence; :: thesis: for i being Nat st i in dom f & f . i <> 0 holds
z /. i is_a_root_of ~ (Product (rpoly (f,z)))
let i be Nat; :: thesis: ( i in dom f & f . i <> 0 implies z /. i is_a_root_of ~ (Product (rpoly (f,z))) )
assume A1: ( i in dom f & f . i <> 0 ) ; :: thesis: z /. i is_a_root_of ~ (Product (rpoly (f,z)))
consider e being FinSequence of the carrier of L such that
A2: eval ((~ (Product (rpoly (f,z)))),(z /. i)) = Product e and
A3: len e = len f and
A4: for j being Nat st 1 <= j & j <= len e holds
e . j = eval ((rpoly ((f /. j),(z /. j))),(z /. i)) by Th50;
A5: eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = 0. L

proof

A6: eval ((rpoly (1,(z /. i))),(z /. i)) = (z /. i) - (z /. i) by HURWITZ:29;
then A7: eval ((rpoly (1,(z /. i))),(z /. i)) = 0. L by VECTSP_1:19;
A8: f . i = f /. i by PARTFUN1:def 6, A1;
f . i >= 1 by A1, NAT_1:14;

per cases then ( f /. i = 1 or f /. i > 1 ) by A8, XXREAL_0:1;

suppose f /. i = 1 ; :: thesis: eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = 0. L

hence eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = 0. L by A6, VECTSP_1:19; :: thesis: verum

end;

suppose f /. i > 1 ; :: thesis: eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = 0. L

then (rpoly (1,(z /. i))) *' (qpoly ((f /. i),(z /. i))) = rpoly ((f /. i),(z /. i)) by HURWITZ:32;
then eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = (eval ((rpoly (1,(z /. i))),(z /. i))) * (eval ((qpoly ((f /. i),(z /. i))),(z /. i))) by POLYNOM4:24;
hence eval ((rpoly ((f /. i),(z /. i))),(z /. i)) = 0. L by A7; :: thesis: verum

end;

end;

end;

( 1 <= i & i <= len e ) by A1, A3, FINSEQ_3:25;
then A9: e . i = eval ((rpoly ((f /. i),(z /. i))),(z /. i)) by A4;
A10: i in dom e by A1, A3, FINSEQ_3:29;
then e /. i = 0. L by A9, A5, PARTFUN1:def 6;
hence z /. i is_a_root_of ~ (Product (rpoly (f,z))) by A2, POLYNOM5:def 7, A10, POLYNOM2:4; :: thesis: verum