let L be Field; :: thesis:
let p be non-zero Polynomial of L; :: thesis:
let a be Element of L; :: thesis:
let b be non zero Element of L; :: thesis:
set q = <%a,b%>;
set B = BRoots p;
set C = canFS (Roots p);
set E = canFS (Roots (<%a,b%> *' p));
set F = (BRoots (<%a,b%> *' p)) (++) (canFS (Roots (<%a,b%> *' p)));
set G = (BRoots p) (++) (canFS (Roots p));
consider g being sequence of L such that
A1: SumRoots p = g . (len ((BRoots p) (++) (canFS (Roots p)))) and
A2: g . 0 = 0. L and
A3: for j being Nat
for v being Element of L st j < len ((BRoots p) (++) (canFS (Roots p))) & v = ((BRoots p) (++) (canFS (Roots p))) . (j + 1) holds
g . (j + 1) = (g . j) + v by RLVECT_1:def 12;
A4: len ((BRoots p) (++) (canFS (Roots p))) = len (canFS (Roots p)) by Def1;
A5: len (canFS (Roots p)) = card (Roots p) by FINSEQ_1:93;
A6: dom g = NAT by FUNCT_2:def 1;

suppose A7: not - (a / b) in Roots p ; :: thesis:

then reconsider N = (canFS (Roots p)) ^ <*(- (a / b))*> as Enumeration of Roots (<%a,b%> *' p) by Th16;
A8: len N = 1 + (card (Roots p)) by Th17;
set BN = (BRoots (<%a,b%> *' p)) (++) N;
A9: len ((BRoots (<%a,b%> *' p)) (++) N) = len N by Def1;
A10: Sum ((BRoots (<%a,b%> *' p)) (++) N) = SumRoots (<%a,b%> *' p) by A7, Th24;
set f = g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)));
A11: (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . 0 = g . 0 by FUNCT_7:32;
A12: (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (len ((BRoots (<%a,b%> *' p)) (++) N)) = (- (a / b)) + (SumRoots p) by A5, A9, A8, A4, A6, FUNCT_7:31;

let j be Nat; :: thesis:
let v be Element of L; :: thesis:
assume that
A13: j < len ((BRoots (<%a,b%> *' p)) (++) N) and
A14: v = ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) ; :: thesis:
reconsider C = canFS (Roots p) as Enumeration of Roots p by Th2;
A15: (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j = g . j by A5, A9, A8, A4, A13, FUNCT_7:32;
A16: j + 1 <= len ((BRoots (<%a,b%> *' p)) (++) N) by A13, NAT_1:13;
then A17: ((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) = (((BRoots (<%a,b%> *' p)) * N) . (j + 1)) * (N /. (j + 1)) by Def1, NAT_1:11;
A18: j + 1 in dom N by A9, A16, NAT_1:11, FINSEQ_3:25;
then A19: N . (j + 1) = N /. (j + 1) by PARTFUN1:def 6;
A20: multiplicity ((<%a,b%> *' p),(N /. (j + 1))) = (multiplicity (<%a,b%>,(N /. (j + 1)))) + (multiplicity (p,(N /. (j + 1)))) by UPROOTS:55;
j <= len ((BRoots p) (++) (canFS (Roots p))) by A5, A9, A8, A4, A13, NAT_1:13;

per cases by XXREAL_0:1;

suppose A21: j < len ((BRoots p) (++) (canFS (Roots p))) ; :: thesis:

then j + 1 < 1 + (len ((BRoots p) (++) (canFS (Roots p)))) by XREAL_1:8;
then A22: (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = g . (j + 1) by FUNCT_7:32;
A23: j + 1 <= len ((BRoots p) (++) (canFS (Roots p))) by A21, NAT_1:13;
A24: j + 1 in dom C by A4, A23, NAT_1:11, FINSEQ_3:25;
then A25: C . (j + 1) = C /. (j + 1) by PARTFUN1:def 6;
A26: N /. (j + 1) = C /. (j + 1) by A4, A5, A23, A19, A25, Th17, NAT_1:11;

assume N /. (j + 1) is_a_root_of <%a,b%> ; :: thesis:
then A27: N /. (j + 1) in Roots <%a,b%> by POLYNOM5:def 10;
Roots <%a,b%> = {(- (a / b))} by Th10;
then A28: N /. (j + 1) = - (a / b) by A27, TARSKI:def 1;
A29: C . (j + 1) in rng C by A24, FUNCT_1:def 3;
rng C c= Roots p by FINSEQ_1:def 4;
hence contradiction by A7, A25, A26, A28, A29; :: thesis:

end;

then A30: multiplicity (<%a,b%>,(N /. (j + 1))) = 0 by NAT_1:14, UPROOTS:52;
A31: ((BRoots (<%a,b%> *' p)) * N) . (j + 1) = (BRoots (<%a,b%> *' p)) . (N . (j + 1)) by A18, FUNCT_1:13
.= multiplicity ((<%a,b%> *' p),(N /. (j + 1))) by A19, UPROOTS:def 9
.= (BRoots p) . (C . (j + 1)) by A25, A26, A20, A30, UPROOTS:def 9
.= ((BRoots p) * C) . (j + 1) by A24, FUNCT_1:13 ;
((BRoots (<%a,b%> *' p)) (++) N) . (j + 1) = ((BRoots p) (++) (canFS (Roots p))) . (j + 1) by A23, A26, A31, A17, Def1, NAT_1:11;
hence (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j) + v by A21, A3, A14, A15, A22; :: thesis:

end;

suppose A32: j = len ((BRoots p) (++) (canFS (Roots p))) ; :: thesis:

then A33: (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = (- (a / b)) + (SumRoots p) by A6, FUNCT_7:31;
A34: ((BRoots (<%a,b%> *' p)) * N) . (j + 1) = (BRoots (<%a,b%> *' p)) . (N . (j + 1)) by A18, FUNCT_1:13;
not - (a / b) is_a_root_of p by A7, POLYNOM5:def 10;
then A35: multiplicity (p,(- (a / b))) = 0 by NAT_1:14, UPROOTS:52;
(BRoots (<%a,b%> *' p)) . (N . (j + 1)) = (multiplicity (<%a,b%>,(- (a / b)))) + (multiplicity (p,(- (a / b)))) by A4, A19, A20, A32, UPROOTS:def 9
.= 1 by A35, Th11 ;
hence (g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . (j + 1) = ((g +* ((1 + (len ((BRoots p) (++) (canFS (Roots p))))),((- (a / b)) + (SumRoots p)))) . j) + v by A1, A4, A14, A15, A17, A19, A32, A33, A34, BINOM:13; :: thesis:

end;

end;

end;

hence SumRoots (<%a,b%> *' p) = (- (a / b)) + (SumRoots p) by A2, A12, A11, A10, RLVECT_1:def 12; :: thesis:

end;

suppose A36: - (a / b) in Roots p ; :: thesis:

Roots <%a,b%> = {(- (a / b))} by Th10;
then A37: Roots p = (Roots <%a,b%>) \/ (Roots p) by A36, XBOOLE_1:12, ZFMISC_1:31
.= Roots (<%a,b%> *' p) by UPROOTS:23 ;
reconsider E = canFS (Roots (<%a,b%> *' p)) as Enumeration of Roots (<%a,b%> *' p) by Th2;
A38: len ((BRoots p) (++) E) = len E by Def1;
A39: Sum ((BRoots <%a,b%>) (++) E) = - (a / b) by Th25;
len ((BRoots <%a,b%>) (++) E) = len E by Def1;
then A40: (BRoots <%a,b%>) (++) E is Element of (len E) -tuples_on the carrier of L by FINSEQ_2:92;
A41: (BRoots p) (++) E is Element of (len E) -tuples_on the carrier of L by A38, FINSEQ_2:92;
BRoots (<%a,b%> *' p) = (BRoots <%a,b%>) + (BRoots p) by UPROOTS:56;
hence SumRoots (<%a,b%> *' p) = Sum (((BRoots <%a,b%>) (++) E) + ((BRoots p) (++) E)) by Th19
.= (- (a / b)) + (SumRoots p) by A37, A39, A40, A41, FVSUM_1:76 ;
:: thesis:

end;

end;