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 st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
let p be non-zero Polynomial of L; :: thesis: for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
let a be Element of L; :: thesis: for b being non zero Element of L st not - (a / b) in Roots p holds
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
let b be non zero Element of L; :: thesis: ( not - (a / b) in Roots p implies for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p)))) )
assume A1: not - (a / b) in Roots p ; :: thesis: for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
set q = <%a,b%>;
set B = BRoots (<%a,b%> *' p);
set C = canFS (Roots p);
set D = canFS (Roots (<%a,b%> *' p));
let E be Enumeration of Roots (<%a,b%> *' p); :: thesis: ( E = (canFS (Roots p)) ^ <*(- (a / b))*> implies Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p)))) )
assume E = (canFS (Roots p)) ^ <*(- (a / b))*> ; :: thesis: Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p))))
then reconsider P = ((canFS (Roots (<%a,b%> *' p))) ") * E as Permutation of (dom E) by A1, Th23;
len ((BRoots (<%a,b%> *' p)) (++) E) = len E by Def1;
then A2: dom ((BRoots (<%a,b%> *' p)) (++) E) = dom E by FINSEQ_3:29;
((canFS (Roots (<%a,b%> *' p))) ") " = canFS (Roots (<%a,b%> *' p)) by FUNCT_1:43;
then A3: P " = (E ") * (canFS (Roots (<%a,b%> *' p))) by FUNCT_1:44;
A4: (E * (E ")) * (canFS (Roots (<%a,b%> *' p))) = canFS (Roots (<%a,b%> *' p))

proof

A5: rng (canFS (Roots (<%a,b%> *' p))) = Roots (<%a,b%> *' p) by FUNCT_2:def 3;
A6: rng E = Roots (<%a,b%> *' p) by RLAFFIN3:def 1;
dom (E * (E ")) = rng E by FUNCT_1:37;
hence A7: dom ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) = dom (canFS (Roots (<%a,b%> *' p))) by A5, A6, RELAT_1:27; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) or ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) . b₁ = (canFS (Roots (<%a,b%> *' p))) . b₁ )
let x be object ; :: thesis: ( not x in dom ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) or ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) . x = (canFS (Roots (<%a,b%> *' p))) . x )
assume A8: x in dom ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) ; :: thesis: ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) . x = (canFS (Roots (<%a,b%> *' p))) . x
(canFS (Roots (<%a,b%> *' p))) . x in rng E by A5, A6, A7, A8, FUNCT_1:def 3;
hence (canFS (Roots (<%a,b%> *' p))) . x = (E * (E ")) . ((canFS (Roots (<%a,b%> *' p))) . x) by FUNCT_1:35
.= ((E * (E ")) * (canFS (Roots (<%a,b%> *' p)))) . x by A8, FUNCT_1:12 ;
:: thesis: verum

end;

((BRoots (<%a,b%> *' p)) (++) E) * (P ") = (BRoots (<%a,b%> *' p)) (++) (E * (P ")) by Th22;
hence Sum ((BRoots (<%a,b%> *' p)) (++) E) = Sum ((BRoots (<%a,b%> *' p)) (++) (E * (P "))) by A2, RLVECT_2:7
.= Sum ((BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p)))) by A3, A4, RELAT_1:36 ;
:: thesis: verum