let L be algebraic-closed domRing; :: thesis: for p being non-zero Polynomial of L
for r being FinSequence of L st r is one-to-one & len r = (len p) -' 1 & Roots p = rng r holds
Sum r = SumRoots p
let p be non-zero Polynomial of L; :: thesis: for r being FinSequence of L st r is one-to-one & len r = (len p) -' 1 & Roots p = rng r holds
Sum r = SumRoots p
let r be FinSequence of L; :: thesis: ( r is one-to-one & len r = (len p) -' 1 & Roots p = rng r implies Sum r = SumRoots p )
assume that
A1: r is one-to-one and
A2: len r = (len p) -' 1 and
A3: Roots p = rng r ; :: thesis: Sum r = SumRoots p
set B = BRoots p;
set s = support (BRoots p);
set L1 = (len r) |-> 1;
consider f being FinSequence of NAT such that
A4: ( degree (BRoots p) = Sum f & f = (BRoots p) * (canFS (support (BRoots p))) ) by UPROOTS:def 4;
A5: degree (BRoots p) = (len p) -' 1 by UPROOTS:59;
A6: ( card (dom r) = card (rng r) & dom r = Seg (len r) ) by A1, CARD_1:70, FINSEQ_1:def 3;
A7: support (BRoots p) = Roots p by UPROOTS:def 9;
A8: ( support (BRoots p) c= dom (BRoots p) & rng (canFS (support (BRoots p))) = support (BRoots p) ) by PRE_POLY:37, FUNCT_2:def 3;
then A9: dom f = dom (canFS (support (BRoots p))) by A4, RELAT_1:27;
then A10: ( len f = len (canFS (support (BRoots p))) & len (canFS (support (BRoots p))) = card (support (BRoots p)) ) by FINSEQ_3:29, FINSEQ_1:93;
then A11: len f = len r by A3, A6, UPROOTS:def 9;
A12: f is len r -element by A10, A6, A7, A3, CARD_1:def 7;
reconsider E = canFS (support (BRoots p)) as FinSequence of L by A8, FINSEQ_1:def 4;
A13: dom f = dom r by A10, A6, A7, A3, FINSEQ_3:29;
A14: for j being Nat st j in Seg (len r) holds
f . j >= ((len r) |-> 1) . j

proof

let j be Nat; :: thesis: ( j in Seg (len r) implies f . j >= ((len r) |-> 1) . j )
assume A15: j in Seg (len r) ; :: thesis: f . j >= ((len r) |-> 1) . j
A16: (canFS (support (BRoots p))) . j in support (BRoots p) by A13, A9, A6, A8, A15, FUNCT_1:def 3;
then reconsider c = E . j as Element of L ;
c is_a_root_of p by A16, A7, POLYNOM5:def 10;
then multiplicity (p,c) >= 1 by UPROOTS:52;
then (BRoots p) . c >= 1 by UPROOTS:def 9;
then f . j >= 1 by A13, A6, A4, A15, FUNCT_1:12;
hence f . j >= ((len r) |-> 1) . j by A15, FINSEQ_2:57; :: thesis: verum

end;

A17: Sum ((len r) |-> 1) = 1 * (len r) by RVSUM_1:80;
A18: len ((BRoots p) (++) E) = len E by Def1;
for j being Nat st 1 <= j & j <= len E holds
((BRoots p) (++) E) . j = E . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len E implies ((BRoots p) (++) E) . j = E . j )
assume A19: ( 1 <= j & j <= len E ) ; :: thesis: ((BRoots p) (++) E) . j = E . j
A20: j in Seg (len r) by A19, A11, A10;
then ( f . j >= ((len r) |-> 1) . j & f . j <= ((len r) |-> 1) . j & ((len r) |-> 1) . j = 1 ) by A2, A14, A12, A17, A4, A5, RVSUM_1:83, FINSEQ_2:57;
then A21: f . j = 1 by XXREAL_0:1;
A22: E /. j = E . j by A20, A13, A9, A6, PARTFUN1:def 6;
((BRoots p) (++) E) . j = (f . j) * (E /. j) by A4, A19, A18, Def1;
hence ((BRoots p) (++) E) . j = E . j by BINOM:13, A21, A22; :: thesis: verum

end;

then A23: (BRoots p) (++) E = E by A18, FINSEQ_1:14;
E,r are_fiberwise_equipotent by A1, A3, A8, UPROOTS:def 9, RFINSEQ:26;
then ex P being Permutation of (dom E) st E = r * P by CLASSES1:80, A13, A9;
hence Sum r = SumRoots p by A23, RLVECT_2:7, A13, A9, A7; :: thesis: verum