:: Vieta's Formula about the Sum of Roots of Polynomials
::  by Artur Korni{\l}owicz and Karol P\kak
:: 
:: Received May 25, 2017
:: Copyright (c) 2017-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, CARD_3,
      FINSEQ_2, ARYTM_3, ORDINAL4, TARSKI, NAT_1, XXREAL_0, ARYTM_1, XBOOLE_0,
      RLVECT_1, ALGSTR_0, SUPINF_2, PARTFUN1, FINSET_1, ALGSTR_1, ZFMISC_1,
      PRE_POLY, FUNCT_4, VALUED_0, BINOP_1, STRUCT_0, POLYNOM1, POLYNOM3,
      AFINSQ_1, MESFUNC1, VECTSP_1, POLYNOM5, VECTSP_2, POLYNOM2, FUNCT_2,
      UPROOTS, AOFA_I00, XCMPLX_0, POLYVIE1, BINOM, SGRAPH1, CLASSES1;
 notations TARSKI, XBOOLE_0, XCMPLX_0, XXREAL_0, SUBSET_1, NUMBERS, RVSUM_1,
      RELAT_1, FINSET_1, FUNCT_1, RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2,
      CARD_1, CLASSES1, FINSEQ_1, FINSEQ_2, FUNCT_7, XXREAL_2, NAT_1, NAT_D,
      STRUCT_0, VECTSP_2, ALGSTR_0, ALGSTR_1, BINOM, RLVECT_1, RLAFFIN3,
      VECTSP_1, PRE_POLY, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, FVSUM_1,
      GROUP_1, UPROOTS, NIVEN;
 constructors NAT_D, ALGSTR_1, POLYNOM4, POLYNOM5, RECDEF_1, XXREAL_2, FUNCT_7,
      FVSUM_1, ALGSEQ_1, UPROOTS, RLAFFIN3, BINOM, FINSEQ_4, NIVEN, RVSUM_1,
      CLASSES1, WSIERP_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
      XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0,
      VECTSP_1, ALGSTR_1, PRE_POLY, POLYNOM3, POLYNOM4, POLYNOM5, VALUED_0,
      XXREAL_2, FUNCT_2, RELSET_1, UPROOTS, NAT_2, RLVECT_1, RING_3, ALGSTR_0,
      RATFUNC1, NEWTON04, FINSEQ_2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, POLYNOM5;
 equalities FINSEQ_1, ALGSTR_0, BINOM;
 expansions STRUCT_0, POLYNOM5;
 theorems NAT_2, XREAL_0, TARSKI, PRE_POLY, UPROOTS, PBOOLE, POLYNOM5, NAT_1,
      RLVECT_1, VECTSP_1, GROUP_1, VECTSP_2, XXREAL_0, XXREAL_2, POLYNOM4,
      XREAL_1, POLYNOM3, INT_1, FINSEQ_2, FINSEQ_1, RELAT_1, RLVECT_2,
      FINSEQ_4, BINOM, RLAFFIN3, FUNCT_2, NAT_D, ALGSEQ_1, NIVEN, CARD_2,
      FINSEQ_3, FUNCT_1, FUNCT_7, PARTFUN1, STRUCT_0, ALGSTR_0, GRAPHSP,
      ENUMSET1, ZFMISC_1, XBOOLE_1, FVSUM_1, MATRIX14, POLYNOM2, NEWTON02,
      CARD_1, CLASSES1, RVSUM_1, RFINSEQ;
 schemes NAT_2, FINSEQ_2;

begin

Lm1: 2-'1 = 2-1 by XREAL_0:def 2;
Lm2: 2-'2 = 2-2 by XREAL_0:def 2;

registration
  let F be FinSequence;
  let f be Function of dom F,dom F;
  cluster F*f -> FinSequence-like;
  coherence by FINSEQ_2:40;
end;

theorem
  for a,b being object st a <> b holds
  canFS({a,b}) = <*a,b*> or canFS({a,b}) = <*b,a*>
  proof
    let a,b be object;
    rng canFS({a,b}) = {a,b} by FUNCT_2:def 3;
    hence thesis by FINSEQ_3:99;
  end;

theorem Th2:
  for X being finite set holds canFS X is Enumeration of X
  proof
    let X be finite set;
    rng canFS X = X by FUNCT_2:def 3;
    hence thesis by RLAFFIN3:def 1;
  end;

registration
  let A be set;
  let X be finite Subset of A;
  cluster canFS X -> A-valued;
  coherence
  proof
    rng canFS X = X by FUNCT_2:def 3;
    hence rng canFS X c= A;
  end;
end;

theorem
  for L being right_zeroed non empty addLoopStr, a being Element of L
  holds 2 * a = a + a
  proof
    let L be right_zeroed non empty addLoopStr;
    let a be Element of L;
    (Nat-mult-left(L)).(0+1,a) = a + (Nat-mult-left(L)).(0,a) by BINOM:def 3
    .= a + 0.L by BINOM:def 3
    .= a by RLVECT_1:def 4;
    hence a+a = (Nat-mult-left(L)).(1+1,a) by BINOM:def 3
    .= 2*a;
  end;

registration
  let L be almost_left_invertible multLoopStr_0;
  cluster non zero -> left_invertible for Element of L;
  coherence by ALGSTR_0:def 39;
end;

registration
  let L be almost_right_invertible multLoopStr_0;
  cluster non zero -> right_invertible for Element of L;
  coherence by ALGSTR_0:def 40;
end;

registration
  let L be almost_left_cancelable multLoopStr_0;
  cluster non zero -> left_mult-cancelable for Element of L;
  coherence by ALGSTR_0:def 36;
end;

registration
  let L be almost_right_cancelable multLoopStr_0;
  cluster non zero -> right_mult-cancelable for Element of L;
  coherence by ALGSTR_0:def 37;
end;

theorem Th4:
  for L being right_unital associative non trivial doubleLoopStr
  for a,b being Element of L st b is left_invertible right_mult-cancelable
  & b*(/b) = (/b)*b holds a*b/b = a
  proof
    let L be right_unital associative non trivial doubleLoopStr;
    let a,b be Element of L;
    assume
