let L be domRing; :: thesis: for z being FinSequence of the carrier of L holds Roots (~ (Product (rpoly (((len z) |-> 1),z)))) = rng z
let z be FinSequence of the carrier of L; :: thesis: Roots (~ (Product (rpoly (((len z) |-> 1),z)))) = rng z
A1: Roots (~ (Product (rpoly (((len z) |-> 1),z)))) c= rng z

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Roots (~ (Product (rpoly (((len z) |-> 1),z)))) or y in rng z )
assume A2: y in Roots (~ (Product (rpoly (((len z) |-> 1),z)))) ; :: thesis: y in rng z
then reconsider y = y as Element of L ;
y is_a_root_of ~ (Product (rpoly (((len z) |-> 1),z))) by A2, POLYNOM5:def 10;
then consider i being Nat such that
A3: ( i in dom ((len z) |-> 1) & y is_a_root_of rpoly ((((len z) |-> 1) /. i),(z /. i)) ) by Th52;
A4: (len z) |-> 1 = (Seg (len z)) --> 1 by FINSEQ_2:def 2;
then ( ((len z) |-> 1) /. i = ((len z) |-> 1) . i & ((len z) |-> 1) . i = 1 ) by A3, PARTFUN1:def 6, FINSEQ_2:57;
then ( y - (z /. i) = eval ((rpoly ((((len z) |-> 1) /. i),(z /. i))),y) & eval ((rpoly ((((len z) |-> 1) /. i),(z /. i))),y) = 0. L ) by HURWITZ:29, A3, POLYNOM5:def 7;
then A5: y = z /. i by VECTSP_1:19;
A6: i in dom z by A3, A4, FINSEQ_1:def 3;
then z /. i = z . i by PARTFUN1:def 6;
hence y in rng z by A5, A6, FUNCT_1:def 3; :: thesis: verum

end;

rng z c= Roots (~ (Product (rpoly (((len z) |-> 1),z))))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng z or y in Roots (~ (Product (rpoly (((len z) |-> 1),z)))) )
assume y in rng z ; :: thesis: y in Roots (~ (Product (rpoly (((len z) |-> 1),z))))
then consider i being object such that
A7: ( i in dom z & z . i = y ) by FUNCT_1:def 3;
reconsider i = i as Nat by A7;
A8: (len z) |-> 1 = (Seg (len z)) --> 1 by FINSEQ_2:def 2;
i in Seg (len z) by A7, FINSEQ_1:def 3;
then ( i in dom ((len z) |-> 1) & ((len z) |-> 1) . i = 1 ) by A8, FINSEQ_2:57;
then z /. i is_a_root_of ~ (Product (rpoly (((len z) |-> 1),z))) by Th51;
then z /. i in Roots (~ (Product (rpoly (((len z) |-> 1),z)))) by POLYNOM5:def 10;
hence y in Roots (~ (Product (rpoly (((len z) |-> 1),z)))) by A7, PARTFUN1:def 6; :: thesis: verum

end;

hence Roots (~ (Product (rpoly (((len z) |-> 1),z)))) = rng z by A1, XBOOLE_0:def 10; :: thesis: verum