polyvie1.miz



    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 :: POLYVIE1:1

    for a,b be 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 :: POLYVIE1:2

    

     Th2: for X be 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 :: POLYVIE1:3

    for L be right_zeroed non empty addLoopStr, a be 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 :: POLYVIE1:4

    

     Th4: for L be right_unital associative non trivial doubleLoopStr holds for a,b be 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, POLYNOM5: 41;

        hence thesis by UPROOTS: 17;

      end;

    end

    theorem :: POLYVIE1:5

    for L be non trivial ZeroStr, p be Polynomial of L st ( len p) = 1 holds ex a be 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 :: POLYVIE1:6

    

     Th6: for L be non trivial ZeroStr, p be Polynomial of L st ( len p) = 2 holds ex a be Element of L, b be 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;

      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 :: POLYVIE1:7

    for L be non trivial ZeroStr, p be Polynomial of L st ( len p) = 3 holds ex a,b be Element of L, c be 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;

      per cases ;

        suppose n = 0 or n = 1 or n = 2;

        hence (p . n) = ( <%a, b, c%> . n) by NIVEN: 23, NIVEN: 24, NIVEN: 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 :: POLYVIE1:8

    

     Th8: for L be add-associative right_zeroed right_complementable associative commutative left-distributive well-unital almost_left_invertible non empty doubleLoopStr holds for a,b,x be 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 :: POLYVIE1:9

    

     Th9: for L be Field holds for a,x be Element of L holds for b be 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 :: POLYVIE1:10

    

     Th10: for L be Field holds for a be Element of L holds for b be 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 :: POLYVIE1:11

    

     Th11: for L be Field holds for a be Element of L holds for b be 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 be finite non empty Subset of NAT such that

       A1: F = { k where k be Element of NAT : ex q be 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 be Element of NAT such that

       A3: k = j and

       A4: ex q be Polynomial of L st p = ((r `^ k) *' q) by A1;

      consider q be 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 :: POLYVIE1:12

    for L be Field holds for a be Element of L holds for b be 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 :: POLYVIE1:13

    for L be Field holds for a,c be Element of L holds for b,d be 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 :: POLYVIE1:14

    

     Th14: for L be Field holds for a,x be Element of L holds for b be 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 :: POLYVIE1:15

    

     Th15: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be 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 :: POLYVIE1:16

    

     Th16: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be 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 :: POLYVIE1:17

    

     Th17: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be non zero Element of L holds for E be 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 be 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, FINSEQ_1: 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;

      :: POLYVIE1:def1

      func B (++) E -> FinSequence of L means

      : Def1: ( len it ) = ( len E) & for n be 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 be FinSequence of L such that

         A1: ( len z) = ( len E) & for j be 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 be Nat st 1 <= n <= ( len f) holds (f . n) = (((B * E) . n) * (E /. n)) and

         A4: ( len g) = ( len E) and

         A5: for n be 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 :: POLYVIE1:18

    

     Th18: for L be domRing holds for p be non-zero Polynomial of L holds for B be bag of the carrier of L holds for E be 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 :: POLYVIE1:19

    

     Th19: for L be left_zeroed add-associative non empty doubleLoopStr holds for B1,B2 be bag of the carrier of L holds for E be 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 :: POLYVIE1:20

    

     Th20: for L be left_zeroed add-associative non empty doubleLoopStr holds for B be bag of the carrier of L holds for E,F be 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 :: POLYVIE1:21

    for L be left_zeroed add-associative non empty doubleLoopStr holds for B1,B2 be bag of the carrier of L holds for E,F be 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 :: POLYVIE1:22

    

     Th22: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be non zero Element of L holds for E be Enumeration of ( Roots ( <%a, b%> *' p)) holds for P be 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 :: POLYVIE1:23

    

     Th23: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be non zero Element of L st not ( - (a / b)) in ( Roots p) holds for E be 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 :: POLYVIE1:24

    

     Th24: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be non zero Element of L st not ( - (a / b)) in ( Roots p) holds for E be 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 :: POLYVIE1:25

    

     Th25: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be non zero Element of L holds for E be 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 be 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;

      :: POLYVIE1:def2

      func SumRoots (p) -> Element of L equals ( Sum (( BRoots p) (++) ( canFS ( Roots p))));

      coherence ;

    end

    theorem :: POLYVIE1:26

    for L be domRing holds for p be 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 :: POLYVIE1:27

    

     Th27: for L be Field holds for a be Element of L holds for b be 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 be sequence of L such that

       A2: ( Sum F) = (g . ( len F)) and

       A3: (g . 0 ) = ( 0. L) and

       A4: for j be Nat, v be 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 :: POLYVIE1:28

    

     Th28: for L be Field holds for p be non-zero Polynomial of L holds for a be Element of L holds for b be 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 be sequence of L such that

       A1: ( SumRoots p) = (g . ( len G)) and

       A2: (g . 0 ) = ( 0. L) and

       A3: for j be Nat, v be 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;

          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 :: POLYVIE1:29

    for L be Field holds for a,c be Element of L holds for b,d be 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 :: POLYVIE1:30

    for L be algebraic-closed Field holds for p,q be 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 be 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 be Element of L, b be 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 be non trivial Nat st P[k] holds P[(k + 1)]

      proof

        let k be non trivial Nat such that

         A5: P[k];

        let p be 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 be 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 be non trivial Nat holds P[k] from NAT_2:sch 2( A2, A4);

      hence thesis by A1;

    end;

    theorem :: POLYVIE1:31

    for L be algebraic-closed domRing, p be non-zero Polynomial of L holds for r be 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 be 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 be 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 be 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;

    ::$Notion-Name

    theorem :: POLYVIE1:32

    for L be algebraic-closed Field, p be 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 be 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 be Element of L, b be 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 be non trivial Nat st P[k] holds P[(k + 1)]

      proof

        let k be non trivial Nat such that

         A5: P[k];

        let p be 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 be 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 be non trivial Nat holds P[k] from NAT_2:sch 2( A2, A4);

      hence thesis by A1;

    end;