A1: b is left_invertible right_mult-cancelable;
    assume b*(/b) = (/b)*b;
    then b*(/b) = 1.L by A1,ALGSTR_0:def 30;
    hence a = a*(b*(/b))
    .= a*b/b by GROUP_1:def 3;
  end;

registration
  let L be non degenerated ZeroOneStr;
  let z0 be Element of L;
  let z1 be non zero Element of L;
  cluster <%z0,z1%> -> non-zero;
  coherence
  proof
    z1 <> 0.L;
    then len <%z0,z1%> = 2 by POLYNOM5:40;
    hence thesis by UPROOTS:17;
  end;
  cluster <%z1,z0%> -> non-zero;
  coherence
  proof
    z0 <> 0.L or z0 = 0.L;
    then len <%z1,z0%> = 2 or len <%z1,z0%> = 1 by POLYNOM5:40,41;
    hence thesis by UPROOTS:17;
  end;
end;

theorem
  for L being non trivial ZeroStr, p being Polynomial of L st len p = 1
  ex a being non zero Element of L st p = <%a%>
  proof
    let L be non trivial ZeroStr;
    let p be Polynomial of L;
    assume
A1: len p = 1;
    1 = 1+0;
    then p.0 <> 0.L by A1,ALGSEQ_1:10;
    then reconsider a = p.0 as non zero Element of L by STRUCT_0:def 12;
    take a;
    let n be Element of NAT;
    per cases;
    suppose n = 0;
      hence p.n = <%a%>.n by POLYNOM5:32;
    end;
    suppose n > 0;
      then
A2:   0+1 <= n by NAT_1:13;
      hence p.n = 0.L by A1,ALGSEQ_1:8
      .= <%a%>.n by A2,POLYNOM5:32;
    end;
  end;

theorem Th6:
  for L being non trivial ZeroStr, p being Polynomial of L st len p = 2
  ex a being Element of L, b being non zero Element of L st p = <%a,b%>
  proof
    let L be non trivial ZeroStr;
    let p be Polynomial of L;
    assume
A1: len p = 2;
    2 = 1+1;
    then p.1 <> 0.L by A1,ALGSEQ_1:10;
    then reconsider b = p.1 as non zero Element of L by STRUCT_0:def 12;
    take a = p.0, b;
    let n be Element of NAT;
    (n = 0 or ... or n = 1) or n > 1;
    then per cases;
    suppose n = 0 or n = 1;
      hence p.n = <%a,b%>.n by POLYNOM5:38;
    end;
    suppose n > 1;
      then
A2:   1+1 <= n by NAT_1:13;
      hence p.n = 0.L by A1,ALGSEQ_1:8
      .= <%a,b%>.n by A2,POLYNOM5:38;
    end;
  end;

theorem
  for L being non trivial ZeroStr, p being Polynomial of L st len p = 3
  ex a,b being Element of L, c being non zero Element of L st p = <%a,b,c%>
  proof
    let L be non trivial ZeroStr;
    let p be Polynomial of L;
    assume
A1: len p = 3;
    3 = 2+1;
    then p.2 <> 0.L by A1,ALGSEQ_1:10;
    then reconsider c = p.2 as non zero Element of L by STRUCT_0:def 12;
    take a = p.0, b = p.1, c;
    let n be Element of NAT;
    (n = 0 or ... or n = 2) or n > 2;
    then per cases;
    suppose n = 0 or n = 1 or n = 2;
      hence p.n = <%a,b,c%>.n by NIVEN:23,24,25;
    end;
    suppose n > 2;
      then
A2:   2+1 <= n by NAT_1:13;
      hence p.n = 0.L by A1,ALGSEQ_1:8
      .= <%a,b,c%>.n by A2,NIVEN:26;
    end;
  end;

theorem Th8:
  for L being add-associative right_zeroed right_complementable
        associative commutative left-distributive well-unital
        almost_left_invertible non empty doubleLoopStr
  for a,b,x being Element of L st b <> 0.L
  holds eval(<%a,b%>,-a/b) = 0.L
  proof
    let L be add-associative right_zeroed right_complementable
        associative commutative left-distributive well-unital
        almost_left_invertible non empty doubleLoopStr;
    let a,b,x be Element of L;
    assume b <> 0.L;
    then
A1: b*(/b) = 1.L by VECTSP_1:def 10;
    -a/b = (-a)/b by VECTSP_1:9;
    then b*(-a/b) = (-a)*1.L by A1,GROUP_1:def 3
    .= -a;
    hence eval(<%a,b%>,-a/b) = a+-a by POLYNOM5:44
    .= 0.L by RLVECT_1:5;
  end;

theorem Th9:
  for L being Field
  for a,x being Element of L
  for b being non zero Element of L holds
  x is_a_root_of <%a,b%> iff x = -a/b
  proof
    let L be Field;
    let a,x be Element of L;
    let b be non zero Element of L;
    set p = <%a,b%>;
    hereby
      assume
A1:   x is_a_root_of p;
      b*(/b) = (/b)*b;
      then
A2:   b*x/b = x by Th4;
      a+b*x = 0.L by A1,POLYNOM5:44;
      then b*x = -a by RLVECT_1:6;
      hence x = -a/b by A2,VECTSP_1:9;
    end;
    assume x = -a/b;
    hence eval(p,x) = 0.L by Th8;
  end;

theorem Th10:
  for L being Field
  for a being Element of L
  for b being non zero Element of L holds
  Roots <%a,b%> = {-a/b}
  proof
    let L be Field;
    let a be Element of L;
    let b be non zero Element of L;
    set p = <%a,b%>;
    thus Roots p c= {-a/b}
    proof
      let x be object;
      assume
A1:   x in Roots p;
      then reconsider x as Element of L;
      x is_a_root_of p by A1,POLYNOM5:def 10;
      then x = -a/b by Th9;
      hence thesis by TARSKI:def 1;
    end;
    let x be object;
    assume x in {-a/b};
    then
