let L be Field; :: thesis: for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
let p be non-zero Polynomial of L; :: thesis: for a being Element of L
for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
let a be Element of L; :: thesis: for b being non zero Element of L
for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
let b be non zero Element of L; :: thesis: for E being Enumeration of Roots (<%a,b%> *' p) holds Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
set q = <%a,b%>;
let E be Enumeration of Roots (<%a,b%> *' p); :: thesis: Sum ((BRoots <%a,b%>) (++) E) = - (a / b)
set B = BRoots <%a,b%>;
set F = (BRoots <%a,b%>) (++) E;
A1: len ((BRoots <%a,b%>) (++) E) = len E by Def1;
A2: - (a / b) in {(- (a / b))} by TARSKI:def 1;
A3: Roots <%a,b%> = {(- (a / b))} by Th10;
A4: Roots (<%a,b%> *' p) = (Roots <%a,b%>) \/ (Roots p) by UPROOTS:23;
A5: Roots <%a,b%> c= (Roots <%a,b%>) \/ (Roots p) by XBOOLE_1:7;
A6: dom E = dom ((BRoots <%a,b%>) (++) E) by A1, FINSEQ_3:29;
rng E = Roots (<%a,b%> *' p) by RLAFFIN3:def 1;
then consider j being object such that
A7: j in dom E and
A8: E . j = - (a / b) by A2, A3, A4, A5, FUNCT_1:def 3;
reconsider j = j as Element of NAT by A7;
A9: 1 <= j by A7, FINSEQ_3:25;
A10: j <= len ((BRoots <%a,b%>) (++) E) by A7, A1, FINSEQ_3:25;
A11: E . j = E /. j by A7, PARTFUN1:def 6;
A12: ((BRoots <%a,b%>) * E) . j = (BRoots <%a,b%>) . (E . j) by A7, FUNCT_1:13
.= multiplicity (<%a,b%>,(- (a / b))) by A8, UPROOTS:def 9
.= 1 by Th11 ;

now :: thesis: for i being Element of NAT st i in dom ((BRoots <%a,b%>) (++) E) & i <> j holds
((BRoots <%a,b%>) (++) E) /. i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom ((BRoots <%a,b%>) (++) E) & i <> j implies ((BRoots <%a,b%>) (++) E) /. i = 0. L )
assume that
A13: i in dom ((BRoots <%a,b%>) (++) E) and
A14: i <> j ; :: thesis: ((BRoots <%a,b%>) (++) E) /. i = 0. L
A15: ( 1 <= i & i <= len ((BRoots <%a,b%>) (++) E) ) by A13, FINSEQ_3:25;
A16: E . i = E /. i by A6, A13, PARTFUN1:def 6;
A17: ((BRoots <%a,b%>) * E) . i = (BRoots <%a,b%>) . (E . i) by A6, A13, FUNCT_1:13
.= multiplicity (<%a,b%>,(E /. i)) by A16, UPROOTS:def 9
.= 0 by A16, A8, A6, A7, A13, A14, FUNCT_1:def 4, Th14 ;
thus ((BRoots <%a,b%>) (++) E) /. i = ((BRoots <%a,b%>) (++) E) . i by A13, PARTFUN1:def 6
.= (((BRoots <%a,b%>) * E) . i) * (E /. i) by A15, Def1
.= 0. L by A17, BINOM:12 ; :: thesis: verum

end;

hence Sum ((BRoots <%a,b%>) (++) E) = ((BRoots <%a,b%>) (++) E) /. j by A6, A7, POLYNOM2:3
.= ((BRoots <%a,b%>) (++) E) . j by A6, A7, PARTFUN1:def 6
.= (((BRoots <%a,b%>) * E) . j) * (E /. j) by A9, A10, Def1
.= - (a / b) by A8, A11, A12, BINOM:13 ;
:: thesis: verum