let L be algebraic-closed Field; :: thesis: for p, q being non-zero Polynomial of L st len p >= 2 holds
SumRoots (p *' q) = (SumRoots p) + (SumRoots q)
let p, q be non-zero Polynomial of L; :: thesis: ( len p >= 2 implies SumRoots (p *' q) = (SumRoots p) + (SumRoots q) )
assume len p >= 2 ; :: thesis: SumRoots (p *' q) = (SumRoots p) + (SumRoots q)
then ( len p <> 0 & len p <> 1 ) ;
then A1: not len p is trivial by NAT_2:28;
defpred S₁[ Nat] means for f being non-zero Polynomial of L st $1 = len f holds
SumRoots (f *' q) = (SumRoots f) + (SumRoots q);
A2: S₁[2]

proof

let f be non-zero Polynomial of L; :: thesis: ( 2 = len f implies SumRoots (f *' q) = (SumRoots f) + (SumRoots q) )
assume len f = 2 ; :: thesis: SumRoots (f *' q) = (SumRoots f) + (SumRoots q)
then consider a being Element of L, b being non zero Element of L such that
A3: f = <%a,b%> by Th6;
SumRoots f = - (a / b) by A3, Th27;
hence SumRoots (f *' q) = (SumRoots f) + (SumRoots q) by A3, Th28; :: thesis: verum

end;

A4: for k being non trivial Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non trivial Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let p be non-zero Polynomial of L; :: thesis: ( k + 1 = len p implies SumRoots (p *' q) = (SumRoots p) + (SumRoots q) )
assume A6: k + 1 = len p ; :: thesis: SumRoots (p *' q) = (SumRoots p) + (SumRoots q)
A7: k >= 2 by NAT_2:29;
k + 1 >= k by NAT_1:11;
then k + 1 >= 2 by A7, XXREAL_0:2;
then len p > 1 by A6, XXREAL_0:2;
then p is with_roots by POLYNOM5:def 9;
then consider r being Element of L such that
A8: r is_a_root_of p ;
set P = poly_quotient (p,r);
A9: (len (poly_quotient (p,r))) + 1 = len p by A6, A8, UPROOTS:def 7;
then reconsider P = poly_quotient (p,r) as non-zero Polynomial of L by A6, UPROOTS:17;
A10: p = <%(- r),(1. L)%> *' P by A8, UPROOTS:50;
then A11: SumRoots p = (- ((- r) / (1. L))) + (SumRoots P) by Th28;
p *' q = <%(- r),(1. L)%> *' (P *' q) by A10, POLYNOM3:33;
hence SumRoots (p *' q) = (- ((- r) / (1. L))) + (SumRoots (P *' q)) by Th28
.= r + ((SumRoots P) + (SumRoots q)) by A5, A6, A9
.= (SumRoots p) + (SumRoots q) by A11, RLVECT_1:def 3 ;
:: thesis: verum

end;

for k being non trivial Nat holds S₁[k] from NAT_2:sch 2(A2, A4);
hence SumRoots (p *' q) = (SumRoots p) + (SumRoots q) by A1; :: thesis: verum