A2: x = -a/b by TARSKI:def 1;
    -a/b is_a_root_of p by Th9;
    hence thesis by A2,POLYNOM5:def 10;
  end;

theorem Th11:
  for L being Field
  for a being Element of L
  for b being non zero Element of L holds
  multiplicity(<%a,b%>,-a/b) = 1
  proof
    let L be Field;
    let a be Element of L;
    let b be non zero Element of L;
    set p = <%a,b%>;
    set x = -a/b;
    set r = <%-x,1.L%>;
    set j = multiplicity(p,x);
    consider F being finite non empty Subset of NAT such that
A1: F = {k where k is Element of NAT : ex q being Polynomial of L st
    p = (r`^k) *' q} and
A2: j = max F by UPROOTS:def 8;
    j in F by A2,XXREAL_2:def 8;
    then consider k being Element of NAT such that
A3: k = j and
A4: ex q being Polynomial of L st p = (r`^k) *' q by A1;
    consider q being Polynomial of L such that
A5: p = (r`^k) *' q by A4;
    b <> 0.L;
    then
A6: len p = 2 by POLYNOM5:40;
A7: now
      assume len q = 0;
      then q = 0_. L by POLYNOM4:5;
      then p = 0_. L by A5,POLYNOM4:2;
      hence contradiction by A6,POLYNOM4:3;
    end;
    then
A8: q is non-zero by UPROOTS:17;
A9: now
      assume k > 1;
      then k >= 1+1 by NAT_1:13;
      then k+len q > 2+(0 qua Nat) by A7,XREAL_1:8;
      hence contradiction by A6,A5,A8,UPROOTS:40;
    end;
    j >= 1 by Th9,UPROOTS:52;
    then k = 1 by A3,A9,XXREAL_0:1;
    then 1 in F by A1,A5;
    then j >= 1 by A2,XXREAL_2:def 8;
    hence thesis by A3,A9,XXREAL_0:1;
  end;

theorem
  for L being Field
  for a being Element of L
  for b being non zero Element of L holds
  BRoots <%a,b%> = ({-a/b},1)-bag
  proof
    let L be Field;
    let a be Element of L;
    let b be non zero Element of L;
    set r = <%a,b%>;
    Roots r = {-a/b} by Th10;
    then
A1: support BRoots r = {-a/b} by UPROOTS:def 9;
A2: -a/b in {-a/b} by TARSKI:def 1;
    now
      let i be object;
      assume i in the carrier of L;
      then reconsider i1 = i as Element of L;
      per cases;
      suppose
A3:     i = -a/b;
        thus (BRoots r).i = multiplicity(r,i1) by UPROOTS:def 9
        .= 1 by A3,Th11
        .= (({-a/b},1)-bag).i by A2,A3,UPROOTS:7;
      end;
      suppose i <> -a/b;
        then
A4:     not i in {-a/b} by TARSKI:def 1;
        hence (BRoots r).i = 0 by A1,PRE_POLY:def 7
        .= (({-a/b},1)-bag).i by A4,UPROOTS:6;
      end;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem
  for L being Field
  for a,c being Element of L
  for b,d being non zero Element of L holds
  Roots(<%a,b%>*'<%c,d%>) = {-a/b,-c/d}
  proof
    let L be Field;
    let a,c be Element of L;
    let b,d be non zero Element of L;
    Roots(<%a,b%>) = {-a/b} & Roots(<%c,d%>) = {-c/d} by Th10;
    hence {-a/b,-c/d} = Roots(<%a,b%>) \/ Roots(<%c,d%>) by ENUMSET1:1
    .= Roots(<%a,b%>*'<%c,d%>) by UPROOTS:23;
  end;

theorem Th14:
  for L being Field
  for a,x being Element of L
  for b being non zero Element of L st x <> -a/b holds
  multiplicity(<%a,b%>,x) = 0
  proof
    let L be Field;
    let a,x be Element of L;
    let b be non zero Element of L;
    assume
A1: x <> -a/b;
    set f = <%a,b%>;
    Roots(f) = {-a/b} by Th10;
    then not x in Roots(f) by A1,TARSKI:def 1;
    then not x is_a_root_of f by POLYNOM5:def 10;
    hence thesis by NAT_1:14,UPROOTS:52;
  end;

theorem Th15:
  for L being Field
  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 card Roots(<%a,b%>*'p) = 1 + card Roots(p)
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L;
A1: Roots(<%a,b%>*'p) = Roots(<%a,b%>) \/ Roots(p) by UPROOTS:23;
    Roots <%a,b%> = {-a/b} by Th10;
    hence thesis by A1,CARD_2:41;
  end;

theorem Th16:
  for L being Field
  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 (canFS Roots(p))^<*-a/b*> is Enumeration of Roots(<%a,b%>*'p)
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L such that
A1: not -a/b in Roots(p);
    set C = canFS Roots(p);
A2: Roots(p) = rng C by FUNCT_2:def 3;
    then
A3: C^<*-a/b*> is one-to-one by A1,GRAPHSP:1;
A4: rng <*-a/b*> = {-a/b} by FINSEQ_1:38;
    Roots <%a,b%> = {-a/b} by Th10;
    then Roots(<%a,b%>*'p) = rng C \/ rng <*-a/b*> by A2,A4,UPROOTS:23
    .= rng(C^<*-a/b*>) by FINSEQ_1:31;
    hence thesis by A3,RLAFFIN3:def 1;
  end;

theorem Th17:
  for L being Field
  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) st E = (canFS Roots(p))^<*-a/b*>
  holds len E = 1 + card Roots(p) &
  E.(1+card Roots(p)) = -a/b &
  for n being Nat st 1 <= n <= card Roots(p) holds E.n = (canFS Roots(p)).n
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L;
    set C = canFS Roots(p);
    let E be Enumeration of Roots(<%a,b%>*'p) such that
A1: E = C^<*-a/b*>;
A2: len C = card Roots(p) by FINSEQ_1:93;
    len <*-a/b*> = 1 by FINSEQ_1:39;
    hence thesis by A1,A2,FINSEQ_1:22,64;
  end;

definition
  let L be non empty doubleLoopStr;
  let B be bag of the carrier of L;
  let E be (the carrier of L)-valued FinSequence;
  func B(++)E -> FinSequence of L means :Def1:
  len it = len E &
  for n being Nat st 1 <= n <= len it holds it.n = (B*E).n * (E/.n);
  existence
  proof
    deffunc F(Nat) = (B*E).$1*(E/.$1);
    consider z being FinSequence of L such that
A1: len z = len E &
    for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
    take z;
    thus thesis by A1,FINSEQ_3:25;
  end;
  uniqueness
  proof
    let f,g be FinSequence of L such that
A2: len f = len E and
A3: for n being Nat st 1 <= n <= len f holds f.n = (B*E).n*(E/.n) and
A4: len g = len E and
A5: for n being Nat st 1 <= n <= len g holds g.n = (B*E).n*(E/.n);
    thus len f = len g by A2,A4;
    let n be Nat;
    assume
A6: 1 <= n <= len f;
    hence f.n = (B*E).n*(E/.n) by A3
    .= g.n by A2,A4,A5,A6;
  end;
end;

theorem Th18:
  for L being domRing
  for p being non-zero Polynomial of L
  for B being bag of the carrier of L
  for E being Enumeration of Roots p st Roots p = {}
  holds B(++)E = {}
  proof
    let L be domRing;
    let p be non-zero Polynomial of L;
    let B be bag of the carrier of L;
    let E be Enumeration of Roots p such that
A1: Roots p = {};
A2: len(B(++)E) = len E by Def1;
    rng E = Roots p by RLAFFIN3:def 1;
    then E = {} by A1;
    hence thesis by A2;
  end;

theorem Th19:
  for L being left_zeroed add-associative non empty doubleLoopStr
  for B1,B2 being bag of the carrier of L
  for E being (the carrier of L)-valued FinSequence
  holds (B1+B2)(++)E = (B1(++)E) + (B2(++)E)
  proof
    let L be left_zeroed add-associative non empty doubleLoopStr;
    let B1,B2 be bag of the carrier of L;
    let E be (the carrier of L)-valued FinSequence;
A1: len(B1(++)E) = len E by Def1;
A2: len(B2(++)E) = len E by Def1;
A3: len((B1+B2)(++)E) = len E by Def1;
    hence
A4: len((B1+B2)(++)E) = len((B1(++)E)+(B2(++)E)) by A1,A2,MATRIX14:2;
    let n be Nat;
    assume
A5: 1 <= n <= len((B1+B2)(++)E);
    then
A6: n in dom((B1(++)E)+(B2(++)E)) by A4,FINSEQ_3:25;
A7: n in dom E by A3,A5,FINSEQ_3:25;
    dom(B1(++)E) = dom(B2(++)E) by A1,A2,FINSEQ_3:29;
    then
A8: (B1(++)E).n = (B1(++)E)/.n & (B2(++)E).n = (B2(++)E)/.n
    by A1,A3,A5,FINSEQ_3:25,PARTFUN1:def 6;
A9: (B1(++)E).n = (B1*E).n * (E/.n) by A1,A3,A5,Def1;
A10: (B2(++)E).n = (B2*E).n * (E/.n) by A2,A3,A5,Def1;
A11: (B1*E).n = B1.(E.n) & (B2*E).n = B2.(E.n) by A7,FUNCT_1:13;
A12: ((B1+B2)*E).n = (B1+B2).(E.n) by A7,FUNCT_1:13
    .= B1.(E.n) + B2.(E.n) by PRE_POLY:def 5;
    thus ((B1+B2)(++)E).n = ((B1+B2)*E).n * (E/.n) by A5,Def1
    .= (B1(++)E)/.n + (B2(++)E)/.n by A8,A9,A10,A11,A12,BINOM:15
    .= ((B1(++)E)+(B2(++)E)).n by A6,A8,FVSUM_1:17;
  end;

theorem Th20:
  for L being left_zeroed add-associative non empty doubleLoopStr
  for B being bag of the carrier of L
  for E,F being (the carrier of L)-valued FinSequence
  holds B(++)(E^F) = (B(++)E) ^ (B(++)F)
  proof
    let L be left_zeroed add-associative non empty doubleLoopStr;
    let B be bag of the carrier of L;
    let E,F be (the carrier of L)-valued FinSequence;
A1: len(B(++)(E^F)) = len(E^F) by Def1;
A2: len(B(++)E) = len E by Def1;
A3: len(B(++)F) = len F by Def1;
A4: len(B(++)E) + len(B(++)F) = len((B(++)E)^(B(++)F)) by FINSEQ_1:22;
A5: len(E^F) = len E + len F by FINSEQ_1:22;
    then
A6: len(B(++)(E^F)) = len(B(++)E) + len(B(++)F) by A2,A3,Def1;
    hence len(B(++)(E^F)) = len((B(++)E)^(B(++)F)) by FINSEQ_1:22;
    let n be Nat;
    assume that
A7: 1 <= n and
A8: n <= len(B(++)(E^F));
A9: (B(++)(E^F)).n = (B*(E^F)).n * ((E^F)/.n) by A7,A8,Def1;
A10: n in dom(E^F) by A1,A7,A8,FINSEQ_3:25;
    then
A11: (B*(E^F)).n = B.((E^F).n) by FUNCT_1:13;
A12: E is FinSequence of L & F is FinSequence of L by NEWTON02:103;
A13: (E^F).n = (E^F)/.n by A10,PARTFUN1:def 6;
    per cases;
    suppose
A14:  n <= len E;
      then
A15:  n in dom E by A7,FINSEQ_3:25;
A16:  (E^F).n = E.n by A7,A14,FINSEQ_1:64;
A17:  (E^F)/.n = E/.n by A15,A12,FINSEQ_4:68;
      (B*E).n = B.(E.n) by A15,FUNCT_1:13;
      hence (B(++)(E^F)).n = (B(++)E).n by A2,A7,A14,A9,A11,A16,A17,Def1
      .= ((B(++)E)^(B(++)F)).n by A2,A7,A14,FINSEQ_1:64;
    end;
    suppose
A18:  n > len E;
      then
A19:  (E^F).n = F.(n-len E) by A1,A8,FINSEQ_1:24;
      set m = n-len(B(++)E);
A20:  m in NAT by A2,A18,INT_1:5;
      n-n < n-len E by A18,XREAL_1:15;
      then
A21:  0+1 <= m by A2,A20,NAT_1:13;
A22:  n-len E <= len E + len F - len E by A1,A8,A5,XREAL_1:9;
      then
A23:  m in dom F by A2,A20,A21,FINSEQ_3:25;
      then
A24:  (B*F).m = B.(F.m) by FUNCT_1:13;
      F/.m = F.m by A23,PARTFUN1:def 6;
      hence (B(++)(E^F)).n = (B(++)F).m
      by A3,A20,A21,A22,A2,A13,A24,A19,A11,A9,Def1
      .= ((B(++)E)^(B(++)F)).n by A2,A6,A4,A8,A18,FINSEQ_1:24;
    end;
  end;

theorem
  for L being left_zeroed add-associative non empty doubleLoopStr
  for B1,B2 being bag of the carrier of L
  for E,F being (the carrier of L)-valued FinSequence
  holds (B1+B2)(++)(E^F) = (B1(++)E)^(B1(++)F) + (B2(++)E)^(B2(++)F)
  proof
    let L be left_zeroed add-associative non empty doubleLoopStr;
    let B1,B2 be bag of the carrier of L;
    let E,F be (the carrier of L)-valued FinSequence;
    thus (B1+B2)(++)(E^F) = (B1(++)(E^F)) + (B2(++)(E^F)) by Th19
    .= (B1(++)E)^(B1(++)F) + (B2(++)(E^F)) by Th20
    .= (B1(++)E)^(B1(++)F) + (B2(++)E)^(B2(++)F) by Th20;
  end;

theorem Th22:
  for L being Field
  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)
  for P being Permutation of dom E
  holds (BRoots(<%a,b%>*'p)(++)E)*P = BRoots(<%a,b%>*'p)(++)(E*P)
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L;
    set q = <%a,b%>;
    set B = BRoots(q*'p);
    let E be Enumeration of Roots(q*'p);
    let P be Permutation of dom E;
    len E = len(B(++)E) by Def1;
    then
A1: dom E = dom(B(++)E) by FINSEQ_3:29;
    then reconsider P1 = P as Permutation of dom(B(++)E);
    (B(++)E)*P1 = B(++)(E*P)
    proof
A2:   len(E*P) = len(B(++)(E*P)) by Def1;
A3:   rng P = dom E by FUNCT_2:def 3;
      then
A4:   dom((B(++)E)*P1) = dom(P1) by A1,RELAT_1:27;
A5:   dom(P1) = dom(E*P) by A3,RELAT_1:27;
      hence
A6:   len((B(++)E)*P1) = len(B(++)(E*P)) by A2,A4,FINSEQ_3:29;
      let n be Nat such that
A7:   1 <= n and
A8:   n <= len((B(++)E)*P1);
A9:   n in dom((B(++)E)*P1) by A7,A8,FINSEQ_3:25;
A10:  (B*E).(P1.n) = (B*E*P1).n by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
      .= (B*(E*P)).n by RELAT_1:36;
A11:  P1.n in rng P1 by A4,A9,FUNCT_1:def 3;
      then
A12:  1 <= P1.n & P1.n <= len(B(++)E) by FINSEQ_3:25;
A13:  E/.(P1.n) = E.(P1.n) by A3,A11,PARTFUN1:def 6
      .= (E*P1).n by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
      .= (E*P)/.n by A4,A5,A7,A8,FINSEQ_3:25,PARTFUN1:def 6;
      thus ((B(++)E)*P1).n = (B(++)E).(P1.n) by A4,A7,A8,FINSEQ_3:25,FUNCT_1:13
      .= (B*E).(P1.n) * (E/.(P1.n)) by A12,Def1
      .= (B(++)(E*P)).n by A6,A7,A8,A10,A13,Def1;
    end;
    hence thesis;
  end;

theorem Th23:
  for L being Field
  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)
  for E being Enumeration of Roots(<%a,b%>*'p) st E = (canFS Roots(p))^<*-a/b*>
  holds (canFS Roots(<%a,b%>*'p))" * E is Permutation of dom E
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L such that
A1: not -a/b in Roots(p);
    set q = <%a,b%>;
    set e = <*-a/b*>;
    set B = BRoots(q*'p);
    set C = canFS Roots(p);
    set D = canFS Roots(q*'p);
    let E be Enumeration of Roots(q*'p) such that
A2: E = C^e;
A3: dom E = Seg(len C + len e) by A2,FINSEQ_1:def 7;
A4: len C = card Roots(p) by FINSEQ_1:93;
A5: len e = 1 by FINSEQ_1:40;
A6: card Roots(q*'p) = 1 + card Roots(p) by A1,Th15;
A7: rng D = Roots(q*'p) by FUNCT_2:def 3;
A8: rng(D") = dom D by FUNCT_1:33;
A9: dom(D") = rng D by FUNCT_1:33;
A10: dom D = Seg len D by FINSEQ_1:def 3;
A11: len D = card Roots(q*'p) by FINSEQ_1:93;
A12: Roots(q*'p) = Roots(q) \/ Roots(p) by UPROOTS:23;
A13: rng C = Roots(p) by FUNCT_2:def 3;
A14: rng e = {-a/b} by FINSEQ_1:39;
A15: Roots(q) = {-a/b} by Th10;
A16: rng(E) = rng C \/ rng e by A2,FINSEQ_1:31;
     then
A17: rng(D"*E) = rng(D") by A9,A12,A13,A14,A15,RELAT_1:28;
    dom(D"*E) = dom(E) by A7,A9,A12,A13,A14,A15,A16,RELAT_1:27;
    then D"*E is Function of dom E,dom E
    by A3,A4,A5,A6,A8,A10,A11,A17,FUNCT_2:1;
    hence D"*E is Permutation of dom E
    by A3,A4,A5,A6,A8,A10,A11,A17,FUNCT_2:57;
  end;

theorem Th24:
  for L being Field
  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)
  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))
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L such that
A1: not -a/b in Roots(p);
    set q = <%a,b%>;
    set B = BRoots(q*'p);
    set C = canFS Roots(p);
    set D = canFS Roots(q*'p);
    let E be Enumeration of Roots(q*'p);
    assume E = C^<*-a/b*>;
    then reconsider P = D"*E as Permutation of dom E by A1,Th23;
    len(B(++)E) = len E by Def1;
    then
A2: dom(B(++)E) = dom E by FINSEQ_3:29;
    D"" = D by FUNCT_1:43;
    then
A3: P" = E"*D by FUNCT_1:44;
A4: E*E"*D = D
    proof
A5:   rng D = Roots(q*'p) by FUNCT_2:def 3;
A6:   rng E = Roots(q*'p) by RLAFFIN3:def 1;
      dom(E*E") = rng E by FUNCT_1:37;
      hence
A7:   dom(E*E"*D) = dom D by A5,A6,RELAT_1:27;
      let x be object such that
A8:   x in dom(E*E"*D);
      D.x in rng E by A5,A6,A7,A8,FUNCT_1:def 3;
      hence D.x = (E*E").(D.x) by FUNCT_1:35
      .= (E*E"*D).x by A8,FUNCT_1:12;
    end;
    (B(++)E)*P" = B(++)(E*P") by Th22;
    hence Sum(B(++)E) = Sum(B(++)(E*P")) by A2,RLVECT_2:7
    .= Sum(B(++)D) by A3,A4,RELAT_1:36;
  end;

theorem Th25:
  for L being Field
  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
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L;
    set q = <%a,b%>;
    let E be Enumeration of Roots(q*'p);
    set B = BRoots(q);
    set F = B(++)E;
A1: len F = len E by Def1;
A2: -a/b in {-a/b} by TARSKI:def 1;
A3: Roots(q) = {-a/b} by Th10;
A4: Roots(q*'p) = Roots(q) \/ Roots(p) by UPROOTS:23;
A5: Roots(q) c= Roots(q) \/ Roots(p) by XBOOLE_1:7;
A6: dom E = dom F by A1,FINSEQ_3:29;
    rng E = Roots(q*'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 as Element of NAT by A7;
A9: 1 <= j by A7,FINSEQ_3:25;
A10: j <= len F by A7,A1,FINSEQ_3:25;
A11: E.j = E/.j by A7,PARTFUN1:def 6;
A12: (B*E).j = B.(E.j) by A7,FUNCT_1:13
     .= multiplicity(<%a,b%>,-a/b) by A8,UPROOTS:def 9
     .= 1 by Th11;
    now
      let i be Element of NAT such that
A13:  i in dom F and
A14:  i <> j;
A15:  1 <= i & i <= len F by A13,FINSEQ_3:25;
A16:  E.i = E/.i by A6,A13,PARTFUN1:def 6;
A17:  (B*E).i = B.(E.i) by A6,A13,FUNCT_1:13
      .= multiplicity(q,E/.i) by A16,UPROOTS:def 9
      .= 0 by A16,A8,A6,A7,A13,A14,FUNCT_1:def 4,Th14;
      thus F/.i = F.i by A13,PARTFUN1:def 6
      .= (B*E).i * (E/.i) by A15,Def1
      .= 0.L by A17,BINOM:12;
    end;
    hence Sum F = F/.j by A6,A7,POLYNOM2:3
    .= F.j by A6,A7,PARTFUN1:def 6
    .= (B*E).j * (E/.j) by A9,A10,Def1
    .= -a/b by A8,A11,A12,BINOM:13;
  end;

definition
  let L be domRing;
  let p be non-zero Polynomial of L;
  func SumRoots(p) -> Element of L equals
  Sum (BRoots(p)(++)canFS Roots p);
  coherence;
end;

theorem
  for L being domRing
  for p being non-zero Polynomial of L st Roots p = {} holds
  SumRoots p = 0.L
  proof
    let L be domRing;
    let p be non-zero Polynomial of L such that
A1: Roots p = {};
    canFS Roots p is Enumeration of Roots p by Th2;
    then BRoots(p)(++)canFS Roots p = {} by A1,Th18;
    then len (BRoots(p)(++)canFS Roots p) = 0;
    hence thesis by RLVECT_1:75;
  end;

theorem Th27:
  for L being Field
  for a being Element of L
  for b being non zero Element of L holds
  SumRoots <%a,b%> = -a/b
  proof
    let L be Field;
    let a be Element of L;
    let b be non zero Element of L;
    set p = <%a,b%>;
    set B = BRoots(p);
A1: Roots p = {-a/b} by Th10;
    reconsider E = canFS Roots p as Enumeration of Roots p by Th2;
    set F = B(++)E;
    consider g being sequence of L such that
A2: Sum(F) = g.(len F) and
A3: g.0 = 0.L and
A4: for j being Nat, v being Element of L st j < len F & v = F.(j+1)
    holds g.(j+1) = g.j + v by RLVECT_1:def 12;
A5: E = <*-a/b*> by A1,FINSEQ_1:94;
A6: len F = len E by Def1;
A7: len E = 1 by A5,FINSEQ_1:39;
A8: 1 in dom E by A7,FINSEQ_3:25;
A9: (B*E).1 = B.(E.1) by A8,FUNCT_1:13
     .= multiplicity(p,-a/b) by A5,UPROOTS:def 9
     .= 1 by Th11;
A10: F.1 = (B*E).1*(E/.1) by A6,A7,Def1
    .= E/.1 by A9,BINOM:13;
    then reconsider v = F.1 as Element of L;
A11: 0 < len F by A7,Def1;
    thus SumRoots p = g.(0+1) by A2,A7,Def1
    .= g.0 + v by A4,A11
    .= -a/b by A5,A3,A10,FINSEQ_4:16;
  end;

theorem Th28:
  for L being Field
  for p being non-zero Polynomial of L
  for a being Element of L
  for b being non zero Element of L
  holds SumRoots(<%a,b%>*'p) = -a/b + SumRoots(p)
  proof
    let L be Field;
    let p be non-zero Polynomial of L;
    let a be Element of L;
    let b be non zero Element of L;
    set q = <%a,b%>;
    set B = BRoots p;
    set C = canFS Roots(p);
    set E = canFS Roots(q*'p);
    set F = BRoots(q*'p)(++)E;
    set G = B(++)C;
    consider g being sequence of L such that
A1: SumRoots(p) = g.(len G) and
A2: g.0 = 0.L and
A3: for j being Nat, v being Element of L st j < len G & v = G.(j+1)
    holds g.(j+1) = g.j + v by RLVECT_1:def 12;
A4: len G = len C by Def1;
A5: len C = card Roots(p) by FINSEQ_1:93;
A6: dom g = NAT by FUNCT_2:def 1;
    per cases;
    suppose
A7:   not -a/b in Roots(p);
      then reconsider N = C^<*-a/b*> as Enumeration of Roots(q*'p) by Th16;
A8:   len N = 1 + card Roots(p) by Th17;
      set BN = BRoots(q*'p)(++)N;
A9:   len BN = len N by Def1;
A10:  Sum(BN) = SumRoots(q*'p) by A7,Th24;
      set f = g+*(1+len G,-a/b+SumRoots(p));
A11:  f.0 = g.0 by FUNCT_7:32;
A12:  f.(len BN) = -a/b+SumRoots(p) by A5,A9,A8,A4,A6,FUNCT_7:31;
      now
        let j be Nat, v be Element of L such that
A13:    j < len BN and
A14:    v = BN.(j+1);
        reconsider C as Enumeration of Roots(p) by Th2;
A15:    f.j = g.j by A5,A9,A8,A4,A13,FUNCT_7:32;
A16:    j+1 <= len BN by A13,NAT_1:13;
        then
A17:    BN.(j+1) = (BRoots(q*'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(q*'p,N/.(j+1)) =
        multiplicity(q,N/.(j+1))+multiplicity(p,N/.(j+1)) by UPROOTS:55;
        j <= len G by A5,A9,A8,A4,A13,NAT_1:13;
        then per cases by XXREAL_0:1;
        suppose
A21:      j < len G;
          then j+1 < 1+len G by XREAL_1:8;
          then
A22:      f.(j+1) = g.(j+1) by FUNCT_7:32;
A23:      j+1 <= len G 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;
          now
            assume N/.(j+1) is_a_root_of q;
            then
A27:        N/.(j+1) in Roots(q) 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;
          end;
          then
A30:      multiplicity(q,N/.(j+1)) = 0 by NAT_1:14,UPROOTS:52;
A31:      (BRoots(q*'p)*N).(j+1) = (BRoots(q*'p)).(N.(j+1)) by A18,FUNCT_1:13
          .= multiplicity(q*'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;
          BN.(j+1) = G.(j+1) by A23,A26,A31,A17,Def1,NAT_1:11;
          hence f.(j+1) = f.j + v by A21,A3,A14,A15,A22;
        end;
        suppose
A32:      j = len G;
          then
A33:      f.(j+1) = -a/b+SumRoots(p) by A6,FUNCT_7:31;
A34:      (BRoots(q*'p)*N).(j+1) = (BRoots(q*'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(q*'p)).(N.(j+1)) = multiplicity(q,-a/b)+multiplicity(p,-a/b)
          by A4,A19,A20,A32,UPROOTS:def 9
          .= 1 by A35,Th11;
          hence f.(j+1) = f.j + v
          by A1,A4,A14,A15,A17,A19,A32,A33,A34,BINOM:13;
        end;
      end;
      hence thesis by A2,A12,A11,A10,RLVECT_1:def 12;
    end;
    suppose
A36:  -a/b in Roots(p);
      Roots(q) = {-a/b} by Th10;
      then
A37:  Roots(p) = Roots(q) \/ Roots(p) by A36,XBOOLE_1:12,ZFMISC_1:31
      .= Roots(q*'p) by UPROOTS:23;
      reconsider E as Enumeration of Roots(q*'p) by Th2;
A38:  len(B(++)E) = len E by Def1;
A39:  Sum(BRoots(q)(++)E) = -a/b by Th25;
      len(BRoots(q)(++)E) = len E by Def1;
      then
A40:  (BRoots(q)(++)E) is Element of (len E)-tuples_on the carrier of L
      by FINSEQ_2:92;
A41:  (B(++)E) is Element of (len E)-tuples_on the carrier of L
      by A38,FINSEQ_2:92;
      BRoots(q*'p) = BRoots(q) + BRoots(p) by UPROOTS:56;
      hence SumRoots(q*'p) = Sum((BRoots(q)(++)E)+(BRoots(p)(++)E)) by Th19
      .= -a/b + SumRoots(p) by A37,A39,A40,A41,FVSUM_1:76;
    end;
  end;

theorem
  for L being Field
  for a,c being Element of L
  for b,d being non zero Element of L
  holds SumRoots(<%a,b%>*'<%c,d%>) = (-a/b) + (-c/d)
  proof
    let L be Field;
    let a,c be Element of L;
    let b,d be non zero Element of L;
    SumRoots(<%a,b%>) = -a/b & SumRoots(<%c,d%>) = -c/d by Th27;
    hence thesis by Th28;
  end;

theorem
  for L being algebraic-closed Field
  for p,q being non-zero Polynomial of L st
  len p >= 2 holds SumRoots(p*'q) = SumRoots(p) + SumRoots(q)
  proof
    let L be algebraic-closed Field;
    let p,q be non-zero Polynomial of L;
    assume len p >= 2;
    then len p <> 0 & len p <> 1;
    then
A1: len p is non trivial by NAT_2:28;
    defpred P[Nat] means
    for f being non-zero Polynomial of L st $1 = len f holds
    SumRoots(f*'q) = SumRoots(f) + SumRoots(q);
A2: P[2]
    proof
      let f be non-zero Polynomial of L;
      assume len f = 2;
      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 thesis by A3,Th28;
    end;
A4: for k being non trivial Nat st P[k] holds P[k+1]
    proof
      let k be non trivial Nat such that
A5:   P[k];
      let p being non-zero Polynomial of L such that
A6:   k+1 = len p;
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 P + 1 = len p by A6,A8,UPROOTS:def 7;
      then reconsider P 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;
    end;
    for k being non trivial Nat holds P[k] from NAT_2:sch 2(A2,A4);
    hence thesis by A1;
  end;

theorem
  for L being algebraic-closed domRing, 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
  proof
    let L be algebraic-closed domRing, p be non-zero Polynomial of L;
    let r be FinSequence of L such that
A1: r is one-to-one and
A2: len r = len p-'1 and
A3: Roots p = rng r;
    set B = BRoots p, s = support B;
    set L1 = (len r) |-> 1;
    consider f being FinSequence of NAT such that
A4: degree B = Sum f & f = B * canFS s by UPROOTS:def 4;
A5: degree B = 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: s = Roots p by UPROOTS:def 9;
A8: s c= dom B & rng canFS s = s by PRE_POLY:37,FUNCT_2:def 3;
    then
A9: dom f = dom canFS s by A4,RELAT_1:27;
    then
A10: len f = len canFS s = card s 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 s 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 >= L1.j
    proof
      let j be Nat such that
A15:  j in Seg len r;
A16:  (canFS s).j in s 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 B.c >= 1 by UPROOTS:def 9;
      then f.j >= 1 by A13,A6,A4,A15,FUNCT_1:12;
      hence thesis by A15,FINSEQ_2:57;
    end;
A17: Sum L1 = 1*len r by RVSUM_1:80;
A18: len (B(++)E) = len E by Def1;
    for j being Nat st 1 <= j <= len E holds (B(++)E).j = E.j
    proof
      let j be Nat such that
A19:  1 <=j <= len E;
A20:  j in Seg len r by A19,A11,A10;
      then f.j >= L1.j & f.j <= L1.j & L1.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;
      (B(++)E).j = (f.j) * (E/.j) by A4,A19,A18,Def1;
      hence thesis by BINOM:13,A21,A22;
    end;
    then
A23: B(++)E = E by A18,FINSEQ_1:14;
    E,r are_fiberwise_equipotent by A1,A3,A8,UPROOTS:def 9,RFINSEQ:26;
    then ex P be Permutation of dom E st E = r*P by CLASSES1:80,A13,A9;
    hence thesis by A23,RLVECT_2:7,A13,A9,A7;
  end;

::$N Vieta's formula about the sum of roots
theorem
  for L being algebraic-closed Field, p being non-zero Polynomial of L holds
  len p >= 2 implies SumRoots p = - p.(len p-'2) / p.(len p-'1)
  proof
    let L be algebraic-closed Field, p be non-zero Polynomial of L;
    assume len p >= 2;
    then len p <> 0 & len p <> 1;
    then
A1: len p is non trivial by NAT_2:28;
    defpred P[Nat] means
    for p being non-zero Polynomial of L holds
    $1 = len p implies SumRoots p = - p.($1-'2) / p.($1-'1);
A2: P[2]
    proof
      let p be non-zero Polynomial of L;
      assume len p = 2;
      then consider a being Element of L, b being non zero Element of L
      such that
A3:   p = <%a,b%> by Th6;
      p.0 = a & p.1 = b by A3,POLYNOM5:38;
      hence thesis by A3,Lm1,Lm2,Th27;
    end;
A4: for k being non trivial Nat st P[k] holds P[k+1]
    proof
      let k be non trivial Nat such that
A5:   P[k];
      let p being non-zero Polynomial of L such that
A6:   k+1 = len p;
A7:   k+1-'1 = k by NAT_D:34;
      k-1 >= 2-1 by XREAL_1:9,NAT_2:29;
      then
A8:   k+1-'2 = k+1-2 by XREAL_0:def 2
      .= k-1;
      then reconsider k1 = k-1 as Nat;
A9:   k >= 2 by NAT_2:29;
      k+1 >= k by NAT_1:11;
      then k+1 >= 2 by A9,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
A10:  r is_a_root_of p;
      set P = poly_quotient(p,r);
A11:  len P + 1 = len p by A6,A10,UPROOTS:def 7;
      then reconsider P as non-zero Polynomial of L by A6,UPROOTS:17;
      reconsider k2 = k-2 as Element of NAT by NAT_2:29,INT_1:5;
A12:  k-'2 = k2 by XREAL_0:def 2;
A13:  k-'1 = k1 by XREAL_0:def 2;
A14:  P.k = 0.L by A6,A11,ALGSEQ_1:8;
A15:  p = <%-r,1.L%>*'P by A10,UPROOTS:50;
      then
A16:  p.(k1+1) = (-r)*P.(k1+1)+1.L*P.k1 by UPROOTS:37;
A17:  p.(k2+1) = (-r)*P.(k2+1)+1.L*P.k2 by A15,UPROOTS:37;
      -((-r)*P.k1) = (--r)*P.k1 by VECTSP_1:9;
      then
A18:  -((-r)*P.k1+P.k2) = r*P.k1 - P.k2 by RLVECT_1:30;
A19:  len P = k1+1 by A6,A11;
      then
A20:  P.k1 <> 0.L by ALGSEQ_1:10;
A21:  P.k1*(/P.k1) = (/P.k1)*P.k1;
      P.k1 is non zero by A19,ALGSEQ_1:10;
      then
A22:  r = r*P.k1/P.k1 by A21,Th4;
      thus SumRoots(p) = -(-r)/1.L + SumRoots(P) by A15,Th28
      .= r - P.k2/P.k1 by A5,A6,A11,A12,A13
      .= (r*P.k1-P.k2) / P.k1 by A20,A22,VECTSP_2:20
      .= - p.(k+1-'2) / p.(k+1-'1) by A7,A8,A14,A16,A17,A18,A20,VECTSP_2:19;
    end;
    for k being non trivial Nat holds P[k] from NAT_2:sch 2(A2,A4);
    hence thesis by A1;
  end;