uproots.miz



    begin

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: UPROOTS:1

    

     Th1: for f be FinSequence of NAT st for i be Element of NAT st i in ( dom f) holds (f . i) <> 0 holds ( Sum f) = ( len f) iff f = (( len f) |-> 1)

    proof

      defpred P[ Nat] means for f be FinSequence of NAT st ( len f) = $1 & for i be Element of NAT st i in ( dom f) holds (f . i) <> 0 holds ( Sum f) = ( len f) iff f = (( len f) |-> 1);

      let f be FinSequence of NAT ;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        let f be FinSequence of NAT such that

         A3: ( len f) = (n + 1) and

         A4: for i be Element of NAT st i in ( dom f) holds (f . i) <> 0 ;

        consider g be FinSequence of NAT , a be Element of NAT such that

         A5: f = (g ^ <*a*>) by A3, FINSEQ_2: 19;

         A6:

        now

          let i be Element of NAT ;

          

           A7: ( dom g) c= ( dom f) by A5, FINSEQ_1: 26;

          assume

           A8: i in ( dom g);

          then (f . i) = (g . i) by A5, FINSEQ_1:def 7;

          hence (g . i) <> 0 by A4, A8, A7;

        end;

        (n + 1) = (( len g) + ( len <*a*>)) by A3, A5, FINSEQ_1: 22;

        then

         A9: (n + 1) = (( len g) + 1) by FINSEQ_1: 40;

        then ( dom f) = ( Seg ( len f)) & (f . ( len f)) = a by A3, A5, FINSEQ_1: 42, FINSEQ_1:def 3;

        then a <> 0 by A3, A4, FINSEQ_1: 4;

        then

         A10: ( 0 qua Nat + 1) <= a by NAT_1: 13;

        

         A11: g is FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

        hereby

          reconsider h = (( len g) |-> jj) as FinSequence of REAL ;

          reconsider h1 = h as Element of (( len h) -tuples_on REAL ) by FINSEQ_2: 92;

          reconsider g1 = g as Element of (( len g) -tuples_on REAL ) by A11, FINSEQ_2: 92;

          assume

           A12: ( Sum f) = ( len f);

          

           A13: ( Sum g) = ((( Sum g) + a) - a)

          .= ((n + 1) - a) by A3, A5, A12, RVSUM_1: 74;

           A14:

          now

            let j be Nat;

            reconsider a = j as Element of NAT by ORDINAL1:def 12;

            assume

             A15: j in ( Seg ( len g));

            then j in ( dom g) by FINSEQ_1:def 3;

            then (g . j) <> 0 by A6;

            then ( 0 qua Nat + 1) <= (g . a) by NAT_1: 13;

            hence (h1 . j) <= (g1 . j) by A15, FUNCOP_1: 7;

          end;

          

           A16: ( Sum h1) <= ( Sum g1) by A14, RVSUM_1: 82;

          ( Sum h) = (n * 1) by A9, RVSUM_1: 80

          .= n;

          then (n + a) <= (((n + 1) - a) + a) by A16, A13, XREAL_1: 6;

          then a <= 1 by XREAL_1: 6;

          then

           A17: a = 1 by A10, XXREAL_0: 1;

          then g = (( len g) |-> 1) by A2, A9, A6, A13;

          hence f = (( len f) |-> 1) by A3, A5, A9, A17, FINSEQ_2: 60;

        end;

        assume f = (( len f) |-> 1);

        

        then

         A18: f = ((n |-> 1) ^ (1 |-> 1)) by A3, FINSEQ_2: 123

        .= ((n |-> 1) ^ <*1*>) by FINSEQ_2: 59;

        then

         A19: a = 1 by A5, FINSEQ_2: 17;

        

         A20: ( Sum f) = (( Sum g) + a) by A5, RVSUM_1: 74;

        g = (( len g) |-> 1) by A5, A9, A18, FINSEQ_2: 17;

        hence thesis by A2, A3, A9, A6, A20, A19;

      end;

      

       A21: P[ 0 ]

      proof

        let f be FinSequence of NAT such that

         A22: ( len f) = 0 and for i be Element of NAT st i in ( dom f) holds (f . i) <> 0 ;

        thus ( Sum f) = ( len f) implies f = (( len f) |-> 1) by A22;

        assume f = (( len f) |-> 1);

        f = {} by A22;

        hence thesis by RVSUM_1: 72;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A21, A1);

      hence thesis;

    end;

    scheme :: UPROOTS:sch1

    IndFinSeq0 { k() -> Nat , P[ set] } :

for i be Element of NAT st 1 <= i & i <= k() holds P[i]

      provided

       A1: P[1]

       and

       A2: for i be Element of NAT st 1 <= i & i < k() holds P[i] implies P[(i + 1)];

      defpred Q[ Nat] means 1 <= $1 & $1 <= k() & not P[$1];

      assume not for i be Element of NAT st 1 <= i & i <= k() holds P[i];

      then

       A3: ex k be Nat st Q[k];

      consider k be Nat such that

       A4: Q[k] & for k9 be Nat st Q[k9] holds k <= k9 from NAT_1:sch 5( A3);

      per cases ;

        suppose k = 1;

        hence thesis by A1, A4;

      end;

        suppose

         A5: k <> 1;

        (1 - 1) <= (k - 1) by A4, XREAL_1: 9;

        then

        reconsider k9 = (k - 1) as Element of NAT by INT_1: 3;

        

         A6: ((k - 1) + 1) = (k + 0 qua Nat);

        1 < k by A4, A5, XXREAL_0: 1;

        then

         A7: 1 <= k9 by A6, NAT_1: 13;

        k9 <= (k9 + 1) & k9 <> (k9 + 1) by NAT_1: 11;

        then

         A8: k9 < k by XXREAL_0: 1;

        then k9 < k() by A4, XXREAL_0: 2;

        hence thesis by A2, A4, A6, A8, A7;

      end;

    end;

    theorem :: UPROOTS:2

    

     Th2: for L be add-associative right_zeroed right_complementable non empty addLoopStr, r be FinSequence of L st ( len r) >= 2 & for k be Element of NAT st 2 < k & k in ( dom r) holds (r . k) = ( 0. L) holds ( Sum r) = ((r /. 1) + (r /. 2))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr, r be FinSequence of L such that

       A1: ( len r) >= 2 and

       A2: for k be Element of NAT st 2 < k & k in ( dom r) holds (r . k) = ( 0. L);

      

       A3: 2 in ( dom r) by A1, FINSEQ_3: 25;

      1 <= ( len r) by A1, XXREAL_0: 2;

      then

       A4: 1 in ( dom r) by FINSEQ_3: 25;

       not r is empty by A1;

      then

      consider a be Element of L, r1 be FinSequence of L such that

       A5: a = (r . 1) and

       A6: r = ( <*a*> ^ r1) by FINSEQ_3: 102;

      

       A7: ( len <*a*>) = 1 by FINSEQ_1: 40;

      

      then

       A8: (r . 2) = (r1 . (2 - 1)) by A1, A6, FINSEQ_1: 24

      .= (r1 . 1);

      ( len r) = (1 + ( len r1)) by A6, A7, FINSEQ_1: 22;

      then r1 is non empty by A1;

      then

      consider b be Element of L, r2 be FinSequence of L such that

       A9: b = (r1 . 1) and

       A10: r1 = ( <*b*> ^ r2) by FINSEQ_3: 102;

      

       A11: ( len <*b*>) = 1 by FINSEQ_1: 40;

       A12:

      now

        let i be Element of NAT such that

         A13: i in ( dom r2);

        

         A14: (1 + i) in ( dom r1) by A10, A11, A13, FINSEQ_1: 28;

        1 <= i by A13, FINSEQ_3: 25;

        then 1 < (1 + i) by NAT_1: 13;

        then

         A15: (1 + 1) < (1 + (1 + i)) by XREAL_1: 8;

        

        thus (r2 . i) = (r1 . (1 + i)) by A10, A11, A13, FINSEQ_1:def 7

        .= (r . (1 + (1 + i))) by A6, A7, A14, FINSEQ_1:def 7

        .= ( 0. L) by A2, A6, A7, A14, A15, FINSEQ_1: 28;

      end;

      

      thus ( Sum r) = (a + ( Sum r1)) by A6, FVSUM_1: 72

      .= (a + (b + ( Sum r2))) by A10, FVSUM_1: 72

      .= (a + (b + ( 0. L))) by A12, POLYNOM3: 1

      .= (a + b) by RLVECT_1:def 4

      .= ((r /. 1) + b) by A5, A4, PARTFUN1:def 6

      .= ((r /. 1) + (r /. 2)) by A9, A3, A8, PARTFUN1:def 6;

    end;

    begin

    definition

      ::$Canceled

      let X be set, S be finite Subset of X, n be Element of NAT ;

      :: UPROOTS:def2

      func (S,n) -bag -> Element of ( Bags X) equals (( EmptyBag X) +* (S --> n));

      correctness

      proof

        set b = (( EmptyBag X) +* (S --> n));

        

         A1: ( EmptyBag X) = (X --> 0 ) by PBOOLE:def 3;

        

         A2: ( dom (S --> n)) = S by FUNCOP_1: 13;

         A3:

        now

          let i be object;

          assume not i in S;

          

          hence (b . i) = (( EmptyBag X) . i) by A2, FUNCT_4: 11

          .= 0 by PBOOLE: 5;

        end;

         A4:

        now

          let i be set such that

           A5: i in S;

          

          thus (b . i) = ((S --> n) . i) by A2, A5, FUNCT_4: 13

          .= n by A5, FUNCOP_1: 7;

        end;

        

         A6: ( support b) is finite

        proof

          per cases ;

            suppose

             A7: S is empty;

            now

              assume ( support b) is non empty;

              then

              consider x be object such that

               A8: x in ( support b) by XBOOLE_0:def 1;

              (b . x) <> 0 by A8, PRE_POLY:def 7;

              hence contradiction by A3, A7;

            end;

            hence thesis;

          end;

            suppose

             A9: S is non empty & n = 0 ;

            now

              assume ( support b) is non empty;

              then

              consider x be object such that

               A10: x in ( support b) by XBOOLE_0:def 1;

              

               A11: (b . x) <> 0 by A10, PRE_POLY:def 7;

              

              then (b . x) = ((S --> n) . x) by A2, A3, FUNCT_4: 13

              .= 0 by A3, A9, A11, FUNCOP_1: 7;

              hence contradiction by A10, PRE_POLY:def 7;

            end;

            hence thesis;

          end;

            suppose S is non empty & n <> 0 ;

            then for x be object holds x in S iff (b . x) <> 0 by A3, A4;

            hence thesis by PRE_POLY:def 7;

          end;

        end;

        ( dom b) = (( dom ( EmptyBag X)) \/ ( dom (S --> n))) by FUNCT_4:def 1

        .= (X \/ ( dom (S --> n))) by A1, FUNCOP_1: 13

        .= (X \/ S) by FUNCOP_1: 13

        .= X by XBOOLE_1: 12;

        then (( EmptyBag X) +* (S --> n)) is bag of X by A6, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

        hence thesis by PRE_POLY:def 12;

      end;

    end

    ::$Canceled

    theorem :: UPROOTS:6

    

     Th3: for X be set, S be finite Subset of X, n be Element of NAT , i be object st not i in S holds (((S,n) -bag ) . i) = 0

    proof

      let X be set, S be finite Subset of X, n be Element of NAT , i be object such that

       A1: not i in S;

      ( dom (S --> n)) = S by FUNCOP_1: 13;

      

      hence (((S,n) -bag ) . i) = (( EmptyBag X) . i) by A1, FUNCT_4: 11

      .= 0 by PBOOLE: 5;

    end;

    theorem :: UPROOTS:7

    

     Th4: for X be set, S be finite Subset of X, n be Element of NAT , i be set st i in S holds (((S,n) -bag ) . i) = n

    proof

      let X be set, S be finite Subset of X, n be Element of NAT , i be set such that

       A1: i in S;

      ( dom (S --> n)) = S by FUNCOP_1: 13;

      

      hence (((S,n) -bag ) . i) = ((S --> n) . i) by A1, FUNCT_4: 13

      .= n by A1, FUNCOP_1: 7;

    end;

    theorem :: UPROOTS:8

    

     Th5: for X be set, S be finite Subset of X, n be Element of NAT st n <> 0 holds ( support ((S,n) -bag )) = S

    proof

      let X be set, S be finite Subset of X, n be Element of NAT ;

      assume n <> 0 ;

      then for x be object holds x in S iff (((S,n) -bag ) . x) <> 0 by Th3, Th4;

      hence thesis by PRE_POLY:def 7;

    end;

    theorem :: UPROOTS:9

    for X be set, S be finite Subset of X, n be Element of NAT st S is empty or n = 0 holds ((S,n) -bag ) = ( EmptyBag X)

    proof

      let X be set, S be finite Subset of X, n be Element of NAT such that

       A1: S is empty or n = 0 ;

      now

        let i be object;

        assume i in X;

        per cases ;

          suppose i in S;

          

          hence (((S,n) -bag ) . i) = 0 by A1, Th4

          .= (( EmptyBag X) . i) by PBOOLE: 5;

        end;

          suppose not i in S;

          

          hence (((S,n) -bag ) . i) = 0 by Th3

          .= (( EmptyBag X) . i) by PBOOLE: 5;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: UPROOTS:10

    

     Th7: for X be set, S,T be finite Subset of X, n be Element of NAT st S misses T holds (((S \/ T),n) -bag ) = (((S,n) -bag ) + ((T,n) -bag ))

    proof

      let X be set, S,T be finite Subset of X, n be Element of NAT ;

      assume S misses T;

      then

       A1: (S /\ T) = {} by XBOOLE_0:def 7;

      now

        let i be object such that i in X;

        per cases by XBOOLE_0:def 3;

          suppose

           A2: not i in (S \/ T);

          then

           A3: not i in T by XBOOLE_0:def 3;

          

           A4: not i in S by A2, XBOOLE_0:def 3;

          

          thus ((((S \/ T),n) -bag ) . i) = 0 by A2, Th3

          .= ((((S,n) -bag ) . i) + 0 qua Nat) by A4, Th3

          .= ((((S,n) -bag ) . i) + (((T,n) -bag ) . i)) by A3, Th3

          .= ((((S,n) -bag ) + ((T,n) -bag )) . i) by PRE_POLY:def 5;

        end;

          suppose

           A5: i in S;

          then

           A6: not i in T by A1, XBOOLE_0:def 4;

          i in (S \/ T) by A5, XBOOLE_0:def 3;

          

          hence ((((S \/ T),n) -bag ) . i) = n by Th4

          .= ((((S,n) -bag ) . i) + 0 qua Nat) by A5, Th4

          .= ((((S,n) -bag ) . i) + (((T,n) -bag ) . i)) by A6, Th3

          .= ((((S,n) -bag ) + ((T,n) -bag )) . i) by PRE_POLY:def 5;

        end;

          suppose

           A7: i in T;

          then

           A8: not i in S by A1, XBOOLE_0:def 4;

          i in (S \/ T) by A7, XBOOLE_0:def 3;

          

          hence ((((S \/ T),n) -bag ) . i) = n by Th4

          .= ((((T,n) -bag ) . i) + 0 qua Nat) by A7, Th4

          .= ((((S,n) -bag ) . i) + (((T,n) -bag ) . i)) by A8, Th3

          .= ((((S,n) -bag ) + ((T,n) -bag )) . i) by PRE_POLY:def 5;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    definition

      let X be set;

      mode Rbag of X is real-valued finite-support ManySortedSet of X;

    end

    definition

      let A be set, b be Rbag of A;

      :: UPROOTS:def3

      func Sum b -> Real means

      : Def2: ex f be FinSequence of REAL st it = ( Sum f) & f = (b * ( canFS ( support b)));

      existence

      proof

        set cS = ( canFS ( support b));

        set f = (b * cS);

        

         A1: ( rng f) c= REAL ;

        ( support b) c= ( dom b) & ( rng cS) = ( support b) by FUNCT_2:def 3, PRE_POLY: 37;

        then ( dom f) = ( dom cS) by RELAT_1: 27;

        then ( dom f) = ( Seg ( len cS)) by FINSEQ_1:def 3;

        then f is FinSequence by FINSEQ_1:def 2;

        then

        reconsider f as FinSequence of REAL by A1, FINSEQ_1:def 4;

        take ( Sum f);

        thus thesis;

      end;

      uniqueness ;

    end

    notation

      let A be set, b be bag of A;

      synonym degree b for Sum b;

    end

    definition

      let A be set, b be bag of A;

      :: original: degree

      redefine

      :: UPROOTS:def4

      func degree b -> Element of NAT means

      : Def3: ex f be FinSequence of NAT st it = ( Sum f) & f = (b * ( canFS ( support b)));

      coherence

      proof

        consider f be FinSequence of REAL such that

         A1: ( degree b) = ( Sum f) and

         A2: f = (b * ( canFS ( support b))) by Def2;

        ( rng f) c= NAT

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) and

           A4: y = (f . x) by FUNCT_1:def 3;

          (f . x) = (b . (( canFS ( support b)) . x)) by A2, A3, FUNCT_1: 12;

          hence thesis by A4;

        end;

        then

        reconsider f as FinSequence of NAT by FINSEQ_1:def 4;

        ( Sum f) is Element of NAT ;

        hence thesis by A1;

      end;

      compatibility

      proof

        set cS = ( canFS ( support b));

        let n be Element of NAT ;

        hereby

          consider f be FinSequence of REAL such that

           A5: ( degree b) = ( Sum f) and

           A6: f = (b * ( canFS ( support b))) by Def2;

          

           A7: ( rng f) c= NAT

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A8: x in ( dom f) and

             A9: y = (f . x) by FUNCT_1:def 3;

            (f . x) = (b . (( canFS ( support b)) . x)) by A6, A8, FUNCT_1: 12;

            hence thesis by A9;

          end;

          assume

           A10: n = ( degree b);

          reconsider f as FinSequence of NAT by A7, FINSEQ_1:def 4;

          take f;

          thus n = ( Sum f) & f = (b * cS) by A10, A5, A6;

        end;

        given f be FinSequence of NAT such that

         A11: n = ( Sum f) & f = (b * cS);

        ( rng f) c= REAL ;

        then

        reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

        f = f;

        hence thesis by A11, Def2;

      end;

    end

    theorem :: UPROOTS:11

    

     Th8: for A be set, b be Rbag of A st b = ( EmptyBag A) holds ( Sum b) = 0

    proof

      let A be set, b be Rbag of A;

      set cS = ( canFS ( support b));

      assume b = ( EmptyBag A);

      then (b * cS) = ( <*> NAT );

      hence thesis by Def2, RVSUM_1: 72;

    end;

    theorem :: UPROOTS:12

    

     Th9: for A be set, b be bag of A st ( Sum b) = 0 holds b = ( EmptyBag A)

    proof

      let A be set, b be bag of A;

      set cS = ( canFS ( support b));

      consider f be FinSequence of NAT such that

       A1: ( degree b) = ( Sum f) and

       A2: f = (b * ( canFS ( support b))) by Def3;

      assume

       A3: ( degree b) = 0 ;

      now

        assume

         A4: ( support b) <> {} ;

        consider x be object such that

         A5: x in ( support b) by A4, XBOOLE_0:def 1;

        x in ( rng cS) by A5, FUNCT_2:def 3;

        then

        consider i be Nat such that

         A6: i in ( dom cS) and

         A7: (cS . i) = x by FINSEQ_2: 10;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        (f . i) = (b . (cS . i)) by A2, A6, FUNCT_1: 13;

        then

         A8: (f . i) <> 0 by A5, A7, PRE_POLY:def 7;

        ( support b) c= ( dom b) by PRE_POLY: 37;

        then

         A9: i in ( dom f) & 0 < (f . i) by A8, A2, A5, A6, A7, FUNCT_1: 11;

        for i be Nat st i in ( dom f) holds 0 <= (f . i);

        hence contradiction by A3, A1, A9, RVSUM_1: 85;

      end;

      hence thesis by PRE_POLY: 81;

    end;

    theorem :: UPROOTS:13

    

     Th10: for A be set, S be finite Subset of A, b be bag of A holds S = ( support b) & ( degree b) = ( card S) iff b = ((S,1) -bag )

    proof

      let A be set, S be finite Subset of A, b be bag of A;

      set cS = ( canFS S);

      set f = (b * cS);

      

       A1: ( dom b) = A by PARTFUN1:def 2;

      set g = (( card S) |-> 1);

      

       A2: ( len cS) = ( card S) by FINSEQ_1: 93;

      

       A3: ( rng cS) = S by FUNCT_2:def 3;

      then

       A4: ( dom f) = ( dom cS) by A1, RELAT_1: 27;

      then ( dom f) = ( Seg ( len cS)) by FINSEQ_1:def 3;

      then

      reconsider f as FinSequence by FINSEQ_1:def 2;

      

       A5: ( len cS) = ( len f) by A4, FINSEQ_3: 29;

      hereby

        set sb = ((S,1) -bag );

        assume that

         A6: S = ( support b) and

         A7: ( degree b) = ( card S);

        consider F be FinSequence of NAT such that

         A8: ( degree b) = ( Sum F) and

         A9: F = (b * cS) by A6, Def3;

        now

          let i be Element of NAT ;

          assume i in ( dom F);

          then (F . i) = (b . (cS . i)) & (cS . i) in ( rng cS) by A4, A9, FUNCT_1: 3, FUNCT_1: 12;

          hence (F . i) <> 0 by A6, PRE_POLY:def 7;

        end;

        then

         A10: F = (( len F) |-> 1) by A2, A5, A7, A8, A9, Th1;

        

         A11: ( support b) = ( support sb) by A6, Th5;

        now

          thus ( dom b) = ( dom sb) by A1, PARTFUN1:def 2;

          let x be object;

          assume x in ( dom b);

          per cases ;

            suppose

             A12: x in ( support b);

            then

             A13: ((cS " ) . x) in ( dom cS) by A3, A6, FUNCT_1: 32;

            then

             A14: ((cS " ) . x) in ( Seg ( len F)) by A4, A9, FINSEQ_1:def 3;

            ( rng cS) = ( support b) by A6, FUNCT_2:def 3;

            

            hence (b . x) = (b . (cS . ((cS " ) . x))) by A12, FUNCT_1: 35

            .= (F . ((cS " ) . x)) by A9, A13, FUNCT_1: 13

            .= 1 by A10, A14, FUNCOP_1: 7

            .= (sb . x) by A6, A12, Th4;

          end;

            suppose

             A15: not x in ( support b);

            

            hence (b . x) = 0 by PRE_POLY:def 7

            .= (sb . x) by A11, A15, PRE_POLY:def 7;

          end;

        end;

        hence b = ((S,1) -bag );

      end;

      ( rng f) c= NAT

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A16: x in ( dom f) and

         A17: y = (f . x) by FUNCT_1:def 3;

        (f . x) = (b . (cS . x)) by A16, FUNCT_1: 12;

        hence thesis by A17;

      end;

      then

      reconsider f as FinSequence of NAT by FINSEQ_1:def 4;

      assume

       A18: b = ((S,1) -bag );

      

       A19: ( rng cS) = S by FUNCT_2:def 3;

      now

        thus ( len f) = ( card S) by A4, A2, FINSEQ_3: 29;

        thus ( len g) = ( card S) by CARD_1:def 7;

        let i be Nat;

        

         A20: ( dom f) = ( Seg ( card S)) by A4, A2, FINSEQ_1:def 3;

        assume

         A21: i in ( dom f);

        

        hence (f . i) = (b . (cS . i)) by FUNCT_1: 12

        .= 1 by A4, A19, A18, A21, Th4, FUNCT_1: 3

        .= (g . i) by A20, A21, FUNCOP_1: 7;

      end;

      then

       A22: f = g by FINSEQ_2: 9;

      thus S = ( support b) by A18, Th5;

      then ( degree b) = ( Sum f) by Def3;

      

      hence ( degree b) = (( card S) * 1) by A22, RVSUM_1: 80

      .= ( card S);

    end;

    theorem :: UPROOTS:14

    

     Th11: for A be set, S be finite Subset of A, b be Rbag of A st ( support b) c= S holds ex f be FinSequence of REAL st f = (b * ( canFS S)) & ( Sum b) = ( Sum f)

    proof

      let A be set, S be finite Subset of A, b be Rbag of A such that

       A1: ( support b) c= S;

      

       A2: ( card ( support b)) <= ( card S) by A1, NAT_1: 43;

      set cs = ( canFS ( support b));

      

       A3: ( rng cs) = ( support b) by FUNCT_2:def 3;

      set cS = ( canFS S);

      set f = (b * cS);

      ( len cS) = ( card S) by FINSEQ_1: 93;

      then

       A4: ( dom cS) = ( Seg ( card S)) by FINSEQ_1:def 3;

      ( len cs) = ( card ( support b)) by FINSEQ_1: 93;

      then

       A5: ( dom cs) = ( Seg ( card ( support b))) by FINSEQ_1:def 3;

      consider g be FinSequence of REAL such that

       A6: ( Sum b) = ( Sum g) and

       A7: g = (b * cs) by Def2;

      

       A8: ( dom b) = A by PARTFUN1:def 2;

      then

       A9: ( dom g) = ( Seg ( card ( support b))) by A1, A7, A5, A3, RELAT_1: 27, XBOOLE_1: 1;

      then

       A10: ( len g) = ( card ( support b)) by FINSEQ_1:def 3;

      

       A11: ( rng cS) = S by FUNCT_2:def 3;

      then

       A12: ( dom f) = ( Seg ( card S)) by A4, A8, RELAT_1: 27;

      then

      reconsider f as FinSequence by FINSEQ_1:def 2;

      ( rng f) c= ( rng b) by RELAT_1: 26;

      then ( rng f) c= REAL by XBOOLE_1: 1;

      then

      reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

      take f;

      thus f = (b * ( canFS S));

      per cases by A2, XXREAL_0: 1;

        suppose

         A13: ( card ( support b)) < ( card S);

        set dd = { j where j be Element of NAT : j in ( dom f) & (f . j) = 0 };

         A14:

        now

          consider x be object such that

           A15: not (x in ( support b) iff x in S) by A13, TARSKI: 2;

          consider j be object such that

           A16: j in ( dom cS) and

           A17: (cS . j) = x by A1, A11, A15, FUNCT_1:def 3;

          reconsider j as Element of NAT by A16;

          (f . j) = (b . x) by A16, A17, FUNCT_1: 13;

          then (f . j) = 0 by A1, A15, PRE_POLY:def 7;

          then j in dd by A4, A12, A16;

          hence dd is non empty;

        end;

        reconsider gr = g as FinSequence of REAL ;

        

         A18: dd c= ( dom f)

        proof

          let x be object;

          assume x in dd;

          then ex j be Element of NAT st x = j & j in ( dom f) & (f . j) = 0 ;

          hence thesis;

        end;

        then

        reconsider dd as finite non empty set by A14;

        consider d be Element of NAT such that

         A19: ( card S) = (( card ( support b)) + d) and 1 <= d by A13, FINSEQ_4: 84;

        set h = (d |-> ( In ( 0 , REAL )));

        set F = (gr ^ h);

        ( rng ( canFS dd)) = dd & dd c= NAT by A18, FUNCT_2:def 3, XBOOLE_1: 1;

        then

        reconsider cdd = ( canFS dd) as FinSequence of NAT by FINSEQ_1:def 4;

        set cdi = (cdd qua Function " );

        reconsider cdi as Function of dd, ( Seg ( card dd)) by FINSEQ_1: 95;

        reconsider cdi as Function of dd, NAT by FUNCT_2: 7;

        deffunc Z( object) = ((cdi /. $1) + ( card ( support b)));

        consider z be Function such that

         A20: ( dom z) = dd and

         A21: for x be object st x in dd holds (z . x) = Z(x) from FUNCT_1:sch 3;

        set p = (((cs " ) * cS) +* z);

        

         A22: ( dom cdi) = dd by FUNCT_2:def 1;

        set cSr = (cS | (( dom f) \ dd));

        now

          let y be object;

          hereby

            assume y in ( rng cSr);

            then

            consider x be object such that

             A23: x in ( dom cSr) and

             A24: y = (cSr . x) by FUNCT_1:def 3;

            

             A25: (cSr . x) = (cS . x) by A23, FUNCT_1: 47;

            x in ( dom cS) by A23, RELAT_1: 57;

            then

            reconsider j = x as Element of NAT ;

            ( dom cSr) c= (( dom f) \ dd) by RELAT_1: 58;

            then

             A26: x in (( findom f) \ dd) by A23;

            then not j in dd by XBOOLE_0:def 5;

            then

             A27: (f . j) <> 0 by A26;

            x in ( dom cS) by A23, RELAT_1: 57;

            then (b . (cS . j)) <> 0 by A27, FUNCT_1: 13;

            hence y in ( support b) by A24, A25, PRE_POLY:def 7;

          end;

          assume

           A28: y in ( support b);

          then

          consider x be object such that

           A29: x in ( dom cS) and

           A30: y = (cS . x) by A1, A11, FUNCT_1:def 3;

          now

            assume x in dd;

            then

            consider j be Element of NAT such that

             A31: j = x and

             A32: j in ( dom f) & (f . j) = 0 ;

             0 = (b . (cS . j)) by A4, A12, A32, FUNCT_1: 13;

            hence contradiction by A28, A30, A31, PRE_POLY:def 7;

          end;

          then x in (( dom f) \ dd) by A4, A12, A29, XBOOLE_0:def 5;

          hence y in ( rng cSr) by A29, A30, FUNCT_1: 50;

        end;

        then

         A33: ( rng cSr) = ( support b) by TARSKI: 2;

        ((( findom f) \ dd) /\ ( dom f)) = (( dom f) \ dd) by XBOOLE_1: 28;

        then cSr is one-to-one & ( dom cSr) = (( dom f) \ dd) by A4, A12, FUNCT_1: 52, RELAT_1: 61;

        then (( support b),(( dom f) \ dd)) are_equipotent by A33, WELLORD2:def 4;

        then

         A34: ( card ( support b)) = ( card (( dom f) \ dd)) by CARD_1: 5;

        ( card (( dom f) \ dd)) = (( card ( dom f)) - ( card dd)) by A18, CARD_2: 44;

        then

         A35: (( card ( support b)) + ( card dd)) = ( card S) by A12, A34, FINSEQ_1: 57;

         A36:

        now

          

           A37: ( dom (cs " )) = ( support b) by A3, FUNCT_1: 33;

          assume (( dom ((cs " ) * cS)) /\ ( dom z)) <> {} ;

          then

          consider x be object such that

           A38: x in (( dom ((cs " ) * cS)) /\ ( dom z)) by XBOOLE_0:def 1;

          x in ( dom z) by A38, XBOOLE_0:def 4;

          then

          consider j be Element of NAT such that

           A39: j = x and j in ( dom f) and

           A40: (f . j) = 0 by A20;

          

           A41: x in ( dom ((cs " ) * cS)) by A38, XBOOLE_0:def 4;

          then j in ( dom cS) by A39, FUNCT_1: 11;

          then (f . j) = (b . (cS . j)) by FUNCT_1: 13;

          then not (cS . j) in ( support b) by A40, PRE_POLY:def 7;

          hence contradiction by A41, A39, A37, FUNCT_1: 11;

        end;

        ( len F) = (( len g) + ( len h)) by FINSEQ_1: 22

        .= ( card S) by A10, A19, CARD_1:def 7;

        then

         A42: ( dom F) = ( Seg ( card S)) by FINSEQ_1:def 3;

        now

          let x be object;

          hereby

            assume

             A43: x in (( dom ((cs " ) * cS)) \/ ( dom z));

            per cases by A43, XBOOLE_0:def 3;

              suppose x in ( dom ((cs " ) * cS));

              hence x in ( dom F) by A4, A42, FUNCT_1: 11;

            end;

              suppose x in ( dom z);

              hence x in ( dom F) by A12, A42, A18, A20;

            end;

          end;

          assume

           A44: x in ( dom F);

          then

          reconsider i = x as Element of NAT ;

          per cases ;

            suppose (f . x) = 0 ;

            then i in ( dom z) by A12, A42, A20, A44;

            hence x in (( dom ((cs " ) * cS)) \/ ( dom z)) by XBOOLE_0:def 3;

          end;

            suppose

             A45: (f . x) <> 0 ;

            (f . i) = (b . (cS . i)) by A4, A42, A44, FUNCT_1: 13;

            then (cS . i) in ( support b) by A45, PRE_POLY:def 7;

            then (cS . i) in ( dom (cs " )) by A3, FUNCT_1: 33;

            then i in ( dom ((cs " ) * cS)) by A4, A42, A44, FUNCT_1: 11;

            hence x in (( dom ((cs " ) * cS)) \/ ( dom z)) by XBOOLE_0:def 3;

          end;

        end;

        then

         A46: (( dom ((cs " ) * cS)) \/ ( dom z)) = ( dom F) by TARSKI: 2;

        then

         A47: ( dom p) = ( dom F) by FUNCT_4:def 1;

        ( len cdd) = ( card dd) by FINSEQ_1: 93;

        then

         A48: ( dom cdd) = ( Seg d) by A19, A35, FINSEQ_1:def 3;

        then

         A49: ( rng cdi) = ( Seg d) by FUNCT_1: 33;

        

         A50: ( rng z) c= ( Seg ( card S))

        proof

          let y be object;

          assume y in ( rng z);

          then

          consider x be object such that

           A51: x in ( dom z) and

           A52: y = (z . x) by FUNCT_1:def 3;

          

           A53: (cdi /. x) = (cdi . x) & (cdi . x) in ( Seg d) by A22, A49, A20, A51, FUNCT_1: 3, PARTFUN1:def 6;

          then 1 <= (cdi /. x) by FINSEQ_1: 1;

          then

           A54: 1 <= ((cdi /. x) + ( card ( support b))) by NAT_1: 12;

          (cdi /. x) <= d by A53, FINSEQ_1: 1;

          then

           A55: ((cdi /. x) + ( card ( support b))) <= (d + ( card ( support b))) by XREAL_1: 6;

          y = ((cdi /. x) + ( card ( support b))) by A20, A21, A51, A52;

          hence thesis by A19, A54, A55, FINSEQ_1: 1;

        end;

         A56:

        now

          let x be object such that

           A57: x in ( dom F);

          per cases by A46, A57, XBOOLE_0:def 3;

            suppose

             A58: x in ( dom ((cs " ) * cS));

            then (((cs " ) * cS) . x) in ( rng ((cs " ) * cS)) by FUNCT_1: 3;

            then (((cs " ) * cS) . x) in ( rng (cs " )) by FUNCT_1: 14;

            then

             A59: (((cs " ) * cS) . x) in ( dom cs) by FUNCT_1: 33;

             not x in ( dom z) by A36, A58, XBOOLE_0:def 4;

            then

             A60: (p . x) = (((cs " ) * cS) . x) by FUNCT_4: 11;

            ( Seg ( card ( support b))) c= ( Seg ( card S)) by A2, FINSEQ_1: 5;

            hence (p . x) in ( dom F) by A5, A42, A60, A59;

          end;

            suppose x in ( dom z);

            then (p . x) = (z . x) & (z . x) in ( rng z) by FUNCT_1: 3, FUNCT_4: 13;

            hence (p . x) in ( dom F) by A42, A50;

          end;

        end;

        

         A61: ( dom p) = (( dom ((cs " ) * cS)) \/ ( dom z)) by FUNCT_4:def 1;

        reconsider p as Function of ( dom F), ( dom F) by A47, A56, FUNCT_2: 3;

        ( len h) = d by CARD_1:def 7;

        then

         A62: ( dom h) = ( Seg d) by FINSEQ_1:def 3;

        

         A63: ( rng cdd) = dd by FUNCT_2:def 3;

        now

          let x be object;

          hereby

            assume x in ( rng p);

            then

            consider a be object such that

             A64: a in ( dom p) and

             A65: x = (p . a) by FUNCT_1:def 3;

            per cases by A64, FUNCT_4: 12;

              suppose

               A66: a in ( dom ((cs " ) * cS));

              then (cS . a) in ( dom (cs " )) by FUNCT_1: 11;

              then ((cs " ) . (cS . a)) in ( rng (cs " )) by FUNCT_1: 3;

              then

               A67: ((cs " ) . (cS . a)) in ( dom cs) by FUNCT_1: 33;

               not a in ( dom z) by A36, A66, XBOOLE_0:def 4;

              

              then

               A68: (p . a) = (((cs " ) * cS) . a) by FUNCT_4: 11

              .= ((cs " ) . (cS . a)) by A66, FUNCT_1: 12;

              ( dom cs) c= ( dom F) by A5, A2, A42, FINSEQ_1: 5;

              hence x in ( dom F) by A65, A68, A67;

            end;

              suppose a in ( dom z);

              then (z . a) in ( rng z) & (p . a) = (z . a) by FUNCT_1: 3, FUNCT_4: 13;

              hence x in ( dom F) by A42, A50, A65;

            end;

          end;

          assume

           A69: x in ( dom F);

          then

          reconsider j = x as Element of NAT ;

          per cases by A69, FINSEQ_1: 25;

            suppose

             A70: j in ( dom gr);

            then

             A71: (cs . j) in ( support b) by A5, A3, A9, FUNCT_1: 3;

            then

             A72: ((cS " ) . (cs . j)) in ( Seg ( card S)) by A1, A4, A11, FUNCT_1: 32;

            now

              assume ((cS " ) . (cs . j)) in ( dom z);

              then

               A73: ex k be Element of NAT st k = ((cS " ) . (cs . j)) & k in ( dom f) & (f . k) = 0 by A20;

              ((b * cS) . ((cS " ) . (cs . j))) = (b . (cS . ((cS " ) . (cs . j)))) by A4, A72, FUNCT_1: 13

              .= (b . (cs . j)) by A1, A11, A71, FUNCT_1: 35;

              hence contradiction by A71, A73, PRE_POLY:def 7;

            end;

            

            then (p . ((cS " ) . (cs . j))) = (((cs " ) * cS) . ((cS " ) . (cs . j))) by FUNCT_4: 11

            .= ((cs " ) . (cS . ((cS " ) . (cs . j)))) by A4, A72, FUNCT_1: 13

            .= ((cs " ) . (cs . j)) by A1, A11, A71, FUNCT_1: 35

            .= j by A5, A9, A70, FUNCT_1: 34;

            hence x in ( rng p) by A42, A47, A72, FUNCT_1: 3;

          end;

            suppose ex n be Nat st n in ( dom h) & j = (( len gr) + n);

            then

            consider n be Nat such that

             A74: n in ( dom h) and

             A75: j = (( len gr) + n);

            

             A76: (cdd . n) in dd by A62, A48, A63, A74, FUNCT_1: 3;

            (p . (cdd . n)) = (z . (cdd . n)) by A62, A48, A63, A20, A74, FUNCT_1: 3, FUNCT_4: 13

            .= ((cdi /. (cdd . n)) + ( card ( support b))) by A62, A48, A63, A21, A74, FUNCT_1: 3

            .= ((cdi . (cdd . n)) + ( card ( support b))) by A62, A48, A63, A22, A74, FUNCT_1: 3, PARTFUN1:def 6

            .= (n + ( card ( support b))) by A62, A48, A74, FUNCT_1: 34

            .= j by A9, A75, FINSEQ_1:def 3;

            hence x in ( rng p) by A12, A42, A18, A47, A76, FUNCT_1: 3;

          end;

        end;

        then

         A77: ( rng p) = ( dom F) by TARSKI: 2;

        then

         A78: ( dom (F * p)) = ( dom F) by A47, RELAT_1: 27;

        now

          let x be object;

          assume

           A79: x in ( dom f);

          per cases ;

            suppose

             A80: (f . x) = 0 ;

            reconsider cdix = (cdi /. x) as Element of NAT ;

            reconsider px = (p . x) as Element of NAT by ORDINAL1:def 12;

            reconsider j = x as Element of NAT by A79;

            

             A81: j in ( dom z) by A20, A79, A80;

            

            then

             A82: (p . x) = (z . x) by FUNCT_4: 13

            .= ((cdi /. x) + ( card ( support b))) by A20, A21, A81;

            

             A83: (cdi . x) in ( Seg ( card dd)) by A20, A81, FUNCT_2: 5;

            ( dom cdi) = dd by FUNCT_2:def 1;

            then

             A84: (cdi /. x) = (cdi . x) by A20, A81, PARTFUN1:def 6;

            

            thus (f . x) = (h . cdix) by A80

            .= (F . px) by A10, A19, A62, A35, A82, A84, A83, FINSEQ_1:def 7

            .= ((F * p) . x) by A12, A42, A78, A79, FUNCT_1: 12;

          end;

            suppose

             A85: (f . x) <> 0 ;

            reconsider px = (p . x) as Element of NAT by ORDINAL1:def 12;

            (f . x) = (b . (cS . x)) by A79, FUNCT_1: 12;

            then (cS . x) in ( support b) by A85, PRE_POLY:def 7;

            then

             A86: (cS . x) in ( rng cs) by FUNCT_2:def 3;

            then

             A87: ((cs " ) . (cS . x)) in ( dom cs) by FUNCT_1: 32;

            now

              assume x in dd;

              then ex j be Element of NAT st j = x & j in ( dom f) & (f . j) = 0 ;

              hence contradiction by A85;

            end;

            

            then

             A88: (p . x) = (((cs " ) * cS) . x) by A20, FUNCT_4: 11

            .= ((cs " ) . (cS . x)) by A4, A12, A79, FUNCT_1: 13;

            

            thus (f . x) = (b . (cS . x)) by A79, FUNCT_1: 12

            .= (b . (cs . px)) by A86, A88, FUNCT_1: 32

            .= (g . px) by A7, A87, A88, FUNCT_1: 13

            .= (F . px) by A5, A9, A87, A88, FINSEQ_1:def 7

            .= ((F * p) . x) by A12, A42, A78, A79, FUNCT_1: 12;

          end;

        end;

        then

         A89: f = (F * p) by A4, A11, A8, A42, A78, RELAT_1: 27;

        

         A90: p is one-to-one

        proof

          let a,c be object such that

           A91: a in ( dom p) & c in ( dom p) and

           A92: (p . a) = (p . c);

          per cases by A61, A91, XBOOLE_0:def 3;

            suppose

             A93: a in ( dom ((cs " ) * cS)) & c in ( dom ((cs " ) * cS));

            then (cS . a) in ( dom (cs " )) by FUNCT_1: 11;

            then (cS . a) in ( rng cs) by FUNCT_1: 33;

            then

             A94: (cs . ((cs " ) . (cS . a))) = (cS . a) by FUNCT_1: 35;

            a in ( dom cS) by A93, FUNCT_1: 11;

            then

             A95: ((cS " ) . (cS . a)) = a by FUNCT_1: 34;

            (cS . c) in ( dom (cs " )) by A93, FUNCT_1: 11;

            then

             A96: (cS . c) in ( rng cs) by FUNCT_1: 33;

             not c in ( dom z) by A36, A93, XBOOLE_0:def 4;

            

            then

             A97: (p . c) = (((cs " ) * cS) . c) by FUNCT_4: 11

            .= ((cs " ) . (cS . c)) by A93, FUNCT_1: 12;

            

             A98: c in ( dom cS) by A93, FUNCT_1: 11;

             not a in ( dom z) by A36, A93, XBOOLE_0:def 4;

            

            then (p . a) = (((cs " ) * cS) . a) by FUNCT_4: 11

            .= ((cs " ) . (cS . a)) by A93, FUNCT_1: 12;

            then ((cS " ) . (cS . a)) = ((cS " ) . (cS . c)) by A92, A97, A94, A96, FUNCT_1: 35;

            hence thesis by A95, A98, FUNCT_1: 34;

          end;

            suppose

             A99: a in ( dom ((cs " ) * cS)) & c in ( dom z);

            then (cS . a) in ( dom (cs " )) by FUNCT_1: 11;

            then ((cs " ) . (cS . a)) in ( rng (cs " )) by FUNCT_1: 3;

            then

             A100: ((cs " ) . (cS . a)) in ( dom cs) by FUNCT_1: 33;

             not a in ( dom z) by A36, A99, XBOOLE_0:def 4;

            

            then

             A101: (p . a) = (((cs " ) * cS) . a) by FUNCT_4: 11

            .= ((cs " ) . (cS . a)) by A99, FUNCT_1: 12;

            (p . c) = (z . c) by A99, FUNCT_4: 13

            .= ((cdi /. c) + ( card ( support b))) by A20, A21, A99;

            then ((cdi /. c) + ( card ( support b))) <= ( 0 qua Nat + ( card ( support b))) by A5, A92, A101, A100, FINSEQ_1: 1;

            then (cdi /. c) = 0 by XREAL_1: 6;

            then

             A102: (cdi . c) = 0 by A22, A20, A99, PARTFUN1:def 6;

            (cdi . c) in ( rng cdi) by A22, A20, A99, FUNCT_1: 3;

            hence thesis by A49, A102, FINSEQ_1: 1;

          end;

            suppose

             A103: a in ( dom z) & c in ( dom ((cs " ) * cS));

            then (cS . c) in ( dom (cs " )) by FUNCT_1: 11;

            then ((cs " ) . (cS . c)) in ( rng (cs " )) by FUNCT_1: 3;

            then

             A104: ((cs " ) . (cS . c)) in ( dom cs) by FUNCT_1: 33;

             not c in ( dom z) by A36, A103, XBOOLE_0:def 4;

            

            then

             A105: (p . c) = (((cs " ) * cS) . c) by FUNCT_4: 11

            .= ((cs " ) . (cS . c)) by A103, FUNCT_1: 12;

            (p . a) = (z . a) by A103, FUNCT_4: 13

            .= ((cdi /. a) + ( card ( support b))) by A20, A21, A103;

            then ((cdi /. a) + ( card ( support b))) <= ( 0 qua Nat + ( card ( support b))) by A5, A92, A105, A104, FINSEQ_1: 1;

            then (cdi /. a) = 0 by XREAL_1: 6;

            then

             A106: (cdi . a) = 0 by A22, A20, A103, PARTFUN1:def 6;

            (cdi . a) in ( rng cdi) by A22, A20, A103, FUNCT_1: 3;

            hence thesis by A49, A106, FINSEQ_1: 1;

          end;

            suppose

             A107: a in ( dom z) & c in ( dom z);

            then

             A108: (cdi /. a) = (cdi . a) & (cdi /. c) = (cdi . c) by A22, A20, PARTFUN1:def 6;

            

             A109: (p . c) = (z . c) by A107, FUNCT_4: 13

            .= ((cdi /. c) + ( card ( support b))) by A20, A21, A107;

            (p . a) = (z . a) by A107, FUNCT_4: 13

            .= ((cdi /. a) + ( card ( support b))) by A20, A21, A107;

            hence thesis by A22, A20, A92, A107, A109, A108, FUNCT_1:def 4;

          end;

        end;

        ( Sum h) = 0 by RVSUM_1: 81;

        

        then

         A110: ( Sum gr) = (( Sum gr) + ( Sum h))

        .= ( Sum F) by RVSUM_1: 75;

        p is onto by A77, FUNCT_2:def 3;

        hence thesis by A6, A90, A89, A110, FINSOP_1: 7;

      end;

        suppose ( card ( support b)) = ( card S);

        hence thesis by A1, A6, A7, CARD_2: 102;

      end;

    end;

    theorem :: UPROOTS:15

    

     Th12: for A be set, b,b1,b2 be Rbag of A st b = (b1 + b2) holds ( Sum b) = (( Sum b1) + ( Sum b2))

    proof

      let A be set, b,b1,b2 be Rbag of A;

      set S = ( support b);

      set SS = (( support b1) \/ ( support b2));

      

       A1: ( dom b2) = A by PARTFUN1:def 2;

      then

       A2: ( support b2) c= A by PRE_POLY: 37;

      

       A3: ( dom b1) = A by PARTFUN1:def 2;

      then ( support b1) c= A by PRE_POLY: 37;

      then

      reconsider SS as finite Subset of A by A2, XBOOLE_1: 8;

      set cS = ( canFS SS);

      consider f1r be FinSequence of REAL such that

       A4: f1r = (b1 * ( canFS SS)) and

       A5: ( Sum b1) = ( Sum f1r) by Th11, XBOOLE_1: 7;

      

       A6: ( rng cS) = SS by FUNCT_2:def 3;

      then

       A7: ( dom f1r) = ( dom cS) by A3, A4, RELAT_1: 27;

      assume

       A8: b = (b1 + b2);

      then S c= SS by PRE_POLY: 75;

      then

      consider f be FinSequence of REAL such that

       A9: f = (b * ( canFS SS)) and

       A10: ( Sum b) = ( Sum f) by Th11;

      ( dom b) = A by PARTFUN1:def 2;

      then

       A11: ( dom f) = ( dom cS) by A9, A6, RELAT_1: 27;

      then

       A12: ( len f1r) = ( len f) by A7, FINSEQ_3: 29;

      consider f2r be FinSequence of REAL such that

       A13: f2r = (b2 * ( canFS SS)) and

       A14: ( Sum b2) = ( Sum f2r) by Th11, XBOOLE_1: 7;

      

       A15: ( dom f2r) = ( dom cS) by A1, A13, A6, RELAT_1: 27;

       A16:

      now

        let k be Element of NAT such that

         A17: k in ( dom f1r);

        

         A18: (f1r /. k) = (f1r . k) by A17, PARTFUN1:def 6

        .= (b1 . (cS . k)) by A4, A17, FUNCT_1: 12;

        

         A19: (f . k) = (b . (cS . k)) by A9, A11, A7, A17, FUNCT_1: 12;

        (f2r /. k) = (f2r . k) by A7, A15, A17, PARTFUN1:def 6

        .= (b2 . (cS . k)) by A13, A7, A15, A17, FUNCT_1: 12;

        hence (f . k) = ((f1r /. k) + (f2r /. k)) by A8, A18, A19, PRE_POLY:def 5;

      end;

      ( len f1r) = ( len f2r) by A7, A15, FINSEQ_3: 29;

      hence thesis by A10, A5, A14, A12, A16, INTEGRA1: 21;

    end;

    theorem :: UPROOTS:16

    

     Th13: for L be associative commutative unital non empty multMagma, f,g be FinSequence of L, p be Permutation of ( dom f) st g = (f * p) holds ( Product g) = ( Product f)

    proof

      let L be associative commutative unital non empty multMagma, f,g be FinSequence of L, p be Permutation of ( dom f) such that

       A1: g = (f * p);

      set mL = the multF of L;

      mL is commutative & mL is associative by MONOID_0:def 11;

      hence thesis by A1, FINSOP_1: 7;

    end;

    begin

    definition

      let L be non empty ZeroStr, p be Polynomial of L;

      :: UPROOTS:def5

      attr p is non-zero means

      : Def4: p <> ( 0_. L);

    end

    theorem :: UPROOTS:17

    

     Th14: for L be non empty ZeroStr, p be Polynomial of L holds p is non-zero iff ( len p) > 0

    proof

      let L be non empty ZeroStr, p be Polynomial of L;

      hereby

        assume p is non-zero;

        then p <> ( 0_. L);

        then ( len p) <> 0 by POLYNOM4: 5;

        hence ( len p) > 0 ;

      end;

      assume ( len p) > 0 ;

      then p <> ( 0_. L) by POLYNOM4: 3;

      hence thesis;

    end;

    registration

      let L be non trivial ZeroStr;

      cluster non-zero for Polynomial of L;

      existence

      proof

        set a = the Element of ( NonZero L);

        reconsider a as Element of L;

        take p = <%a%>;

        

         A1: ( not a in {( 0. L)}) & (( 0_. L) . 0 ) = ( 0. L) by FUNCOP_1: 7, XBOOLE_0:def 5;

        (p . 0 ) = a by POLYNOM5: 32;

        then p <> ( 0_. L) by A1, TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      let L be non degenerated non empty multLoopStr_0, x be Element of L;

      cluster <%x, ( 1. L)%> -> non-zero;

      correctness

      proof

        ( len <%x, ( 1. L)%>) = 2 by POLYNOM5: 40;

        hence thesis by Th14;

      end;

    end

    theorem :: UPROOTS:18

    

     Th15: for L be non empty ZeroStr, p be Polynomial of L st ( len p) > 0 holds (p . (( len p) -' 1)) <> ( 0. L)

    proof

      let L be non empty ZeroStr, p be Polynomial of L;

      assume ( len p) > 0 ;

      then ex k be Nat st ( len p) = (k + 1) by NAT_1: 6;

      then ( len p) = ((( len p) -' 1) + 1) by NAT_D: 34;

      hence thesis by ALGSEQ_1: 10;

    end;

    theorem :: UPROOTS:19

    

     Th16: for L be non empty ZeroStr, p be AlgSequence of L st ( len p) = 1 holds p = <%(p . 0 )%> & (p . 0 ) <> ( 0. L)

    proof

      let L be non empty ZeroStr, p be AlgSequence of L such that

       A1: ( len p) = 1;

      thus p = <%(p . 0 )%> by A1, ALGSEQ_1:def 5;

      hence thesis by A1, ALGSEQ_1: 14;

    end;

    theorem :: UPROOTS:20

    

     Th17: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L holds (p *' ( 0_. L)) = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, p be Polynomial of L;

      now

        let i be Element of NAT ;

        consider r be FinSequence of L such that ( len r) = (i + 1) and

         A1: ((p *' ( 0_. L)) . i) = ( Sum r) and

         A2: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (( 0_. L) . ((i + 1) -' k))) by POLYNOM3:def 9;

        now

          let k be Element of NAT ;

          assume k in ( dom r);

          

          hence (r . k) = ((p . (k -' 1)) * (( 0_. L) . ((i + 1) -' k))) by A2

          .= ((p . (k -' 1)) * ( 0. L)) by FUNCOP_1: 7

          .= ( 0. L);

        end;

        

        hence ((p *' ( 0_. L)) . i) = ( 0. L) by A1, POLYNOM3: 1

        .= (( 0_. L) . i) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      cluster algebraic-closed add-associative right_zeroed right_complementable Abelian commutative associative distributive domRing-like non degenerated for unital non empty doubleLoopStr;

      existence

      proof

        take F_Complex ;

        thus thesis;

      end;

    end

    theorem :: UPROOTS:21

    

     Th18: for L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p,q be Polynomial of L st (p *' q) = ( 0_. L) holds p = ( 0_. L) or q = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p,q be Polynomial of L such that

       A1: (p *' q) = ( 0_. L) and

       A2: p <> ( 0_. L) and

       A3: q <> ( 0_. L);

      consider lp1 be Nat such that

       A4: ( len p) = (lp1 + 1) by A2, NAT_1: 6, POLYNOM4: 5;

      ( len p) <> 0 by A2, POLYNOM4: 5;

      then

       A5: ( 0 qua Nat + 1) <= ( len p) by NAT_1: 13;

      consider lq1 be Nat such that

       A6: ( len q) = (lq1 + 1) by A3, NAT_1: 6, POLYNOM4: 5;

      reconsider lp1, lq1 as Element of NAT by ORDINAL1:def 12;

      

       A7: (p . lp1) <> ( 0. L) by A4, ALGSEQ_1: 10;

      

       A8: (q . lq1) <> ( 0. L) by A6, ALGSEQ_1: 10;

      set lpq = (lp1 + lq1);

      consider r be FinSequence of L such that

       A9: ( len r) = (lpq + 1) and

       A10: ((p *' q) . lpq) = ( Sum r) and

       A11: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((lpq + 1) -' k))) by POLYNOM3:def 9;

      

       A12: ((lpq + 1) -' ( len p)) = ((lq1 + (lp1 + 1)) -' ( len p))

      .= lq1 by A4, NAT_D: 34;

      ( len p) <= ((lp1 + 1) + lq1) by A4, NAT_1: 12;

      then

       A13: ( len p) in ( dom r) by A9, A5, FINSEQ_3: 25;

      now

        let k be Nat such that

         A14: k in ( dom r) and

         A15: k <> ( len p);

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        

         A16: (r . k1) = ((p . (k1 -' 1)) * (q . ((lpq + 1) -' k1))) by A11, A14;

        per cases by A15, XXREAL_0: 1;

          suppose k < ( len p);

          then

          consider d be Element of NAT such that

           A17: ( len p) = (k1 + d) and

           A18: 1 <= d by FINSEQ_4: 84;

          

           A19: ( len q) <= (lq1 + d) by A6, A18, XREAL_1: 6;

          ((lpq + 1) -' k) = (((lq1 + d) + k) -' k) by A4, A17

          .= (lq1 + d) by NAT_D: 34;

          

          hence (r . k) = ((p . (k -' 1)) * ( 0. L)) by A16, A19, ALGSEQ_1: 8

          .= ( 0. L);

        end;

          suppose k > ( len p);

          then k >= (( len p) + 1) by NAT_1: 13;

          then (k -' 1) >= ((( len p) + 1) -' 1) by NAT_D: 42;

          then (k -' 1) >= ( len p) by NAT_D: 34;

          

          hence (r . k) = (( 0. L) * (q . ((lpq + 1) -' k))) by A16, ALGSEQ_1: 8

          .= ( 0. L);

        end;

      end;

      

      then ( Sum r) = (r . ( len p)) by A13, MATRIX_3: 12

      .= ((p . (( len p) -' 1)) * (q . ((lpq + 1) -' ( len p)))) by A11, A13

      .= ((p . lp1) * (q . lq1)) by A4, A12, NAT_D: 34;

      then ( Sum r) <> ( 0. L) by A7, A8, VECTSP_2:def 1;

      hence contradiction by A1, A10, FUNCOP_1: 7;

    end;

    registration

      let L be add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr;

      cluster ( Polynom-Ring L) -> domRing-like;

      correctness

      proof

        set PRL = ( Polynom-Ring L);

        let x,y be Element of PRL;

        reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def 10;

        

         A1: ( 0_. L) = ( 0. PRL) by POLYNOM3:def 10;

        assume (x * y) = ( 0. PRL);

        then (xp *' yp) = ( 0_. L) by A1, POLYNOM3:def 10;

        hence thesis by A1, Th18;

      end;

    end

    registration

      let L be domRing, p,q be non-zero Polynomial of L;

      cluster (p *' q) -> non-zero;

      correctness by Th18;

    end

    theorem :: UPROOTS:22

    for L be non degenerated comRing, p,q be Polynomial of L holds (( Roots p) \/ ( Roots q)) c= ( Roots (p *' q))

    proof

      let L be non degenerated comRing, p,q be Polynomial of L;

      let x be object;

      assume

       A1: x in (( Roots p) \/ ( Roots q));

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: x in ( Roots p);

        then

        reconsider a = x as Element of L;

        a is_a_root_of p by A2, POLYNOM5:def 10;

        then ( eval (p,a)) = ( 0. L);

        then (( eval (p,a)) * ( eval (q,a))) = ( 0. L);

        then ( eval ((p *' q),a)) = ( 0. L) by POLYNOM4: 24;

        then a is_a_root_of (p *' q);

        hence thesis by POLYNOM5:def 10;

      end;

        suppose

         A3: x in ( Roots q);

        then

        reconsider a = x as Element of L;

        a is_a_root_of q by A3, POLYNOM5:def 10;

        then ( eval (q,a)) = ( 0. L);

        then (( eval (p,a)) * ( eval (q,a))) = ( 0. L);

        then ( eval ((p *' q),a)) = ( 0. L) by POLYNOM4: 24;

        then a is_a_root_of (p *' q);

        hence thesis by POLYNOM5:def 10;

      end;

    end;

    theorem :: UPROOTS:23

    

     Th20: for L be domRing, p,q be Polynomial of L holds ( Roots (p *' q)) = (( Roots p) \/ ( Roots q))

    proof

      let L be domRing, p,q be Polynomial of L;

      now

        let x be object;

        hereby

          assume

           A1: x in ( Roots (p *' q));

          then

          reconsider a = x as Element of L;

          a is_a_root_of (p *' q) by A1, POLYNOM5:def 10;

          then ( eval ((p *' q),a)) = ( 0. L);

          then

           A2: (( eval (p,a)) * ( eval (q,a))) = ( 0. L) by POLYNOM4: 24;

          per cases by A2, VECTSP_2:def 1;

            suppose ( eval (p,a)) = ( 0. L);

            then a is_a_root_of p;

            then a in ( Roots p) by POLYNOM5:def 10;

            hence x in (( Roots p) \/ ( Roots q)) by XBOOLE_0:def 3;

          end;

            suppose ( eval (q,a)) = ( 0. L);

            then a is_a_root_of q;

            then a in ( Roots q) by POLYNOM5:def 10;

            hence x in (( Roots p) \/ ( Roots q)) by XBOOLE_0:def 3;

          end;

        end;

        assume

         A3: x in (( Roots p) \/ ( Roots q));

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: x in ( Roots p);

          then

          reconsider a = x as Element of L;

          a is_a_root_of p by A4, POLYNOM5:def 10;

          then ( eval (p,a)) = ( 0. L);

          then (( eval (p,a)) * ( eval (q,a))) = ( 0. L);

          then ( eval ((p *' q),a)) = ( 0. L) by POLYNOM4: 24;

          then a is_a_root_of (p *' q);

          hence x in ( Roots (p *' q)) by POLYNOM5:def 10;

        end;

          suppose

           A5: x in ( Roots q);

          then

          reconsider a = x as Element of L;

          a is_a_root_of q by A5, POLYNOM5:def 10;

          then ( eval (q,a)) = ( 0. L);

          then (( eval (p,a)) * ( eval (q,a))) = ( 0. L);

          then ( eval ((p *' q),a)) = ( 0. L) by POLYNOM4: 24;

          then a is_a_root_of (p *' q);

          hence x in ( Roots (p *' q)) by POLYNOM5:def 10;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: UPROOTS:24

    

     Th21: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Polynomial of L, pc be Element of ( Polynom-Ring L) st p = pc holds ( - p) = ( - pc)

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Polynomial of L, pc be Element of ( Polynom-Ring L) such that

       A1: p = pc;

      set PRL = ( Polynom-Ring L);

      reconsider mpc = ( - p) as Element of PRL by POLYNOM3:def 10;

      (p + ( - p)) = (p - p)

      .= ( 0_. L) by POLYNOM3: 29;

      

      then (pc + mpc) = ( 0_. L) by A1, POLYNOM3:def 10

      .= ( 0. PRL) by POLYNOM3:def 10;

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: UPROOTS:25

    

     Th22: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L, pc,qc be Element of ( Polynom-Ring L) st p = pc & q = qc holds (p - q) = (pc - qc)

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L, pc,qc be Element of ( Polynom-Ring L) such that

       A1: p = pc and

       A2: q = qc;

      ( - q) = ( - qc) by A2, Th21;

      hence thesis by A1, POLYNOM3:def 10;

    end;

    theorem :: UPROOTS:26

    

     Th23: for L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q,r be Polynomial of L holds ((p *' q) - (p *' r)) = (p *' (q - r))

    proof

      let L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q,r be Polynomial of L;

      set PRL = ( Polynom-Ring L);

      reconsider pc = p, qc = q, rc = r as Element of PRL by POLYNOM3:def 10;

      

       A1: (qc - rc) = (q - r) by Th22;

      (p *' q) = (pc * qc) & (p *' r) = (pc * rc) by POLYNOM3:def 10;

      

      hence ((p *' q) - (p *' r)) = ((pc * qc) - (pc * rc)) by Th22

      .= (pc * (qc - rc)) by VECTSP_1: 11

      .= (p *' (q - r)) by A1, POLYNOM3:def 10;

    end;

    theorem :: UPROOTS:27

    

     Th24: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L st (p - q) = ( 0_. L) holds p = q

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, q,r be Polynomial of L;

      set PRL = ( Polynom-Ring L);

      reconsider qc = q, rc = r as Element of PRL by POLYNOM3:def 10;

      assume

       A1: (q - r) = ( 0_. L);

      ( 0_. L) = ( 0. PRL) by POLYNOM3:def 10;

      then (qc - rc) = ( 0. PRL) by A1, Th22;

      hence thesis by VECTSP_1: 27;

    end;

    theorem :: UPROOTS:28

    

     Th25: for L be Abelian add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p,q,r be Polynomial of L st p <> ( 0_. L) & (p *' q) = (p *' r) holds q = r

    proof

      let L be Abelian add-associative right_zeroed right_complementable distributive domRing-like non empty doubleLoopStr, p,q,r be Polynomial of L;

      assume

       A1: p <> ( 0_. L);

      assume (p *' q) = (p *' r);

      then ((p *' q) - (p *' r)) = ( 0_. L) by POLYNOM3: 29;

      then (p *' (q - r)) = ( 0_. L) by Th23;

      then (q - r) = ( 0_. L) by A1, Th18;

      hence thesis by Th24;

    end;

    theorem :: UPROOTS:29

    

     Th26: for L be domRing, n be Element of NAT , p be Polynomial of L st p <> ( 0_. L) holds (p `^ n) <> ( 0_. L)

    proof

      let L be domRing, n be Element of NAT , p be Polynomial of L;

      defpred P[ Nat] means (p `^ $1) <> ( 0_. L);

      assume

       A1: p <> ( 0_. L);

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A3: P[n];

        (p `^ (n + 1)) = ((p `^ n) *' p) by POLYNOM5: 19;

        hence thesis by A1, A3, Th18;

      end;

      (( 1_. L) . 0 ) = ( 1. L) & (( 0_. L) . 0 ) = ( 0. L) by FUNCOP_1: 7, POLYNOM3: 30;

      then

       A4: P[ 0 ] by POLYNOM5: 15;

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: UPROOTS:30

    

     Th27: for L be comRing, i,j be Nat, p be Polynomial of L holds ((p `^ i) *' (p `^ j)) = (p `^ (i + j))

    proof

      let L be comRing, i,j be Nat, p be Polynomial of L;

      defpred P[ Nat] means ((p `^ i) *' (p `^ $1)) = (p `^ (i + $1));

      

       A1: for j be Nat st P[j] holds P[(j + 1)]

      proof

        let j be Nat such that

         A2: P[j];

        ((p `^ i) *' (p `^ (j + 1))) = ((p `^ i) *' ((p `^ j) *' p)) by POLYNOM5: 19

        .= ((p `^ (i + j)) *' p) by A2, POLYNOM3: 33

        .= (p `^ ((i + j) + 1)) by POLYNOM5: 19

        .= (p `^ (i + (j + 1)));

        hence thesis;

      end;

      ((p `^ i) *' (p `^ 0 )) = ((p `^ i) *' ( 1_. L)) by POLYNOM5: 15

      .= (p `^ (i + 0 qua Nat)) by POLYNOM3: 35;

      then

       A3: P[ 0 ];

      for j be Nat holds P[j] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: UPROOTS:31

    

     Th28: for L be non empty multLoopStr_0 holds ( 1_. L) = <%( 1. L)%>

    proof

      let L be non empty multLoopStr_0;

      

       A1: ( dom ( 0_. L)) = NAT by FUNCT_2:def 1;

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider n = x as Element of NAT ;

        per cases ;

          suppose

           A2: x = 0 ;

          

          hence (( 1_. L) . x) = ( 1. L) by A1, FUNCT_7: 31

          .= ( <%( 1. L)%> . x) by A2, ALGSEQ_1:def 5;

        end;

          suppose

           A3: n <> 0 ;

          then

           A4: n = 1 or n > 1 by NAT_1: 53;

          

          thus (( 1_. L) . x) = (( 0_. L) . n) by A3, FUNCT_7: 32

          .= ( 0. L) by FUNCOP_1: 7

          .= ( <%( 1. L)%> . x) by A4, POLYNOM5: 32;

        end;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: UPROOTS:32

    for L be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, p be Polynomial of L holds (p *' <%( 1. L)%>) = p

    proof

      let L be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, p be Polynomial of L;

      

      thus (p *' <%( 1. L)%>) = (p *' ( 1_. L)) by Th28

      .= p by POLYNOM3: 35;

    end;

    theorem :: UPROOTS:33

    

     Th30: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L st ( len p) = 0 or ( len q) = 0 holds ( len (p *' q)) = 0

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L;

      assume

       A1: ( len p) = 0 or ( len q) = 0 ;

      per cases by A1;

        suppose ( len p) = 0 ;

        then p = ( 0_. L) by POLYNOM4: 5;

        then (p *' q) = ( 0_. L) by POLYNOM4: 2;

        hence thesis by POLYNOM4: 3;

      end;

        suppose ( len q) = 0 ;

        then q = ( 0_. L) by POLYNOM4: 5;

        then (p *' q) = ( 0_. L) by Th17;

        hence thesis by POLYNOM4: 3;

      end;

    end;

    theorem :: UPROOTS:34

    

     Th31: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L st (p *' q) is non-zero holds p is non-zero & q is non-zero

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p,q be Polynomial of L;

      assume that

       A1: (p *' q) is non-zero and

       A2: p is non non-zero or q is non non-zero;

      ( len p) = 0 or ( len q) = 0 by A2, Th14;

      then ( len (p *' q)) = 0 by Th30;

      hence thesis by A1, Th14;

    end;

    theorem :: UPROOTS:35

    for L be add-associative right_zeroed right_complementable distributive commutative associative well-unital non empty doubleLoopStr, p,q be Polynomial of L st ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) holds 0 < ( len (p *' q))

    proof

      let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital non empty doubleLoopStr, p,q be Polynomial of L;

      assume

       A1: ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L);

      now

        assume ( len q) <= 0 ;

        then ( len q) = 0 ;

        then q = ( 0_. L) by POLYNOM4: 5;

        then (q . (( len q) -' 1)) = ( 0. L) by FUNCOP_1: 7;

        hence contradiction by A1;

      end;

      then

       A2: ( 0 qua Nat + 1) <= ( len q) by NAT_1: 13;

      now

        assume ( len p) <= 0 ;

        then ( len p) = 0 ;

        then p = ( 0_. L) by POLYNOM4: 5;

        then (p . (( len p) -' 1)) = ( 0. L) by FUNCOP_1: 7;

        hence contradiction by A1;

      end;

      then ( 0 qua Nat + 1) <= ( len p) by NAT_1: 13;

      then (( len p) + ( len q)) >= (1 + 1) by A2, XREAL_1: 7;

      then ((( len p) + ( len q)) - 1) >= ((1 + 1) - 1) by XREAL_1: 9;

      hence thesis by A1, POLYNOM4: 10;

    end;

    theorem :: UPROOTS:36

    

     Th33: for L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p,q be Polynomial of L st 1 < ( len p) & 1 < ( len q) holds ( len p) < ( len (p *' q))

    proof

      let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr, p,q be Polynomial of L such that

       A1: 1 < ( len p) and

       A2: 1 < ( len q);

      (p . (( len p) -' 1)) <> ( 0. L) & (q . (( len q) -' 1)) <> ( 0. L) by A1, A2, Th15;

      then ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) by VECTSP_2:def 1;

      then

       A3: ( len (p *' q)) = ((( len p) + ( len q)) - 1) by POLYNOM4: 10;

      (( len q) - 1) > (1 - 1) by A2, XREAL_1: 14;

      then (( len p) + (( len q) - 1)) > ( 0 qua Nat + ( len p)) by XREAL_1: 8;

      hence thesis by A3;

    end;

    theorem :: UPROOTS:37

    

     Th34: for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, a,b be Element of L, p be Polynomial of L holds (( <%a, b%> *' p) . 0 ) = (a * (p . 0 )) & for i be Nat holds (( <%a, b%> *' p) . (i + 1)) = ((a * (p . (i + 1))) + (b * (p . i)))

    proof

      let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr, a,b be Element of L, q be Polynomial of L;

      set p = <%a, b%>;

      consider r be FinSequence of L such that

       A1: ( len r) = ( 0 qua Nat + 1) and

       A2: ((p *' q) . 0 ) = ( Sum r) and

       A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . (( 0 qua Nat + 1) -' k))) by POLYNOM3:def 9;

      

       A4: 1 in ( dom r) by A1, FINSEQ_3: 25;

      then

      reconsider r1 = (r . 1) as Element of L by FINSEQ_2: 11;

      r = <*r1*> by A1, FINSEQ_1: 40;

      

      then ( Sum r) = r1 by RLVECT_1: 44

      .= ((p . (1 -' 1)) * (q . (( 0 qua Nat + 1) -' 1))) by A3, A4

      .= ((p . 0 ) * (q . (( 0 qua Nat + 1) -' 1))) by XREAL_1: 232

      .= ((p . 0 ) * (q . 0 )) by NAT_D: 34;

      hence (( <%a, b%> *' q) . 0 ) = (a * (q . 0 )) by A2, POLYNOM5: 38;

      let i be Nat;

      consider r be FinSequence of L such that

       A5: ( len r) = ((i + 1) + 1) and

       A6: ((p *' q) . (i + 1)) = ( Sum r) and

       A7: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . (((i + 1) + 1) -' k))) by POLYNOM3:def 9;

      ( len r) = (i + 2) by A5;

      then

       A8: ( 0 qua Nat + 2) <= ( len r) by XREAL_1: 6;

      then

       A9: 2 in ( dom r) by FINSEQ_3: 25;

      

      then

       A10: (r /. 2) = (r . 2) by PARTFUN1:def 6

      .= ((p . ((1 + 1) -' 1)) * (q . (((i + 1) + 1) -' 2))) by A7, A9

      .= ((p . 1) * (q . (((i + 1) + 1) -' 2))) by NAT_D: 34

      .= (b * (q . ((i + (1 + 1)) -' 2))) by POLYNOM5: 38

      .= (b * (q . i)) by NAT_D: 34;

       A11:

      now

        let k be Element of NAT such that

         A12: 2 < k and

         A13: k in ( dom r);

        consider k1 be Nat such that

         A14: k = (k1 + 1) by A12, NAT_1: 6;

        

         A15: 2 <= k1 by A12, A14, NAT_1: 13;

        reconsider k1 as Element of NAT by ORDINAL1:def 12;

        

        thus (r . k) = ((p . (k -' 1)) * (q . (((i + 1) + 1) -' k))) by A7, A13

        .= ((p . k1) * (q . (((i + 1) + 1) -' k))) by A14, NAT_D: 34

        .= (( 0. L) * (q . (((i + 1) + 1) -' k))) by A15, POLYNOM5: 38

        .= ( 0. L);

      end;

      1 <= ( len r) by A8, XXREAL_0: 2;

      then

       A16: 1 in ( dom r) by FINSEQ_3: 25;

      

      then (r /. 1) = (r . 1) by PARTFUN1:def 6

      .= ((p . (1 -' 1)) * (q . (((i + 1) + 1) -' 1))) by A7, A16

      .= ((p . 0 ) * (q . (((i + 1) + 1) -' 1))) by XREAL_1: 232

      .= ((p . 0 ) * (q . (i + 1))) by NAT_D: 34

      .= (a * (q . (i + 1))) by POLYNOM5: 38;

      hence thesis by A6, A8, A10, A11, Th2;

    end;

    theorem :: UPROOTS:38

    

     Th35: for L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r be Element of L, q be non-zero Polynomial of L holds ( len ( <%r, ( 1. L)%> *' q)) = (( len q) + 1)

    proof

      let L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r be Element of L, q be non-zero Polynomial of L;

      set p = <%r, ( 1. L)%>;

      

       A1: ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) = ((p . ((1 + 1) -' 1)) * (q . (( len q) -' 1))) by POLYNOM5: 40

      .= ((p . 1) * (q . (( len q) -' 1))) by NAT_D: 34

      .= (( 1. L) * (q . (( len q) -' 1))) by POLYNOM5: 38

      .= (q . (( len q) -' 1));

      ( len <%r, ( 1. L)%>) = 2 & ( len q) > 0 by Th14, POLYNOM5: 40;

      

      hence ( len ( <%r, ( 1. L)%> *' q)) = ((( len q) + (1 + 1)) - 1) by A1, Th15, POLYNOM4: 10

      .= (( len q) + 1);

    end;

    theorem :: UPROOTS:39

    

     Th36: for L be non degenerated comRing, x be Element of L, i be Nat holds ( len ( <%x, ( 1. L)%> `^ i)) = (i + 1)

    proof

      let L be non degenerated comRing, x be Element of L;

      defpred P[ Nat] means ( len ( <%x, ( 1. L)%> `^ $1)) = ($1 + 1);

      set r = <%x, ( 1. L)%>;

      

       A1: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A2: P[i];

        reconsider ri = (r `^ i) as non-zero Polynomial of L by A2, Th14;

        

        thus ( len (r `^ (i + 1))) = ( len ((r `^ 1) *' ri)) by Th27

        .= ( len (r *' ri)) by POLYNOM5: 16

        .= ((i + 1) + 1) by A2, Th35;

      end;

      (r `^ 0 ) = ( 1_. L) by POLYNOM5: 15;

      then

       A3: P[ 0 ] by POLYNOM4: 4;

      thus for i be Nat holds P[i] from NAT_1:sch 2( A3, A1);

    end;

    registration

      let L be non degenerated comRing, x be Element of L, n be Nat;

      cluster ( <%x, ( 1. L)%> `^ n) -> non-zero;

      correctness

      proof

        ( len ( <%x, ( 1. L)%> `^ n)) = (n + 1) by Th36;

        hence thesis by Th14;

      end;

    end

    theorem :: UPROOTS:40

    

     Th37: for L be non degenerated comRing, x be Element of L, q be non-zero Polynomial of L, i be Nat holds ( len (( <%x, ( 1. L)%> `^ i) *' q)) = (i + ( len q))

    proof

      let L be non degenerated comRing, x be Element of L, q be non-zero Polynomial of L;

      set r = <%x, ( 1. L)%>;

      defpred P[ Nat] means ( len ((r `^ $1) *' q)) = ($1 + ( len q));

      

       A1: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A2: P[i];

        ( len q) > 0 by Th14;

        then

         A3: ((r `^ i) *' q) is non-zero by A2, Th14;

        

        thus ( len ((r `^ (i + 1)) *' q)) = ( len (((r `^ 1) *' (r `^ i)) *' q)) by Th27

        .= ( len ((r *' (r `^ i)) *' q)) by POLYNOM5: 16

        .= ( len (r *' ((r `^ i) *' q))) by POLYNOM3: 33

        .= ((i + ( len q)) + 1) by A2, A3, Th35

        .= ((i + 1) + ( len q));

      end;

      ( len ((r `^ 0 ) *' q)) = ( len (( 1_. L) *' q)) by POLYNOM5: 15

      .= ( 0 qua Nat + ( len q)) by POLYNOM3: 35;

      then

       A4: P[ 0 ];

      thus for i be Nat holds P[i] from NAT_1:sch 2( A4, A1);

    end;

    theorem :: UPROOTS:41

    

     Th38: for L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, r be Element of L, p,q be Polynomial of L st p = ( <%r, ( 1. L)%> *' q) & (p . (( len p) -' 1)) = ( 1. L) holds (q . (( len q) -' 1)) = ( 1. L)

    proof

      let L be add-associative right_zeroed right_complementable distributive well-unital commutative associative non degenerated non empty doubleLoopStr, x be Element of L, p,q be Polynomial of L such that

       A1: p = ( <%x, ( 1. L)%> *' q) and

       A2: (p . (( len p) -' 1)) = ( 1. L);

      set lp1 = (( len p) -' 1);

       A3:

      now

        assume q = ( 0_. L);

        then p = ( 0_. L) by A1, POLYNOM3: 34;

        hence contradiction by A2, FUNCOP_1: 7;

      end;

      then q is non-zero;

      then ( len p) = (( len q) + 1) by A1, Th35;

      then

       A4: lp1 = ( len q) by NAT_D: 34;

      then

      consider lp2 be Nat such that

       A5: lp1 = (lp2 + 1) by A3, NAT_1: 6, POLYNOM4: 5;

      reconsider lp2 as Element of NAT by ORDINAL1:def 12;

      

       A6: (q . lp1) = ( 0. L) by A4, ALGSEQ_1: 8;

      (( <%x, ( 1. L)%> *' q) . lp1) = ((x * (q . lp1)) + (( 1. L) * (q . lp2))) by A5, Th34

      .= (( 0. L) + (( 1. L) * (q . lp2))) by A6

      .= (( 1. L) * (q . lp2)) by RLVECT_1: 4

      .= (q . lp2);

      hence thesis by A1, A2, A4, A5, NAT_D: 34;

    end;

    begin

    definition

      let L be non empty ZeroStr, p be Polynomial of L;

      let n be Nat;

      :: UPROOTS:def6

      func poly_shift (p,n) -> Polynomial of L means

      : Def5: for i be Nat holds (it . i) = (p . (n + i));

      existence

      proof

        deffunc F( Nat) = (p . (n + $1));

        consider ps be AlgSequence of L such that

         A1: ( len ps) <= ( len p) and

         A2: for k be Nat st k < ( len p) holds (ps . k) = F(k) from ALGSEQ_1:sch 1;

        take ps;

        let i be Nat;

        per cases ;

          suppose i < ( len p);

          hence thesis by A2;

        end;

          suppose

           A3: i >= ( len p);

          

          hence (ps . i) = ( 0. L) by A1, ALGSEQ_1: 8, XXREAL_0: 2

          .= (p . (n + i)) by A3, ALGSEQ_1: 8, NAT_1: 12;

        end;

      end;

      uniqueness

      proof

        let it1,it2 be Polynomial of L such that

         A4: for i be Nat holds (it1 . i) = (p . (n + i)) and

         A5: for i be Nat holds (it2 . i) = (p . (n + i));

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Element of NAT ;

          

          thus (it1 . x) = (p . (n + i)) by A4

          .= (it2 . x) by A5;

        end;

        hence it1 = it2 by FUNCT_2: 12;

      end;

    end

    theorem :: UPROOTS:42

    

     Th39: for L be non empty ZeroStr, p be Polynomial of L holds ( poly_shift (p, 0 )) = p

    proof

      let L be non empty ZeroStr, p be Polynomial of L;

      set ps = ( poly_shift (p, 0 ));

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        

        thus (ps . x) = (p . ( 0 qua Nat + i)) by Def5

        .= (p . x);

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: UPROOTS:43

    

     Th40: for L be non empty ZeroStr, n be Element of NAT , p be Polynomial of L st n >= ( len p) holds ( poly_shift (p,n)) = ( 0_. L)

    proof

      let L be non empty ZeroStr, n be Element of NAT , p be Polynomial of L;

      set ps = ( poly_shift (p,n));

      assume

       A1: n >= ( len p);

       A2:

      now

        let z be object;

        assume z in ( dom ps);

        then

        reconsider i = z as Element of NAT ;

        

        thus (ps . z) = (p . (n + i)) by Def5

        .= ( 0. L) by A1, ALGSEQ_1: 8, NAT_1: 12;

      end;

      ( dom ps) = NAT by FUNCT_2:def 1;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    theorem :: UPROOTS:44

    

     Th41: for L be non degenerated non empty multLoopStr_0, n be Element of NAT , p be Polynomial of L st n <= ( len p) holds (( len ( poly_shift (p,n))) + n) = ( len p)

    proof

      let L be non degenerated non empty multLoopStr_0, n be Element of NAT , p be Polynomial of L such that

       A1: n <= ( len p);

      set ps = ( poly_shift (p,n)), lpn = (( len p) - n);

      (n - n) <= lpn by A1, XREAL_1: 9;

      then

      reconsider lpn as Element of NAT by INT_1: 3;

       A2:

      now

        let m be Nat such that

         A3: m is_at_least_length_of ps and

         A4: lpn > m;

        lpn >= (m + 1) by A4, NAT_1: 13;

        then

         A5: (lpn - 1) >= ((m + 1) - 1) by XREAL_1: 9;

        then

        reconsider lpn1 = (lpn - 1) as Element of NAT by INT_1: 3;

        ((n + lpn1) + 1) = ( len p);

        then

         A6: (p . (n + lpn1)) <> ( 0. L) by ALGSEQ_1: 10;

        (ps . lpn1) = (p . (n + lpn1)) by Def5;

        hence contradiction by A3, A5, A6, ALGSEQ_1:def 2;

      end;

      now

        let i be Nat;

        assume i >= lpn;

        then

         A7: (i + n) >= ( len p) by XREAL_1: 20;

        

        thus (ps . i) = (p . (n + i)) by Def5

        .= ( 0. L) by A7, ALGSEQ_1: 8;

      end;

      then lpn is_at_least_length_of ps by ALGSEQ_1:def 2;

      

      hence (( len ( poly_shift (p,n))) + n) = (lpn + n) by A2, ALGSEQ_1:def 3

      .= ( len p);

    end;

    theorem :: UPROOTS:45

    

     Th42: for L be non degenerated comRing, x be Element of L, n be Element of NAT , p be Polynomial of L st n < ( len p) holds ( eval (( poly_shift (p,n)),x)) = ((x * ( eval (( poly_shift (p,(n + 1))),x))) + (p . n))

    proof

      let L be non degenerated comRing, x be Element of L, n be Element of NAT , p be Polynomial of L such that

       A1: n < ( len p);

      set ps = ( poly_shift (p,n)), ps1 = ( poly_shift (p,(n + 1)));

      consider f be FinSequence of L such that

       A2: ( eval (ps,x)) = ( Sum f) and

       A3: ( len f) = ( len ps) and

       A4: for k be Element of NAT st k in ( dom f) holds (f . k) = ((ps . (k -' 1)) * (( power L) . (x,(k -' 1)))) by POLYNOM4:def 2;

      consider f1 be FinSequence of L such that

       A5: ( eval (ps1,x)) = ( Sum f1) and

       A6: ( len f1) = ( len ps1) and

       A7: for k be Element of NAT st k in ( dom f1) holds (f1 . k) = ((ps1 . (k -' 1)) * (( power L) . (x,(k -' 1)))) by POLYNOM4:def 2;

      ( rng f1) c= the carrier of L & ( dom (x multfield )) = the carrier of L by FUNCT_2:def 1;

      then

       A8: (x * f1) = ((x multfield ) * f1) & ( dom ((x multfield ) * f1)) = ( dom f1) by FVSUM_1:def 6, RELAT_1: 27;

      

       A9: ( 1_ L) = ( 1. L);

      now

        

         A10: (n + 1) <= ( len p) by A1, NAT_1: 13;

        

         A11: ((( len ps1) + 1) + n) = (( len ps1) + (n + 1))

        .= ( len p) by A10, Th41

        .= (( len ps) + n) by A1, Th41;

        thus ( len f) = ( len f);

        

         A12: ( len <*(p . n)*>) = 1 by FINSEQ_1: 40;

        

         A13: ( len (x * f1)) = ( len f1) by A8, FINSEQ_3: 29;

        hence ( len ( <*(p . n)*> ^ (x * f1))) = ( len f) by A3, A6, A11, A12, FINSEQ_1: 22;

        let j be Nat such that

         A14: j in ( dom f);

        

         A15: 1 <= j by A14, FINSEQ_3: 25;

        

         A16: j <= ( len f) by A14, FINSEQ_3: 25;

        per cases by A15, XXREAL_0: 1;

          suppose

           A17: j = 1;

          

           A18: 1 in ( dom <*(p . n)*>) by A12, FINSEQ_3: 25;

          

          thus (f . j) = ((ps . (1 -' 1)) * (( power L) . (x,(1 -' 1)))) by A4, A14, A17

          .= ((ps . 0 ) * (( power L) . (x,(1 -' 1)))) by XREAL_1: 232

          .= ((ps . 0 ) * (( power L) . (x, 0 ))) by XREAL_1: 232

          .= ((ps . 0 ) * ( 1. L)) by A9, GROUP_1:def 7

          .= (ps . 0 )

          .= (p . (n + 0 qua Nat)) by Def5

          .= ( <*(p . n)*> . 1) by FINSEQ_1: 40

          .= (( <*(p . n)*> ^ (x * f1)) . j) by A17, A18, FINSEQ_1:def 7;

        end;

          suppose

           A19: 1 < j;

          (1 - 1) <= (j - 1) by A15, XREAL_1: 9;

          then

          reconsider j1 = (j - 1) as Element of NAT by INT_1: 3;

          

           A20: (1 + 1) <= j by A19, NAT_1: 13;

          then

           A21: ((1 + 1) - 1) <= (j - 1) by XREAL_1: 9;

          then ex j2 be Nat st j1 = (j2 + 1) by NAT_1: 6;

          then

           A22: ((j1 -' 1) + 1) = j1 by NAT_D: 34;

          j = (j1 + 1);

          then

           A23: j1 = (j -' 1) by NAT_D: 34;

          (j - 1) <= ((( len f1) + 1) - 1) by A3, A6, A11, A16, XREAL_1: 9;

          then

           A24: j1 in ( dom f1) by A21, FINSEQ_3: 25;

          then

          reconsider f1j = (f1 . j1) as Element of L by FINSEQ_2: 11;

          

          thus (f . j) = ((ps . (j -' 1)) * (( power L) . (x,(j -' 1)))) by A4, A14

          .= ((p . (n + j1)) * (( power L) . (x,j1))) by A23, Def5

          .= ((p . ((n + 1) + (j1 -' 1))) * ((( power L) . (x,(j1 -' 1))) * x)) by A22, GROUP_1:def 7

          .= (x * ((p . ((n + 1) + (j1 -' 1))) * (( power L) . (x,(j1 -' 1))))) by GROUP_1:def 3

          .= (x * ((ps1 . (j1 -' 1)) * (( power L) . (x,(j1 -' 1))))) by Def5

          .= (x * f1j) by A7, A24

          .= ((x * f1) . j1) by A8, A24, FVSUM_1: 50

          .= (( <*(p . n)*> ^ (x * f1)) . j) by A3, A6, A11, A12, A13, A16, A20, FINSEQ_1: 23;

        end;

      end;

      then (x * ( Sum f1)) = ( Sum (x * f1)) & f = ( <*(p . n)*> ^ (x * f1)) by FINSEQ_2: 9, FVSUM_1: 73;

      hence thesis by A2, A5, FVSUM_1: 72;

    end;

    theorem :: UPROOTS:46

    

     Th43: for L be non degenerated comRing, p be Polynomial of L st ( len p) = 1 holds ( Roots p) = {}

    proof

      let L be non degenerated comRing, p be Polynomial of L;

      assume ( len p) = 1;

      then

       A1: p = <%(p . 0 )%> & (p . 0 ) <> ( 0. L) by Th16;

      assume ( Roots p) <> {} ;

      then

      consider x be object such that

       A2: x in ( Roots p) by XBOOLE_0:def 1;

      reconsider x as Element of L by A2;

      x is_a_root_of p by A2, POLYNOM5:def 10;

      then ( eval (p,x)) = ( 0. L);

      hence contradiction by A1, POLYNOM5: 37;

    end;

    definition

      let L be non degenerated comRing, r be Element of L, p be Polynomial of L;

      :: UPROOTS:def7

      func poly_quotient (p,r) -> Polynomial of L means

      : Def6: (( len it ) + 1) = ( len p) & for i be Nat holds (it . i) = ( eval (( poly_shift (p,(i + 1))),r)) if ( len p) > 0

      otherwise it = ( 0_. L);

      existence

      proof

        hereby

          r in ( Roots p) by A1, POLYNOM5:def 10;

          then

           A2: ( len p) <> 1 by Th43;

          deffunc F( Nat) = ( eval (( poly_shift (p,($1 + 1))),r));

          set lq = (( len p) -' 1);

          consider q be sequence of L such that

           A3: for k be Element of NAT holds (q . k) = F(k) from FUNCT_2:sch 4;

          reconsider q as sequence of L;

          assume

           A4: ( len p) > 0 ;

          then

          consider p1 be Nat such that

           A5: ( len p) = (p1 + 1) by NAT_1: 6;

          

           A6: lq = p1 by A5, NAT_D: 34;

          then

           A7: lq < ( len p) by A5, NAT_1: 13;

          ( len p) >= ( 0 qua Nat + 1) by A4, NAT_1: 13;

          then

          consider lq1 be Nat such that

           A8: lq = (lq1 + 1) by A5, A6, A2, NAT_1: 6;

           A9:

          now

            let i be Nat;

            assume i >= lq;

            then i >= p1 by A5, NAT_D: 34;

            then

             A10: (i + 1) >= ( len p) by A5, XREAL_1: 6;

            i in NAT by ORDINAL1:def 12;

            

            hence (q . i) = ( eval (( poly_shift (p,(i + 1))),r)) by A3

            .= ( eval (( 0_. L),r)) by A10, Th40

            .= ( 0. L) by POLYNOM4: 17;

          end;

          reconsider lq1 as Element of NAT by ORDINAL1:def 12;

          (q . lq1) = ( eval (( poly_shift (p,(lq1 + 1))),r)) by A3

          .= ((r * ( eval (( poly_shift (p,( len p))),r))) + (p . lq)) by A5, A6, A8, A7, Th42

          .= ((r * ( eval (( 0_. L),r))) + (p . lq)) by Th40

          .= ((r * ( 0. L)) + (p . lq)) by POLYNOM4: 17

          .= (( 0. L) + (p . lq))

          .= (p . lq) by RLVECT_1: 4;

          then

           A11: (q . lq1) <> ( 0. L) by A5, A6, ALGSEQ_1: 10;

          reconsider q as AlgSequence of L by A9, ALGSEQ_1:def 1;

          

           A12: lq1 = (lq -' 1) by A8, NAT_D: 34;

           A13:

          now

            let m be Nat;

            assume

             A14: m is_at_least_length_of q;

            assume

             A15: lq > m;

            then

            consider lq1 be Nat such that

             A16: lq = (lq1 + 1) by NAT_1: 6;

            lq1 >= m by A15, A16, NAT_1: 13;

            then (lq -' 1) >= m by A16, NAT_D: 34;

            hence contradiction by A12, A11, A14, ALGSEQ_1:def 2;

          end;

          take q;

          lq is_at_least_length_of q by A9, ALGSEQ_1:def 2;

          

          hence (( len q) + 1) = (((p1 + 1) -' 1) + 1) by A5, A13, ALGSEQ_1:def 3

          .= ( len p) by A5, NAT_D: 34;

          let k be Nat;

          k in NAT by ORDINAL1:def 12;

          hence (q . k) = F(k) by A3;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let it1,it2 be Polynomial of L;

        hereby

          assume ( len p) > 0 ;

          assume that

           A17: (( len it1) + 1) = ( len p) and

           A18: for i be Nat holds (it1 . i) = ( eval (( poly_shift (p,(i + 1))),r)) and

           A19: (( len it2) + 1) = ( len p) and

           A20: for i be Nat holds (it2 . i) = ( eval (( poly_shift (p,(i + 1))),r));

          now

            let k be Nat such that k < ( len it1);

            

            thus (it1 . k) = ( eval (( poly_shift (p,(k + 1))),r)) by A18

            .= (it2 . k) by A20;

          end;

          hence it1 = it2 by A17, A19, ALGSEQ_1: 12;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: UPROOTS:47

    

     Th44: for L be non degenerated comRing, r be Element of L, p be non-zero Polynomial of L st r is_a_root_of p holds ( len ( poly_quotient (p,r))) > 0

    proof

      let L be non degenerated comRing, r be Element of L, p be non-zero Polynomial of L such that

       A1: r is_a_root_of p;

      assume ( len ( poly_quotient (p,r))) <= 0 ;

      then

       A2: ( len ( poly_quotient (p,r))) = 0 ;

      ( len p) > 0 by Th14;

      then (( len ( poly_quotient (p,r))) + 1) = ( len p) by A1, Def6;

      then ( Roots p) = {} by A2, Th43;

      hence contradiction by A1, POLYNOM5:def 10;

    end;

    theorem :: UPROOTS:48

    

     Th45: for L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr, x be Element of L holds ( Roots <%( - x), ( 1. L)%>) = {x}

    proof

      let L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr, x be Element of L;

      now

        let a be object;

        hereby

          assume

           A1: a in ( Roots <%( - x), ( 1. L)%>);

          then

          reconsider b = a as Element of L;

          b is_a_root_of <%( - x), ( 1. L)%> by A1, POLYNOM5:def 10;

          

          then ( 0. L) = ( eval ( <%( - x), ( 1. L)%>,b))

          .= (( - x) + b) by POLYNOM5: 47;

          then ( - x) = ( - b) by RLVECT_1: 6;

          hence x = a by RLVECT_1: 18;

        end;

        ( eval ( <%( - x), ( 1. L)%>,x)) = (( - x) + x) by POLYNOM5: 47

        .= ( 0. L) by RLVECT_1: 5;

        then

         A2: x is_a_root_of <%( - x), ( 1. L)%>;

        assume a = x;

        hence a in ( Roots <%( - x), ( 1. L)%>) by A2, POLYNOM5:def 10;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: UPROOTS:49

    

     Th46: for L be non trivial comRing, x be Element of L, p,q be Polynomial of L st p = ( <%( - x), ( 1. L)%> *' q) holds x is_a_root_of p

    proof

      let L be non trivial comRing, x be Element of L, p,q be Polynomial of L such that

       A1: p = ( <%( - x), ( 1. L)%> *' q);

      

       A2: ( eval ( <%( - x), ( 1. L)%>,x)) = (( - x) + x) by POLYNOM5: 47

      .= ( 0. L) by RLVECT_1: 5;

      

      thus ( eval (p,x)) = (( eval ( <%( - x), ( 1. L)%>,x)) * ( eval (q,x))) by A1, POLYNOM4: 24

      .= ( 0. L) by A2;

    end;

    ::$Notion-Name

    theorem :: UPROOTS:50

    

     Th47: for L be non degenerated comRing, r be Element of L, p be Polynomial of L st r is_a_root_of p holds p = ( <%( - r), ( 1. L)%> *' ( poly_quotient (p,r)))

    proof

      let L be non degenerated comRing, x be Element of L, p be Polynomial of L;

      assume

       A1: x is_a_root_of p;

      set r = <%( - x), ( 1. L)%>, pq = ( poly_quotient (p,x));

      per cases ;

        suppose

         A2: ( len p) > 0 ;

        (r . (( len r) -' 1)) = (r . ((1 + 1) -' 1)) by POLYNOM5: 40

        .= (r . 1) by NAT_D: 34

        .= ( 1. L) by POLYNOM5: 38;

        then

         A3: ((r . (( len r) -' 1)) * (pq . (( len pq) -' 1))) = (pq . (( len pq) -' 1));

        p is non-zero by A2, Th14;

        then

         A4: ( len pq) > 0 by A1, Th44;

        now

          ( len (r *' pq)) = ((( len r) + ( len pq)) - 1) by A4, A3, Th15, POLYNOM4: 10

          .= ((( len pq) + (1 + 1)) - 1) by POLYNOM5: 40

          .= (( len pq) + 1)

          .= ( len p) by A1, A2, Def6;

          hence ( len p) = ( len (r *' pq));

          defpred P[ Nat] means (p . $1) = ((r *' pq) . $1);

          let k be Nat;

          assume k < ( len p);

          

           A5: ( 0. L) = ( eval (p,x)) by A1

          .= ( eval (( poly_shift (p, 0 )),x)) by Th39

          .= ((x * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x))) + (p . 0 )) by A2, Th42;

          

           A6: (( - x) * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x))) = ((( - x) * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x))) + ( 0. L)) by RLVECT_1:def 4

          .= (((( - x) * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x))) + (x * ( eval (( poly_shift (p,1)),x)))) + (p . 0 )) by A5, RLVECT_1:def 3

          .= ((( - (x * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x)))) + (x * ( eval (( poly_shift (p,1)),x)))) + (p . 0 )) by VECTSP_1: 9

          .= (( 0. L) + (p . 0 )) by RLVECT_1: 5

          .= (p . 0 ) by RLVECT_1: 4;

          

           A7: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume P[k];

            

             A8: (pq . (k + 1)) = ( eval (( poly_shift (p,((k + 1) + 1))),x)) by A1, A2, Def6;

            

             A9: (pq . k) = ( eval (( poly_shift (p,(k + 1))),x)) by A1, A2, Def6;

            per cases ;

              suppose

               A10: (k + 1) >= ( len p);

              

              then

               A11: (pq . (k + 1)) = ( eval (( 0_. L),x)) by A8, Th40, NAT_1: 12

              .= ( 0. L) by POLYNOM4: 17;

              

               A12: (pq . k) = ( eval (( 0_. L),x)) by A9, A10, Th40

              .= ( 0. L) by POLYNOM4: 17;

              ((r *' pq) . (k + 1)) = ((( - x) * (pq . (k + 1))) + (( 1. L) * (pq . k))) by Th34

              .= (( 0. L) + (( 1. L) * (pq . k))) by A11

              .= (( 0. L) + ( 0. L)) by A12

              .= ( 0. L) by RLVECT_1: 4;

              hence thesis by A10, ALGSEQ_1: 8;

            end;

              suppose (k + 1) < ( len p);

              then (pq . k) = ((x * ( eval (( poly_shift (p,((k + 1) + 1))),x))) + (p . (k + 1))) by A9, Th42;

              

              then

               A13: (( - (x * (pq . (k + 1)))) + (pq . k)) = ((( - (x * (pq . (k + 1)))) + (x * ( eval (( poly_shift (p,((k + 1) + 1))),x)))) + (p . (k + 1))) by RLVECT_1:def 3

              .= (( 0. L) + (p . (k + 1))) by A8, RLVECT_1: 5;

              ((r *' pq) . (k + 1)) = ((( - x) * (pq . (k + 1))) + (( 1. L) * (pq . k))) by Th34

              .= ((( - x) * (pq . (k + 1))) + (pq . k))

              .= (( - (x * (pq . (k + 1)))) + (pq . k)) by VECTSP_1: 9;

              hence thesis by A13, RLVECT_1: 4;

            end;

          end;

          ((r *' pq) . 0 ) = (( - x) * (pq . 0 )) by Th34

          .= (( - x) * ( eval (( poly_shift (p,( 0 qua Nat + 1))),x))) by A1, A2, Def6;

          then

           A14: P[ 0 ] by A6;

          for k be Nat holds P[k] from NAT_1:sch 2( A14, A7);

          hence (p . k) = ((r *' pq) . k);

        end;

        hence thesis by ALGSEQ_1: 12;

      end;

        suppose ( len p) = 0 ;

        then pq = ( 0_. L) & p = ( 0_. L) by A1, Def6, POLYNOM4: 5;

        hence thesis by POLYNOM3: 34;

      end;

    end;

    theorem :: UPROOTS:51

    for L be non degenerated comRing, r be Element of L, p,q be Polynomial of L st p = ( <%( - r), ( 1. L)%> *' q) holds r is_a_root_of p

    proof

      let L be non degenerated comRing, r be Element of L, p,q be Polynomial of L;

      assume p = ( <%( - r), ( 1. L)%> *' q);

      

      then ( eval (p,r)) = (( eval ( <%( - r), ( 1. L)%>,r)) * ( eval (q,r))) by POLYNOM4: 24

      .= ((( - r) + r) * ( eval (q,r))) by POLYNOM5: 47

      .= (( 0. L) * ( eval (q,r))) by RLVECT_1:def 10

      .= ( 0. L);

      hence thesis;

    end;

     Lm1:

    now

      let L be domRing, p be non-zero Polynomial of L;

      defpred P[ Nat] means for p be Polynomial of L st ( len p) = $1 holds ( Roots p) is finite & ex n be Element of NAT st n = ( card ( Roots p)) & n < ( len p);

      p <> ( 0_. L) by Def4;

      then ( len p) <> 0 by POLYNOM4: 5;

      then

       A1: ( len p) >= ( 0 qua Nat + 1) by NAT_1: 13;

      

       A2: for n be Nat st n >= 1 & P[n] holds P[(n + 1)]

      proof

        let n be Nat such that n >= 1 and

         A3: P[n];

        let p be Polynomial of L;

        assume

         A4: ( len p) = (n + 1);

        per cases ;

          suppose p is with_roots;

          then

          consider x be Element of L such that

           A5: x is_a_root_of p;

          set r = <%( - x), ( 1. L)%>, pq = ( poly_quotient (p,x));

          

           A6: p = ( <%( - x), ( 1. L)%> *' ( poly_quotient (p,x))) by A5, Th47;

          then

           A7: ( Roots p) = (( Roots r) \/ ( Roots pq)) by Th20;

          

           A8: ( Roots r) = {x} by Th45;

          then

          reconsider Rr = ( Roots r) as finite set;

          

           A9: (( len pq) + 1) = ( len p) by A4, A5, Def6;

          then

          consider k be Element of NAT such that

           A10: k = ( card ( Roots pq)) and

           A11: k < ( len pq) by A3, A4;

          reconsider Rpq = ( Roots pq) as finite set by A3, A4, A9;

          reconsider Rp = (Rpq \/ Rr) as finite set;

          ( card Rr) = 1 by A8, CARD_1: 30;

          then

           A12: ( card Rp) <= (k + 1) by A10, CARD_2: 43;

          ( Roots pq) is finite by A3, A4, A9;

          hence ( Roots p) is finite by A8, A7;

          take m = ( card Rp);

          thus m = ( card ( Roots p)) by A6, Th20;

          (k + 1) < (n + 1) by A4, A9, A11, XREAL_1: 8;

          hence thesis by A4, A12, XXREAL_0: 2;

        end;

          suppose

           A13: not p is with_roots;

           A14:

          now

            assume ( Roots p) <> {} ;

            then

            consider x be object such that

             A15: x in ( Roots p) by XBOOLE_0:def 1;

            reconsider x as Element of L by A15;

            x is_a_root_of p by A15, POLYNOM5:def 10;

            hence contradiction by A13;

          end;

          hence ( Roots p) is finite;

          take 0 ;

          thus 0 = ( card ( Roots p)) by A14;

          thus thesis by A4;

        end;

      end;

      

       A16: P[1]

      proof

        let p be Polynomial of L;

        assume

         A17: ( len p) = 1;

        hence ( Roots p) is finite by Th43;

        take 0 ;

        thus 0 = ( card ( Roots p)) by A17, Th43, CARD_1: 27;

        thus thesis by A17;

      end;

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A16, A2);

      hence ( Roots p) is finite & ex n be Element of NAT st n = ( card ( Roots p)) & n < ( len p) by A1;

    end;

    begin

    registration

      let L be domRing, p be non-zero Polynomial of L;

      cluster ( Roots p) -> finite;

      correctness by Lm1;

    end

    definition

      let L be non degenerated comRing, x be Element of L, p be non-zero Polynomial of L;

      :: UPROOTS:def8

      func multiplicity (p,x) -> Element of NAT means

      : Def7: ex F be finite non empty Subset of NAT st F = { k where k be Element of NAT : ex q be Polynomial of L st p = (( <%( - x), ( 1. L)%> `^ k) *' q) } & it = ( max F);

      existence

      proof

        set r = <%( - x), ( 1. L)%>;

        defpred P[ Element of NAT ] means ex q be Polynomial of L st p = ((r `^ $1) *' q);

        set F = { k where k be Element of NAT : P[k] };

        

         A1: F c= NAT from FRAENKEL:sch 10;

        p = (( 1_. L) *' p) by POLYNOM3: 35

        .= ((r `^ 0 ) *' p) by POLYNOM5: 15;

        then

         A2: 0 in F;

        

         A3: ( len p) > 0 by Th14;

        F c= ( len p)

        proof

          let a be object;

          assume a in F;

          then

          consider k be Element of NAT such that

           A4: a = k and

           A5: P[k];

          consider q be Polynomial of L such that

           A6: p = ((r `^ k) *' q) by A5;

           A7:

          now

            assume ( len q) = 0 ;

            then q = ( 0_. L) by POLYNOM4: 5;

            then p = ( 0_. L) by A6, POLYNOM4: 2;

            hence contradiction by A3, POLYNOM4: 3;

          end;

          then

          reconsider q as non-zero Polynomial of L by Th14;

          now

            assume k >= ( len p);

            then (k + ( len q)) > (( len p) + 0 qua Nat) by A7, XREAL_1: 8;

            hence contradiction by A6, Th37;

          end;

          then k in { i where i be Nat : i < ( len p) };

          hence thesis by A4, AXIOMS: 4;

        end;

        then

        reconsider F as finite non empty Subset of NAT by A2, A1;

        reconsider FF = F as finite non empty natural-membered set;

        reconsider m = ( max FF) as Element of NAT by ORDINAL1:def 12;

        take m;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: UPROOTS:52

    

     Th49: for L be non degenerated comRing, p be non-zero Polynomial of L, x be Element of L holds x is_a_root_of p iff ( multiplicity (p,x)) >= 1

    proof

      let L be non degenerated comRing, p be non-zero Polynomial of L, x be Element of L;

      set r = <%( - x), ( 1. L)%>;

      set m = ( 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: m = ( max F) by Def7;

      m in F by A2, XXREAL_2:def 8;

      then

      consider k be Element of NAT such that

       A3: m = k and

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

      hereby

        assume x is_a_root_of p;

        then

         A5: p = (r *' ( poly_quotient (p,x))) by Th47;

        (r `^ 1) = r by POLYNOM5: 16;

        then 1 in F by A1, A5;

        hence ( multiplicity (p,x)) >= 1 by A2, XXREAL_2:def 8;

      end;

      consider q be Polynomial of L such that

       A6: p = ((r `^ k) *' q) by A4;

      assume ( multiplicity (p,x)) >= 1;

      then

      consider k1 be Nat such that

       A7: k = (k1 + 1) by A3, NAT_1: 6;

      reconsider k1 as Element of NAT by ORDINAL1:def 12;

      p = ((r *' (r `^ k1)) *' q) by A6, A7, POLYNOM5: 19

      .= (r *' ((r `^ k1) *' q)) by POLYNOM3: 33;

      hence thesis by Th46;

    end;

    theorem :: UPROOTS:53

    

     Th50: for L be non degenerated comRing, x be Element of L holds ( multiplicity ( <%( - x), ( 1. L)%>,x)) = 1

    proof

      let L be non degenerated comRing, x be Element of L;

      set r = <%( - x), ( 1. L)%>;

      set j = ( multiplicity (r,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 r = ((r `^ k) *' q) } and

       A2: ( multiplicity (r,x)) = ( max F) by Def7;

      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 r = ((r `^ k) *' q) by A1;

      consider q be Polynomial of L such that

       A5: r = ((r `^ k) *' q) by A4;

      

       A6: ( len r) = 2 by POLYNOM5: 40;

       A7:

      now

        assume ( len q) = 0 ;

        then q = ( 0_. L) by POLYNOM4: 5;

        then r = ( 0_. L) by A5, POLYNOM4: 2;

        hence contradiction by A6, POLYNOM4: 3;

      end;

      then

       A8: q is non-zero by Th14;

       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, Th37;

      end;

      r = (r `^ 1) by POLYNOM5: 16;

      then r = ((r `^ 1) *' ( 1_. L)) by POLYNOM3: 35;

      then 1 in F by A1;

      then ( multiplicity (r,x)) >= 1 by A2, XXREAL_2:def 8;

      hence thesis by A3, A9, XXREAL_0: 1;

    end;

    definition

      let L be domRing, p be non-zero Polynomial of L;

      :: UPROOTS:def9

      func BRoots (p) -> bag of the carrier of L means

      : Def8: ( support it ) = ( Roots p) & for x be Element of L holds (it . x) = ( multiplicity (p,x));

      existence

      proof

        deffunc F( Element of L) = ( multiplicity (p,$1));

        consider b be Function of the carrier of L, NAT such that

         A1: for x be Element of L holds (b . x) = F(x) from FUNCT_2:sch 4;

        ( dom b) = the carrier of L by FUNCT_2:def 1;

        then

         A2: ( support b) c= the carrier of L by PRE_POLY: 37;

         A3:

        now

          let x be object;

          hereby

            assume

             A4: x in ( support b);

            then

            reconsider xx = x as Element of L by A2;

            (b . x) <> 0 by A4, PRE_POLY:def 7;

            then

             A5: (b . xx) >= ( 0 qua Nat + 1) by NAT_1: 13;

            (b . x) = F(xx) by A1;

            then xx is_a_root_of p by A5, Th49;

            hence x in ( Roots p) by POLYNOM5:def 10;

          end;

          assume

           A6: x in ( Roots p);

          then

          reconsider xx = x as Element of L;

          xx is_a_root_of p by A6, POLYNOM5:def 10;

          then ( multiplicity (p,xx)) >= 1 by Th49;

          then (b . xx) >= 1 by A1;

          hence x in ( support b) by PRE_POLY:def 7;

        end;

        then ( support b) = ( Roots p) by TARSKI: 2;

        then

        reconsider b as bag of the carrier of L by PRE_POLY:def 8;

        take b;

        thus thesis by A1, A3, TARSKI: 2;

      end;

      uniqueness

      proof

        let it1,it2 be bag of the carrier of L such that ( support it1) = ( Roots p) and

         A7: for x be Element of L holds (it1 . x) = ( multiplicity (p,x)) and ( support it2) = ( Roots p) and

         A8: for x be Element of L holds (it2 . x) = ( multiplicity (p,x));

        now

          let x be object;

          assume x in the carrier of L;

          then

          reconsider xx = x as Element of L;

          

          thus (it1 . x) = ( multiplicity (p,xx)) by A7

          .= (it2 . x) by A8;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    theorem :: UPROOTS:54

    

     Th51: for L be domRing, x be Element of L holds ( BRoots <%( - x), ( 1. L)%>) = (( {x},1) -bag )

    proof

      let L be domRing, x be Element of L;

      set r = <%( - x), ( 1. L)%>;

      ( Roots r) = {x} by Th45;

      then

       A1: ( support ( BRoots r)) = {x} by Def8;

      

       A2: x in {x} 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 = x;

          

          thus (( BRoots r) . i) = ( multiplicity (r,i1)) by Def8

          .= 1 by A3, Th50

          .= ((( {x},1) -bag ) . i) by A2, A3, Th4;

        end;

          suppose i <> x;

          then

           A4: not i in {x} by TARSKI:def 1;

          

          hence (( BRoots r) . i) = 0 by A1, PRE_POLY:def 7

          .= ((( {x},1) -bag ) . i) by A4, Th3;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: UPROOTS:55

    

     Th52: for L be domRing, x be Element of L, p,q be non-zero Polynomial of L holds ( multiplicity ((p *' q),x)) = (( multiplicity (p,x)) + ( multiplicity (q,x)))

    proof

      let L be domRing, x be Element of L, p,q be non-zero Polynomial of L;

      set r = <%( - x), ( 1. L)%>;

      consider F be finite non empty Subset of NAT such that

       A1: F = { k where k be Element of NAT : ex pqq be Polynomial of L st (p *' q) = ((r `^ k) *' pqq) } and

       A2: ( multiplicity ((p *' q),x)) = ( max F) by Def7;

      consider f be finite non empty Subset of NAT such that

       A3: f = { k where k be Element of NAT : ex pq be Polynomial of L st p = ((r `^ k) *' pq) } and

       A4: ( multiplicity (p,x)) = ( max f) by Def7;

      ( max f) in f by XXREAL_2:def 8;

      then

      consider i be Element of NAT such that

       A5: i = ( max f) and

       A6: ex pq be Polynomial of L st p = ((r `^ i) *' pq) by A3;

      consider pq be Polynomial of L such that

       A7: p = ((r `^ i) *' pq) by A6;

      consider g be finite non empty Subset of NAT such that

       A8: g = { k where k be Element of NAT : ex qq be Polynomial of L st q = ((r `^ k) *' qq) } and

       A9: ( multiplicity (q,x)) = ( max g) by Def7;

      ( max F) in F by XXREAL_2:def 8;

      then

      consider k be Element of NAT such that

       A10: k = ( max F) and

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

      consider pqq be Polynomial of L such that

       A12: (p *' q) = ((r `^ k) *' pqq) by A11;

      ( max g) in g by XXREAL_2:def 8;

      then

      consider j be Element of NAT such that

       A13: j = ( max g) and

       A14: ex qq be Polynomial of L st q = ((r `^ j) *' qq) by A8;

      consider qq be Polynomial of L such that

       A15: q = ((r `^ j) *' qq) by A14;

      

       A16: (p *' q) = ((((r `^ i) *' pq) *' (r `^ j)) *' qq) by A7, A15, POLYNOM3: 33

      .= ((((r `^ i) *' (r `^ j)) *' pq) *' qq) by POLYNOM3: 33

      .= (((r `^ (i + j)) *' pq) *' qq) by Th27

      .= ((r `^ (i + j)) *' (pq *' qq)) by POLYNOM3: 33;

       A17:

      now

        assume (i + j) < k;

        then ( 0 qua Nat + (i + j)) < k;

        then

         A18: 0 < (k - (i + j)) by XREAL_1: 20;

        then

        reconsider kij = (k - (i + j)) as Element of NAT by INT_1: 3;

        consider kk be Nat such that

         A19: kij = (kk + 1) by A18, NAT_1: 6;

        reconsider kk as Element of NAT by ORDINAL1:def 12;

        (r `^ kij) = ((r `^ 1) *' (r `^ kk)) by A19, Th27

        .= (r *' (r `^ kk)) by POLYNOM5: 16;

        then

         A20: ((r `^ kij) *' pqq) = (r *' ((r `^ kk) *' pqq)) by POLYNOM3: 33;

        (( 0_. L) . 1) = ( 0. L) & (r . 1) = ( 1. L) by FUNCOP_1: 7, POLYNOM5: 38;

        then

         A21: (r `^ (i + j)) <> ( 0_. L) by Th26;

        k = (kij + (i + j));

        

        then (p *' q) = (((r `^ (i + j)) *' (r `^ kij)) *' pqq) by A12, Th27

        .= ((r `^ (i + j)) *' ((r `^ kij) *' pqq)) by POLYNOM3: 33;

        then x is_a_root_of (pq *' qq) by A16, A21, A20, Th25, Th46;

        then x in ( Roots (pq *' qq)) by POLYNOM5:def 10;

        then

         A22: x in (( Roots pq) \/ ( Roots qq)) by Th20;

        per cases by A22, XBOOLE_0:def 3;

          suppose x in ( Roots pq);

          then x is_a_root_of pq by POLYNOM5:def 10;

          then pq = (r *' ( poly_quotient (pq,x))) by Th47;

          

          then p = (((r `^ i) *' r) *' ( poly_quotient (pq,x))) by A7, POLYNOM3: 33

          .= (((r `^ i) *' (r `^ 1)) *' ( poly_quotient (pq,x))) by POLYNOM5: 16

          .= ((r `^ (i + 1)) *' ( poly_quotient (pq,x))) by Th27;

          then (i + 1) in f by A3;

          then (i + 1) <= i by A5, XXREAL_2:def 8;

          hence contradiction by NAT_1: 13;

        end;

          suppose x in ( Roots qq);

          then x is_a_root_of qq by POLYNOM5:def 10;

          then qq = (r *' ( poly_quotient (qq,x))) by Th47;

          

          then q = (((r `^ j) *' r) *' ( poly_quotient (qq,x))) by A15, POLYNOM3: 33

          .= (((r `^ j) *' (r `^ 1)) *' ( poly_quotient (qq,x))) by POLYNOM5: 16

          .= ((r `^ (j + 1)) *' ( poly_quotient (qq,x))) by Th27;

          then (j + 1) in g by A8;

          then (j + 1) <= j by A13, XXREAL_2:def 8;

          hence contradiction by NAT_1: 13;

        end;

      end;

      (i + j) in F by A1, A16;

      then (i + j) <= k by A10, XXREAL_2:def 8;

      hence thesis by A2, A4, A9, A10, A5, A13, A17, XXREAL_0: 1;

    end;

    theorem :: UPROOTS:56

    

     Th53: for L be domRing, p,q be non-zero Polynomial of L holds ( BRoots (p *' q)) = (( BRoots p) + ( BRoots q))

    proof

      let L be domRing, p,q be non-zero Polynomial of L;

      now

        let i be object;

        assume i in the carrier of L;

        then

        reconsider x = i as Element of L;

        

        thus (( BRoots (p *' q)) . i) = ( multiplicity ((p *' q),x)) by Def8

        .= (( multiplicity (p,x)) + ( multiplicity (q,x))) by Th52

        .= ((( BRoots p) . i) + ( multiplicity (q,x))) by Def8

        .= ((( BRoots p) . i) + (( BRoots q) . i)) by Def8

        .= ((( BRoots p) + ( BRoots q)) . i) by PRE_POLY:def 5;

      end;

      hence thesis by PBOOLE: 3;

    end;

     Lm2:

    now

      let L be domRing, p,q be non-zero Polynomial of L;

      ( BRoots (p *' q)) = (( BRoots p) + ( BRoots q)) by Th53;

      hence ( degree ( BRoots (p *' q))) = (( degree ( BRoots p)) + ( degree ( BRoots q))) by Th12;

    end;

    theorem :: UPROOTS:57

    

     Th54: for L be domRing, p be non-zero Polynomial of L st ( len p) = 1 holds ( degree ( BRoots p)) = 0

    proof

      let L be domRing, p be non-zero Polynomial of L;

      assume ( len p) = 1;

      then ( Roots p) = {} by Th43;

      then ( support ( BRoots p)) = {} by Def8;

      then ( BRoots p) = ( EmptyBag the carrier of L) by PRE_POLY: 81;

      hence thesis by Th8;

    end;

    theorem :: UPROOTS:58

    

     Th55: for L be domRing, x be Element of L, n be Nat holds ( degree ( BRoots ( <%( - x), ( 1. L)%> `^ n))) = n

    proof

      let L be domRing, x be Element of L;

      set r = <%( - x), ( 1. L)%>;

      defpred P[ Nat] means ( degree ( BRoots (r `^ $1))) = $1;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: P[n];

        (r `^ (n + 1)) = ((r `^ n) *' r) by POLYNOM5: 19;

        

        then

         A3: ( degree ( BRoots (r `^ (n + 1)))) = (( degree ( BRoots (r `^ n))) + ( degree ( BRoots r))) by Lm2

        .= (n + ( degree (( {x},1) -bag ))) by A2, Th51;

        ( card {x}) = 1 by CARD_1: 30;

        hence thesis by A3, Th10;

      end;

      ( len ( 1_. L)) = 1 & (r `^ 0 ) = ( 1_. L) by POLYNOM4: 4, POLYNOM5: 15;

      then

       A4: P[ 0 ] by Th54;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A4, A1);

    end;

    theorem :: UPROOTS:59

    for L be algebraic-closed domRing, p be non-zero Polynomial of L holds ( degree ( BRoots p)) = (( len p) -' 1)

    proof

      let L be algebraic-closed domRing, p be non-zero Polynomial of L;

      defpred P[ Nat] means for p be non-zero Polynomial of L st ( len p) = $1 & $1 > 0 holds ( degree ( BRoots p)) = (( len p) -' 1);

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds P[n];

        let p be non-zero Polynomial of L;

        assume that

         A3: ( len p) = k and

         A4: k > 0 ;

        

         A5: k >= ( 0 qua Nat + 1) by A4, NAT_1: 13;

        thus thesis

        proof

          per cases by A5, XXREAL_0: 1;

            suppose

             A6: k = 1;

            

            hence ( degree ( BRoots p)) = (1 - 1) by A3, Th54

            .= (( len p) -' 1) by A3, A6, XREAL_1: 233;

          end;

            suppose

             A7: k > 1;

            then p is with_roots by A3, POLYNOM5:def 9;

            then

            consider x be Element of L such that

             A8: x is_a_root_of p;

            

             A9: ( multiplicity (p,x)) >= 1 by A8, Th49;

            set r = <%( - x), ( 1. L)%>;

            consider F be finite non empty Subset of NAT such that

             A10: F = { l where l be Element of NAT : ex q be Polynomial of L st p = (( <%( - x), ( 1. L)%> `^ l) *' q) } and

             A11: ( multiplicity (p,x)) = ( max F) by Def7;

            ( max F) in F by XXREAL_2:def 8;

            then

            consider l be Element of NAT such that

             A12: l = ( max F) and

             A13: ex q be Polynomial of L st p = (( <%( - x), ( 1. L)%> `^ l) *' q) by A10;

            set rr = ( <%( - x), ( 1. L)%> `^ l);

            consider q be Polynomial of L such that

             A14: p = (( <%( - x), ( 1. L)%> `^ l) *' q) by A13;

            reconsider q as non-zero Polynomial of L by A14, Th31;

            ( len q) > 0 by Th14;

            then

             A15: ( len q) >= ( 0 qua Nat + 1) by NAT_1: 13;

            thus thesis

            proof

              ( len q) > 0 by Th14;

              then

               A16: (q . (( len q) -' 1)) <> ( 0. L) by Th15;

              ( len rr) > 0 by Th14;

              then (rr . (( len rr) -' 1)) <> ( 0. L) by Th15;

              then

               A17: ((rr . (( len rr) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) by A16, VECTSP_2:def 1;

              

               A18: (((l * 2) - l) + 1) = (l + 1);

              

               A19: ( len r) = 2 by POLYNOM5: 40;

              then

               A20: ( len rr) = (((l * 2) - l) + 1) by POLYNOM5: 23;

              then

               A21: ( len rr) > 1 by A9, A11, A12, NAT_1: 13;

              per cases by A15, XXREAL_0: 1;

                suppose

                 A22: ( len q) = 1;

                

                 A23: ( len p) = ((( len rr) + ( len q)) - 1) by A14, A17, POLYNOM4: 10

                .= ( len rr) by A22;

                

                thus ( degree ( BRoots p)) = (( degree ( BRoots rr)) + ( degree ( BRoots q))) by A14, Lm2

                .= (( degree ( BRoots rr)) + 0 qua Nat) by A22, Th54

                .= ((((2 * l) - l) + 1) - 1) by Th55

                .= (( len p) -' 1) by A3, A5, A20, A23, XREAL_1: 233;

              end;

                suppose

                 A24: ( len q) > 1;

                then

                 A25: ( degree ( BRoots rr)) = ((l + 1) -' 1) & ( degree ( BRoots q)) = (( len q) -' 1) by A2, A3, A14, A20, A21, Th33;

                

                thus ( degree ( BRoots p)) = (( degree ( BRoots rr)) + ( degree ( BRoots q))) by A14, Lm2

                .= ((( len rr) -' 1) + (( len q) -' 1)) by A19, A18, A25, POLYNOM5: 23

                .= ((( len rr) - 1) + (( len q) -' 1)) by A21, XREAL_1: 233

                .= ((( len rr) - 1) + (( len q) - 1)) by A24, XREAL_1: 233

                .= (((( len rr) + ( len q)) - 1) - 1)

                .= (( len p) - 1) by A14, A17, POLYNOM4: 10

                .= (( len p) -' 1) by A3, A7, XREAL_1: 233;

              end;

            end;

          end;

        end;

      end;

      

       A26: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len p) > 0 by Th14;

      hence thesis by A26;

    end;

    definition

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c be Element of L, n be Element of NAT ;

      :: UPROOTS:def10

      func fpoly_mult_root (c,n) -> FinSequence of ( Polynom-Ring L) means

      : Def9: ( len it ) = n & for i be Element of NAT st i in ( dom it ) holds (it . i) = <%( - c), ( 1. L)%>;

      existence

      proof

         <%( - c), ( 1. L)%> is Element of ( Polynom-Ring L) by POLYNOM3:def 10;

        then

        reconsider f = (n |-> <%( - c), ( 1. L)%>) as FinSequence of ( Polynom-Ring L) by FINSEQ_2: 63;

        take f;

        thus

         A1: ( len f) = n by CARD_1:def 7;

        let i be Element of NAT ;

        assume i in ( dom f);

        then i in ( Seg n) by A1, FINSEQ_1:def 3;

        hence thesis by FUNCOP_1: 7;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of ( Polynom-Ring L) such that

         A2: ( len it1) = n and

         A3: for i be Element of NAT st i in ( dom it1) holds (it1 . i) = <%( - c), ( 1. L)%> and

         A4: ( len it2) = n and

         A5: for i be Element of NAT st i in ( dom it2) holds (it2 . i) = <%( - c), ( 1. L)%>;

        

         A6: ( dom it1) = ( dom it2) by A2, A4, FINSEQ_3: 29;

        now

          let x be Nat;

          assume

           A7: x in ( dom it1);

          

          hence (it1 . x) = <%( - c), ( 1. L)%> by A3

          .= (it2 . x) by A5, A6, A7;

        end;

        hence thesis by A6;

      end;

    end

    definition

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L;

      :: UPROOTS:def11

      func poly_with_roots (b) -> Polynomial of L means

      : Def10: ex f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L st ( len f) = ( card ( support b)) & s = ( canFS ( support b)) & (for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i))))) & it = ( Product ( FlattenSeq f));

      existence

      proof

        ( rng ( canFS ( support b))) c= the carrier of L by XBOOLE_1: 1;

        then

        reconsider s = ( canFS ( support b)) as FinSequence of L by FINSEQ_1:def 4;

        deffunc F( set) = ( fpoly_mult_root ((s /. $1),(b . (s /. $1))));

        consider f be FinSequence such that

         A1: ( len f) = ( card ( support b)) and

         A2: for k be Nat st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

        ( rng f) c= (the carrier of ( Polynom-Ring L) * )

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider i be Nat such that

           A3: i in ( dom f) & (f . i) = x by FINSEQ_2: 10;

          x = F(i) by A2, A3;

          hence thesis by FINSEQ_1:def 11;

        end;

        then

        reconsider f as FinSequence of (the carrier of ( Polynom-Ring L) * ) by FINSEQ_1:def 4;

        reconsider it1 = ( Product ( FlattenSeq f)) as Polynomial of L by POLYNOM3:def 10;

        take it1, f, s;

        thus ( len f) = ( card ( support b)) by A1;

        thus s = ( canFS ( support b));

        thus for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) by A2;

        thus thesis;

      end;

      uniqueness

      proof

        let it1,it2 be Polynomial of L;

        given f1 be FinSequence of (the carrier of ( Polynom-Ring L) * ), s1 be FinSequence of L such that

         A4: ( len f1) = ( card ( support b)) and

         A5: s1 = ( canFS ( support b)) and

         A6: for i be Element of NAT st i in ( dom f1) holds (f1 . i) = ( fpoly_mult_root ((s1 /. i),(b . (s1 /. i)))) and

         A7: it1 = ( Product ( FlattenSeq f1));

        given f2 be FinSequence of (the carrier of ( Polynom-Ring L) * ), s2 be FinSequence of L such that

         A8: ( len f2) = ( card ( support b)) and

         A9: s2 = ( canFS ( support b)) & for i be Element of NAT st i in ( dom f2) holds (f2 . i) = ( fpoly_mult_root ((s2 /. i),(b . (s2 /. i)))) and

         A10: it2 = ( Product ( FlattenSeq f2));

        

         A11: ( dom f1) = ( dom f2) by A4, A8, FINSEQ_3: 29;

        now

          let i be Nat;

          assume

           A12: i in ( dom f1);

          

          hence (f1 . i) = ( fpoly_mult_root ((s1 /. i),(b . (s1 /. i)))) by A6

          .= (f2 . i) by A5, A9, A11, A12;

        end;

        hence thesis by A4, A7, A8, A10, FINSEQ_2: 9;

      end;

    end

    theorem :: UPROOTS:60

    

     Th57: for L be Abelian add-associative right_zeroed right_complementable commutative distributive well-unital non empty doubleLoopStr holds ( poly_with_roots ( EmptyBag the carrier of L)) = <%( 1. L)%>

    proof

      let L be Abelian add-associative right_zeroed right_complementable commutative distributive well-unital non empty doubleLoopStr;

      set b = ( EmptyBag the carrier of L);

      consider f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L such that

       A1: ( len f) = ( card ( support b)) and s = ( canFS ( support b)) and for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) and

       A2: ( poly_with_roots b) = ( Product ( FlattenSeq f)) by Def10;

      f = ( <*> (the carrier of ( Polynom-Ring L) * )) by A1;

      then ( 1_ ( Polynom-Ring L)) = ( 1. ( Polynom-Ring L)) & ( FlattenSeq f) = ( <*> the carrier of ( Polynom-Ring L));

      

      then ( Product ( FlattenSeq f)) = ( 1. ( Polynom-Ring L)) by GROUP_4: 8

      .= ( 1_. L) by POLYNOM3: 37;

      hence thesis by A2, Th28;

    end;

    theorem :: UPROOTS:61

    

     Th58: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c be Element of L holds ( poly_with_roots (( {c},1) -bag )) = <%( - c), ( 1. L)%>

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, c be Element of L;

      set b = (( {c},1) -bag );

      consider f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L such that

       A1: ( len f) = ( card ( support b)) and

       A2: s = ( canFS ( support b)) and

       A3: for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) and

       A4: ( poly_with_roots b) = ( Product ( FlattenSeq f)) by Def10;

      

       A5: ( support b) = {c} by Th5;

      then

       A6: s = <*c*> by A2, FINSEQ_1: 94;

      

       A7: ( card ( support b)) = 1 by A5, CARD_1: 30;

      then

       A8: 1 in ( dom f) by A1, FINSEQ_3: 25;

      then

       A9: (f . 1) = (f /. 1) by PARTFUN1:def 6;

      ( len s) = 1 by A2, A7, FINSEQ_1: 93;

      then 1 in ( dom s) by FINSEQ_3: 25;

      

      then

       A10: (s /. 1) = (s . 1) by PARTFUN1:def 6

      .= c by A6, FINSEQ_1: 40;

      set f1 = ( fpoly_mult_root ((s /. 1),(b . (s /. 1))));

      c in {c} by TARSKI:def 1;

      then (b . (s /. 1)) = 1 by A10, Th4;

      then

       A11: ( len f1) = 1 by Def9;

      then

       A12: 1 in ( dom f1) by FINSEQ_3: 25;

      f = <*(f . 1)*> by A1, A5, CARD_1: 30, FINSEQ_5: 14;

      then

       A13: ( FlattenSeq f) = (f . 1) by A9, PRE_POLY: 1;

      

       A14: (f . 1) = ( fpoly_mult_root ((s /. 1),(b . (s /. 1)))) by A3, A8;

      

       A: (f1 . 1) = (f1 /. 1) by PARTFUN1:def 6, A12;

      f1 = <*(f1 . 1)*> by A11, FINSEQ_5: 14;

      

      hence ( poly_with_roots (( {c},1) -bag )) = (f1 . 1) by A, A4, A13, A14, FINSOP_1: 11

      .= <%( - c), ( 1. L)%> by A10, A12, Def9;

    end;

    theorem :: UPROOTS:62

    

     Th59: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L st ( len f) = ( card ( support b)) & s = ( canFS ( support b)) & (for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i))))) holds ( len ( FlattenSeq f)) = ( degree b)

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L such that

       A1: ( len f) = ( card ( support b)) and

       A2: s = ( canFS ( support b)) and

       A3: for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i))));

      reconsider Cf = ( Card f) as FinSequence of NAT ;

      consider g be FinSequence of NAT such that

       A4: ( degree b) = ( Sum g) and

       A5: g = (b * ( canFS ( support b))) by Def3;

      ( len s) = ( card ( support b)) by A2, FINSEQ_1: 93;

      then

       A6: ( dom f) = ( dom s) by A1, FINSEQ_3: 29;

       A7:

      now

        

         A8: ( rng s) c= ( dom b)

        proof

          let x be object;

          assume x in ( rng s);

          then

           A9: x in ( support b) by A2, FUNCT_2:def 3;

          ( support b) c= ( dom b) by PRE_POLY: 37;

          hence thesis by A9;

        end;

        

        thus ( dom ( Card f)) = ( dom f) by CARD_3:def 2

        .= ( dom g) by A2, A6, A5, A8, RELAT_1: 27;

        let i be Nat;

        assume i in ( dom ( Card f));

        then

         A10: i in ( dom f) by CARD_3:def 2;

        then

         A11: (g . i) = (b . (s . i)) by A2, A6, A5, FUNCT_1: 13;

        (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) by A3, A10;

        then

         A12: ( len (f . i)) = (b . (s /. i)) by Def9;

        

        thus (Cf . i) = ( card (f . i)) by A10, CARD_3:def 2

        .= (g . i) by A6, A10, A12, A11, PARTFUN1:def 6;

      end;

      ( len ( FlattenSeq f)) = ( Sum Cf) by PRE_POLY: 27;

      hence thesis by A4, A7, FINSEQ_1: 13;

    end;

    theorem :: UPROOTS:63

    

     Th60: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L, c be Element of L st ( len f) = ( card ( support b)) & s = ( canFS ( support b)) & (for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i))))) holds (c in ( support b) implies ( card (( FlattenSeq f) " { <%( - c), ( 1. L)%>})) = (b . c)) & ( not c in ( support b) implies ( card (( FlattenSeq f) " { <%( - c), ( 1. L)%>})) = 0 )

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, b be bag of the carrier of L, f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L, c be Element of L such that

       A1: ( len f) = ( card ( support b)) and

       A2: s = ( canFS ( support b)) and

       A3: for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i))));

      ( len f) = ( len s) by A1, A2, FINSEQ_1: 93;

      then

       A4: ( dom f) = ( dom s) by FINSEQ_3: 29;

      hereby

        set X = { k where k be Nat : k < (b . c) };

        set ff = ( FlattenSeq f);

        set Y = (ff " { <%( - c), ( 1. L)%>});

        assume c in ( support b);

        then c in ( rng s) by A2, FUNCT_2:def 3;

        then

        consider i be Nat such that

         A5: i in ( dom s) and

         A6: (s . i) = c by FINSEQ_2: 10;

        defpred P[ object, object] means ex n be Nat st n = $1 & $2 = (( Sum ( Card (f | (i -' 1)))) + (1 + n));

        

         A7: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          consider k be Nat such that

           A8: x = k and k < (b . c);

          take (( Sum ( Card (f | (i -' 1)))) + (1 + k));

          thus thesis by A8;

        end;

        consider g be Function such that

         A9: ( dom g) = X and

         A10: for x be object st x in X holds P[x, (g . x)] from CLASSES1:sch 1( A7);

        

         A11: (s /. i) = c by A5, A6, PARTFUN1:def 6;

        now

          let y be object;

          

           A12: ( <%( - c), ( 1. L)%> . 0 ) = ( - c) by POLYNOM5: 38;

          hereby

            assume y in ( rng g);

            then

            consider x be object such that

             A13: x in ( dom g) and

             A14: y = (g . x) by FUNCT_1:def 3;

            consider n be Nat such that

             A15: n = x and

             A16: (g . x) = (( Sum ( Card (f | (i -' 1)))) + (1 + n)) by A9, A10, A13;

            ex k be Nat st x = k & k < (b . c) by A9, A13;

            then

             A17: 1 <= (1 + n) & (1 + n) <= (b . c) by A15, NAT_1: 12, NAT_1: 13;

            

             A18: (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) by A3, A4, A5;

            then ( len (f . i)) = (b . c) by A11, Def9;

            then

             A19: (1 + n) in ( dom (f . i)) by A17, FINSEQ_3: 25;

            then ((f . i) . (1 + n)) = <%( - c), ( 1. L)%> by A11, A18, Def9;

            then

             A20: ((f . i) . (1 + n)) in { <%( - c), ( 1. L)%>} by TARSKI:def 1;

            (( Sum ( Card (f | (i -' 1)))) + (1 + n)) in ( dom ff) & ((f . i) . (1 + n)) = (ff . (( Sum ( Card (f | (i -' 1)))) + (1 + n))) by A4, A5, A19, PRE_POLY: 30;

            hence y in Y by A14, A16, A20, FUNCT_1:def 7;

          end;

          assume

           A21: y in Y;

          then

          reconsider yn = y as Element of NAT ;

          

           A22: (ff . y) in { <%( - c), ( 1. L)%>} by A21, FUNCT_1:def 7;

          y in ( dom ff) by A21, FUNCT_1:def 7;

          then

          consider i1,j be Nat such that

           A23: i1 in ( dom f) and

           A24: j in ( dom (f . i1)) and

           A25: yn = (( Sum ( Card (f | (i1 -' 1)))) + j) and

           A26: ((f . i1) . j) = (ff . yn) by PRE_POLY: 29;

          

           A27: (f . i1) = ( fpoly_mult_root ((s /. i1),(b . (s /. i1)))) by A3, A23;

          then ((f . i1) . j) = <%( - (s /. i1)), ( 1. L)%> by A24, Def9;

          then <%( - c), ( 1. L)%> = <%( - (s /. i1)), ( 1. L)%> by A22, A26, TARSKI:def 1;

          then

           A28: c = (s /. i1) by A12, POLYNOM5: 38, RLVECT_1: 18;

          i1 in ( dom s) & (s /. i1) = (s . i1) by A4, A23, PARTFUN1:def 6;

          then

           A29: i1 = i by A2, A5, A6, A28, FUNCT_1:def 4;

          consider j1 be Nat such that

           A30: j = (j1 + 1) by A24, FINSEQ_3: 24, NAT_1: 6;

          reconsider j1 as Element of NAT by ORDINAL1:def 12;

          ( len (f . i1)) = (b . c) by A27, A28, Def9;

          then j <= (b . c) by A24, FINSEQ_3: 25;

          then j1 < (b . c) by A30, NAT_1: 13;

          then

           A31: j1 in X;

          then ex n be Nat st n = j1 & (g . j1) = (( Sum ( Card (f | (i -' 1)))) + (1 + n)) by A10;

          hence y in ( rng g) by A9, A25, A30, A29, A31, FUNCT_1: 3;

        end;

        then

         A32: ( rng g) = Y by TARSKI: 2;

        g is one-to-one

        proof

          let x1,x2 be object such that

           A33: x1 in ( dom g) & x2 in ( dom g) and

           A34: (g . x1) = (g . x2);

          (ex n1 be Nat st n1 = x1 & (g . x1) = (( Sum ( Card (f | (i -' 1)))) + (1 + n1))) & ex n2 be Nat st n2 = x2 & (g . x2) = (( Sum ( Card (f | (i -' 1)))) + (1 + n2)) by A9, A10, A33;

          hence thesis by A34;

        end;

        then (b . c) = { k where k be Nat : k < (b . c) } & (X,Y) are_equipotent by A9, A32, AXIOMS: 4, WELLORD2:def 4;

        hence ( card (( FlattenSeq f) " { <%( - c), ( 1. L)%>})) = (b . c) by CARD_1:def 2;

      end;

      assume that

       A35: not c in ( support b) and

       A36: ( card (( FlattenSeq f) " { <%( - c), ( 1. L)%>})) <> 0 ;

      consider x be object such that

       A37: x in (( FlattenSeq f) " { <%( - c), ( 1. L)%>}) by A36, CARD_1: 27, XBOOLE_0:def 1;

      

       A38: x in ( dom ( FlattenSeq f)) by A37, FUNCT_1:def 7;

      reconsider x as Element of NAT by A37;

      consider i,j be Nat such that

       A39: i in ( dom f) and

       A40: j in ( dom (f . i)) and x = (( Sum ( Card (f | (i -' 1)))) + j) and

       A41: ((f . i) . j) = (( FlattenSeq f) . x) by A38, PRE_POLY: 29;

      

       A42: (s /. i) = (s . i) & (s . i) in ( rng s) by A4, A39, FUNCT_1: 3, PARTFUN1:def 6;

      (( FlattenSeq f) . x) in { <%( - c), ( 1. L)%>} by A37, FUNCT_1:def 7;

      then

       A43: (( FlattenSeq f) . x) = <%( - c), ( 1. L)%> by TARSKI:def 1;

      (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) by A3, A39;

      then

       A44: ((f . i) . j) = <%( - (s /. i)), ( 1. L)%> by A40, Def9;

      ( <%( - c), ( 1. L)%> . 0 ) = ( - c) by POLYNOM5: 38;

      then c = (s /. i) by A41, A43, A44, POLYNOM5: 38, RLVECT_1: 18;

      hence contradiction by A2, A35, A42, FUNCT_2:def 3;

    end;

    theorem :: UPROOTS:64

    

     Th61: for L be comRing holds for b1,b2 be bag of the carrier of L holds ( poly_with_roots (b1 + b2)) = (( poly_with_roots b1) *' ( poly_with_roots b2))

    proof

      let L be comRing, b1,b2 be bag of the carrier of L;

      set b = (b1 + b2);

      

       A1: ( support b) = (( support b1) \/ ( support b2)) by PRE_POLY: 38;

      consider f2 be FinSequence of (the carrier of ( Polynom-Ring L) * ), s2 be FinSequence of L such that

       A2: ( len f2) = ( card ( support b2)) and

       A3: s2 = ( canFS ( support b2)) and

       A4: for i be Element of NAT st i in ( dom f2) holds (f2 . i) = ( fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i)))) and

       A5: ( poly_with_roots b2) = ( Product ( FlattenSeq f2)) by Def10;

      consider f1 be FinSequence of (the carrier of ( Polynom-Ring L) * ), s1 be FinSequence of L such that

       A6: ( len f1) = ( card ( support b1)) and

       A7: s1 = ( canFS ( support b1)) and

       A8: for i be Element of NAT st i in ( dom f1) holds (f1 . i) = ( fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i)))) and

       A9: ( poly_with_roots b1) = ( Product ( FlattenSeq f1)) by Def10;

      consider f be FinSequence of (the carrier of ( Polynom-Ring L) * ), s be FinSequence of L such that

       A10: ( len f) = ( card ( support b)) and

       A11: s = ( canFS ( support b)) and

       A12: for i be Element of NAT st i in ( dom f) holds (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) and

       A13: ( poly_with_roots (b1 + b2)) = ( Product ( FlattenSeq f)) by Def10;

      set ff = ( FlattenSeq f), ff1 = ( FlattenSeq f1), ff2 = ( FlattenSeq f2);

      

       A14: ( len ff) = ( degree b) by A10, A11, A12, Th59;

      

       A15: ( len ff2) = ( degree b2) by A2, A3, A4, Th59;

      set g = (( FlattenSeq f1) ^ ( FlattenSeq f2));

      ( len g) = (( len ff1) + ( len ff2)) by FINSEQ_1: 22

      .= (( degree b1) + ( degree b2)) by A6, A7, A8, A15, Th59

      .= ( degree b) by Th12;

      then

       A16: ( dom ff) = ( dom g) by A14, FINSEQ_3: 29;

      

       A17: ( len s) = ( card ( support b)) by A11, FINSEQ_1: 93;

      now

        let x be object;

        per cases ;

          suppose x in ( rng ff);

          then

          consider k be Nat such that

           A18: k in ( dom ff) and

           A19: (ff . k) = x by FINSEQ_2: 10;

          consider i,j be Nat such that

           A20: i in ( dom f) and

           A21: j in ( dom (f . i)) and k = (( Sum ( Card (f | (i -' 1)))) + j) and

           A22: ((f . i) . j) = (ff . k) by A18, PRE_POLY: 29;

          (f . i) = ( fpoly_mult_root ((s /. i),(b . (s /. i)))) by A12, A20;

          then

           A23: ((f . i) . j) = <%( - (s /. i)), ( 1. L)%> by A21, Def9;

          i in ( dom s) by A10, A17, A20, FINSEQ_3: 29;

          then (s . i) = (s /. i) & (s . i) in ( rng s) by FUNCT_1: 3, PARTFUN1:def 6;

          then

           A24: (s /. i) in ( support b) by A11, FUNCT_2:def 3;

          

           A25: ( card (g " {x})) = (( card (ff1 " {x})) + ( card (ff2 " {x}))) by FINSEQ_3: 57;

          per cases by A1, A24, XBOOLE_0:def 3;

            suppose

             A26: (s /. i) in ( support b1) & not (s /. i) in ( support b2);

            then

             A27: ( card (ff2 " {x})) = 0 by A2, A3, A4, A19, A22, A23, Th60;

            

            thus ( card ( Coim (ff,x))) = (b . (s /. i)) by A10, A11, A12, A19, A22, A23, A24, Th60

            .= ((b1 . (s /. i)) + (b2 . (s /. i))) by PRE_POLY:def 5

            .= ((b1 . (s /. i)) + 0 qua Nat) by A26, PRE_POLY:def 7

            .= ( card ( Coim (g,x))) by A6, A7, A8, A19, A22, A23, A25, A26, A27, Th60;

          end;

            suppose

             A28: not (s /. i) in ( support b1) & (s /. i) in ( support b2);

            then

             A29: ( card (ff2 " {x})) = (b2 . (s /. i)) by A2, A3, A4, A19, A22, A23, Th60;

            

            thus ( card ( Coim (ff,x))) = (b . (s /. i)) by A10, A11, A12, A19, A22, A23, A24, Th60

            .= ((b1 . (s /. i)) + (b2 . (s /. i))) by PRE_POLY:def 5

            .= ( 0 qua Nat + (b2 . (s /. i))) by A28, PRE_POLY:def 7

            .= ( card ( Coim (g,x))) by A6, A7, A8, A19, A22, A23, A25, A28, A29, Th60;

          end;

            suppose

             A30: (s /. i) in ( support b1) & (s /. i) in ( support b2);

            then

             A31: ( card (ff2 " {x})) = (b2 . (s /. i)) by A2, A3, A4, A19, A22, A23, Th60;

            

            thus ( card ( Coim (ff,x))) = (b . (s /. i)) by A10, A11, A12, A19, A22, A23, A24, Th60

            .= ((b1 . (s /. i)) + (b2 . (s /. i))) by PRE_POLY:def 5

            .= ( card ( Coim (g,x))) by A6, A7, A8, A19, A22, A23, A25, A30, A31, Th60;

          end;

        end;

          suppose

           A32: not x in ( rng ff);

          now

            assume x in ( rng g);

            then

             A33: x in (( rng ff1) \/ ( rng ff2)) by FINSEQ_1: 31;

            per cases by A33, XBOOLE_0:def 3;

              suppose x in ( rng ff1);

              then

              consider k be Nat such that

               A34: k in ( dom ff1) and

               A35: (ff1 . k) = x by FINSEQ_2: 10;

              consider i,j be Nat such that

               A36: i in ( dom f1) and

               A37: j in ( dom (f1 . i)) and k = (( Sum ( Card (f1 | (i -' 1)))) + j) and

               A38: ((f1 . i) . j) = (ff1 . k) by A34, PRE_POLY: 29;

              (f1 . i) = ( fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i)))) by A8, A36;

              then

               A39: ((f1 . i) . j) = <%( - (s1 /. i)), ( 1. L)%> by A37, Def9;

              ( len s1) = ( card ( support b1)) by A7, FINSEQ_1: 93;

              then i in ( dom s1) by A6, A36, FINSEQ_3: 29;

              then (s1 . i) = (s1 /. i) & (s1 . i) in ( rng s1) by FUNCT_1: 3, PARTFUN1:def 6;

              then (s1 /. i) in ( support b1) by A7, FUNCT_2:def 3;

              then

               A40: (s1 /. i) in ( support b) by A1, XBOOLE_0:def 3;

              then (b . (s1 /. i)) <> 0 by PRE_POLY:def 7;

              then

               A41: ( 0 qua Nat + 1) <= (b . (s1 /. i)) by NAT_1: 13;

              (s1 /. i) in ( rng s) by A11, A40, FUNCT_2:def 3;

              then

              consider l be Nat such that

               A42: l in ( dom s) and

               A43: (s . l) = (s1 /. i) by FINSEQ_2: 10;

              

               A44: (s . l) = (s /. l) by A42, PARTFUN1:def 6;

              

               A45: l in ( dom f) by A10, A17, A42, FINSEQ_3: 29;

              then

               A46: (f . l) = ( fpoly_mult_root ((s /. l),(b . (s /. l)))) by A12;

              then ( len (f . l)) = (b . (s /. l)) by Def9;

              then

               A47: 1 in ( dom (f . l)) by A43, A44, A41, FINSEQ_3: 25;

              then (( Sum ( Card (f | (l -' 1)))) + 1) in ( dom ff) & ((f . l) . 1) = (ff . (( Sum ( Card (f | (l -' 1)))) + 1)) by A45, PRE_POLY: 30;

              then ((f . l) . 1) in ( rng ff) by FUNCT_1: 3;

              hence contradiction by A32, A35, A38, A39, A43, A46, A44, A47, Def9;

            end;

              suppose x in ( rng ff2);

              then

              consider k be Nat such that

               A48: k in ( dom ff2) and

               A49: (ff2 . k) = x by FINSEQ_2: 10;

              consider i,j be Nat such that

               A50: i in ( dom f2) and

               A51: j in ( dom (f2 . i)) and k = (( Sum ( Card (f2 | (i -' 1)))) + j) and

               A52: ((f2 . i) . j) = (ff2 . k) by A48, PRE_POLY: 29;

              (f2 . i) = ( fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i)))) by A4, A50;

              then

               A53: ((f2 . i) . j) = <%( - (s2 /. i)), ( 1. L)%> by A51, Def9;

              ( len s2) = ( card ( support b2)) by A3, FINSEQ_1: 93;

              then i in ( dom s2) by A2, A50, FINSEQ_3: 29;

              then (s2 . i) = (s2 /. i) & (s2 . i) in ( rng s2) by FUNCT_1: 3, PARTFUN1:def 6;

              then (s2 /. i) in ( support b2) by A3, FUNCT_2:def 3;

              then

               A54: (s2 /. i) in ( support b) by A1, XBOOLE_0:def 3;

              then (b . (s2 /. i)) <> 0 by PRE_POLY:def 7;

              then

               A55: ( 0 qua Nat + 1) <= (b . (s2 /. i)) by NAT_1: 13;

              (s2 /. i) in ( rng s) by A11, A54, FUNCT_2:def 3;

              then

              consider l be Nat such that

               A56: l in ( dom s) and

               A57: (s . l) = (s2 /. i) by FINSEQ_2: 10;

              

               A58: (s . l) = (s /. l) by A56, PARTFUN1:def 6;

              

               A59: l in ( dom f) by A10, A17, A56, FINSEQ_3: 29;

              then

               A60: (f . l) = ( fpoly_mult_root ((s /. l),(b . (s /. l)))) by A12;

              then ( len (f . l)) = (b . (s /. l)) by Def9;

              then

               A61: 1 in ( dom (f . l)) by A57, A58, A55, FINSEQ_3: 25;

              then (( Sum ( Card (f | (l -' 1)))) + 1) in ( dom ff) & ((f . l) . 1) = (ff . (( Sum ( Card (f | (l -' 1)))) + 1)) by A59, PRE_POLY: 30;

              then ((f . l) . 1) in ( rng ff) by FUNCT_1: 3;

              hence contradiction by A32, A49, A52, A53, A57, A60, A58, A61, Def9;

            end;

          end;

          then (g " {x}) = {} by FUNCT_1: 72;

          hence ( card ( Coim (ff,x))) = ( card ( Coim (g,x))) by A32, FUNCT_1: 72;

        end;

      end;

      then (ff,g) are_fiberwise_equipotent by CLASSES1:def 10;

      then ex p be Permutation of ( dom ( FlattenSeq f)) st ( FlattenSeq f) = ((( FlattenSeq f1) ^ ( FlattenSeq f2)) * p) by A16, RFINSEQ: 4;

      

      hence ( poly_with_roots (b1 + b2)) = ( Product (( FlattenSeq f1) ^ ( FlattenSeq f2))) by A13, A16, Th13

      .= (( Product ( FlattenSeq f1)) * ( Product ( FlattenSeq f2))) by GROUP_4: 5

      .= (( poly_with_roots b1) *' ( poly_with_roots b2)) by A9, A5, POLYNOM3:def 10;

    end;

    theorem :: UPROOTS:65

    for L be algebraic-closed domRing, p be non-zero Polynomial of L st (p . (( len p) -' 1)) = ( 1. L) holds p = ( poly_with_roots ( BRoots p))

    proof

      let L be algebraic-closed domRing, p be non-zero Polynomial of L;

      assume

       A1: (p . (( len p) -' 1)) = ( 1. L);

      defpred P[ Nat] means for p be non-zero Polynomial of L st ( len p) = $1 & $1 >= 1 & (p . (( len p) -' 1)) = ( 1. L) holds p = ( poly_with_roots ( BRoots p));

      ( len p) > 0 by Th14;

      then

       A2: ( len p) >= ( 0 qua Nat + 1) by NAT_1: 13;

      

       A3: for n be Nat st n >= 1 & P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A4: n >= 1 and

         A5: P[n];

        let p be non-zero Polynomial of L such that

         A6: ( len p) = (n + 1) and (n + 1) >= 1 and

         A7: (p . (( len p) -' 1)) = ( 1. L);

        (n + 1) > 1 by A4, NAT_1: 13;

        then p is with_roots by A6, POLYNOM5:def 9;

        then

        consider x be Element of L such that

         A8: x is_a_root_of p;

        set r = <%( - x), ( 1. L)%>;

        set q = ( poly_quotient (p,x));

        

         A9: p = (r *' q) by A8, Th47;

        then

        reconsider q as non-zero Polynomial of L by Th31;

        

         A10: ( len r) = 2 by POLYNOM5: 40;

        then

         A11: (r . (( len r) -' 1)) <> ( 0. L) by Th15;

        ( len q) > 0 by Th14;

        then (q . (( len q) -' 1)) <> ( 0. L) by Th15;

        then ((r . (( len r) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) by A11, VECTSP_2:def 1;

        then

         A12: ( len p) = ((( len q) + (1 + 1)) - 1) by A9, A10, POLYNOM4: 10;

        (q . (( len q) -' 1)) = ( 1. L) by A7, A9, Th38;

        then

         A13: q = ( poly_with_roots ( BRoots q)) by A4, A5, A6, A12;

        

         A14: ( poly_with_roots (( {x},1) -bag )) = <%( - x), ( 1. L)%> by Th58;

        ( BRoots r) = (( {x},1) -bag ) by Th51;

        then ( BRoots p) = ((( {x},1) -bag ) + ( BRoots q)) by A9, Th53;

        hence thesis by A9, A13, A14, Th61;

      end;

      

       A15: P[1]

      proof

        let p be non-zero Polynomial of L such that

         A16: ( len p) = 1 and 1 >= 1 and

         A17: (p . (( len p) -' 1)) = ( 1. L);

        ( degree ( BRoots p)) = 0 by A16, Th54;

        then

         A18: ( BRoots p) = ( EmptyBag the carrier of L) by Th9;

        (( len p) -' 1) = 0 by A16, XREAL_1: 232;

        

        hence p = <%( 1. L)%> by A16, A17, ALGSEQ_1:def 5

        .= ( poly_with_roots ( BRoots p)) by A18, Th57;

      end;

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A15, A3);

      hence thesis by A1, A2;

    end;

    theorem :: UPROOTS:66

    for L be comRing, s be non empty finite Subset of L, f be FinSequence of ( Polynom-Ring L) st ( len f) = ( card s) & for i be Element of NAT , c be Element of L st i in ( dom f) & c = (( canFS s) . i) holds (f . i) = <%( - c), ( 1. L)%> holds ( poly_with_roots ((s,1) -bag )) = ( Product f)

    proof

      let L be comRing;

      set cL = the carrier of L;

      set cPRL = the carrier of ( Polynom-Ring L);

      let s be non empty finite Subset of cL, f be FinSequence of cPRL such that

       A1: ( len f) = ( card s) and

       A2: for i be Element of NAT , c be Element of cL st i in ( dom f) & c = (( canFS s) . i) holds (f . i) = <%( - c), ( 1. L)%>;

      set cs = ( canFS s);

      

       A3: ( rng cs) = s by FUNCT_2:def 3;

      defpred P[ Nat] means ex t be finite Subset of cL, g be FinSequence of cPRL st t = ( rng (cs | ( Seg $1))) & g = (f | ( Seg $1)) & ( poly_with_roots ((t,1) -bag )) = ( Product g);

      

       A4: ( len cs) = ( card s) by FINSEQ_1: 93;

      then

       A5: ( dom f) = ( dom cs) by A1, FINSEQ_3: 29;

      

       A6: for j be Element of NAT st 1 <= j & j < ( len f) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT such that

         A7: 1 <= j and

         A8: j < ( len f);

        reconsider g1 = (f | ( Seg (j + 1))) as FinSequence of cPRL by FINSEQ_1: 18;

        

         A9: (j + 1) <= ( len f) by A8, NAT_1: 13;

        then ex l be Nat st ( len f) = ((j + 1) + l) by NAT_1: 10;

        then

         A10: ( len g1) = (j + 1) by FINSEQ_3: 53;

        1 <= (j + 1) by A7, NAT_1: 13;

        then

         A11: (j + 1) in ( dom cs) by A1, A4, A9, FINSEQ_3: 25;

        then (cs . (j + 1)) in s by FINSEQ_2: 11;

        then

        reconsider csj1 = (cs . (j + 1)) as Element of cL;

        

         A12: (g1 . (j + 1)) = (f . (j + 1)) by FINSEQ_1: 4, FUNCT_1: 49

        .= <%( - csj1), ( 1. L)%> by A2, A5, A11;

        reconsider csja1 = (cs | ( Seg (j + 1))) as FinSequence of s by FINSEQ_1: 18;

        reconsider csja = (cs | ( Seg j)) as FinSequence of s by FINSEQ_1: 18;

        given t be finite Subset of cL, g be FinSequence of cPRL such that

         A13: t = ( rng (cs | ( Seg j))) and

         A14: g = (f | ( Seg j)) and

         A15: ( poly_with_roots ((t,1) -bag )) = ( Product g);

        j <= (j + 1) by NAT_1: 12;

        then ( Seg j) c= ( Seg (j + 1)) by FINSEQ_1: 5;

        then g = (g1 | ( Seg j)) by A14, RELAT_1: 74;

        then

         A16: g1 = (g ^ <* <%( - csj1), ( 1. L)%>*>) by A10, A12, FINSEQ_3: 55;

        reconsider pt = ( poly_with_roots ((t,1) -bag )) as Polynomial of L;

        set t1 = ( rng csja1);

        ( Seg (j + 1)) = (( Seg j) \/ {(j + 1)}) by FINSEQ_1: 9;

        then

         A17: csja1 = (csja \/ (cs | {(j + 1)})) by RELAT_1: 78;

        (cs | {(j + 1)}) = ((j + 1) .--> csj1) by A11, FUNCT_7: 6;

        then ( rng (cs | {(j + 1)})) = {csj1} by FUNCOP_1: 8;

        then

         A18: t1 = (t \/ {csj1}) by A13, A17, RELAT_1: 12;

        reconsider epj1 = <%( - csj1), ( 1. L)%> as Element of cPRL by POLYNOM3:def 10;

        reconsider pj1 = ( poly_with_roots (( {csj1},1) -bag )) as Polynomial of L;

        

         A19: pj1 = epj1 by Th58;

        reconsider t1 as finite Subset of cL by A18;

        take t1, g1;

        thus t1 = ( rng (cs | ( Seg (j + 1)))) & g1 = (f | ( Seg (j + 1)));

        t misses {csj1}

        proof

          assume not thesis;

          then (t /\ {csj1}) <> {} by XBOOLE_0:def 7;

          then

          consider x be object such that

           A20: x in (t /\ {csj1}) by XBOOLE_0:def 1;

          x in {csj1} by A20, XBOOLE_0:def 4;

          then

           A21: x = csj1 by TARSKI:def 1;

          x in t by A20, XBOOLE_0:def 4;

          then

          consider i be object such that

           A22: i in ( dom (cs | ( Seg j))) and

           A23: x = ((cs | ( Seg j)) . i) by A13, FUNCT_1:def 3;

          

           A24: i in ( Seg j) by A22, RELAT_1: 57;

          reconsider i as Element of NAT by A22;

          

           A25: 1 <= i by A24, FINSEQ_1: 1;

          i <= j by A24, FINSEQ_1: 1;

          then

           A26: i < (j + 1) by NAT_1: 13;

          x = (cs . i) by A22, A23, FUNCT_1: 47;

          hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5: 7;

        end;

        then ((t1,1) -bag ) = (((t,1) -bag ) + (( {csj1},1) -bag )) by A18, Th7;

        

        hence ( poly_with_roots ((t1,1) -bag )) = (pt *' pj1) by Th61

        .= (( Product g) * epj1) by A15, A19, POLYNOM3:def 10

        .= ( Product g1) by A16, GROUP_4: 6;

      end;

      (f | ( Seg ( len f))) is FinSequence by FINSEQ_1: 18;

      then

       A27: (cs | ( Seg ( len f))) is FinSequence & (f | ( Seg ( len f))) = f by FINSEQ_1: 18, FINSEQ_2: 20;

      

       A28: ( 0 qua Nat + 1) <= ( len f) by A1, NAT_1: 13;

      

       A29: P[1]

      proof

        1 in ( dom cs) by A1, A4, A28, FINSEQ_3: 25;

        then

        reconsider cs1 = (cs . 1) as Element of s by FINSEQ_2: 11;

        reconsider g = (f | ( Seg 1)) as FinSequence of cPRL by FINSEQ_1: 18;

        reconsider cs1a = (cs | ( Seg 1)) as FinSequence of s by FINSEQ_1: 18;

        

         A30: cs1 in cL;

        

         A31: 1 in ( Seg 1) by FINSEQ_1: 1;

        then

         A32: (cs1a . 1) = cs1 by FUNCT_1: 49;

        reconsider cs1 = (cs . 1) as Element of cL by A30;

        reconsider t = {cs1} as finite Subset of cL;

        take t, g;

        consider s1 be Element of s such that

         A33: cs1a = <*s1*> by A1, A4, A28, TREES_9: 34;

        (cs1a . 1) = s1 by A33, FINSEQ_1: 40;

        hence t = ( rng (cs | ( Seg 1))) & g = (f | ( Seg 1)) by A33, A32, FINSEQ_1: 39;

        consider p1 be Element of cPRL such that

         A34: g = <*p1*> by A28, TREES_9: 34;

        

         A35: (g . 1) = p1 & ( Product g) = p1 by A34, FINSEQ_1: 40, FINSOP_1: 11;

        

         A36: 1 in ( dom f) by A28, FINSEQ_3: 25;

        then

        reconsider f1 = (f . 1) as Element of cPRL by FINSEQ_2: 11;

        

         A37: (g . 1) = f1 by A31, FUNCT_1: 49;

        f1 = <%( - cs1), ( 1. L)%> by A2, A36;

        hence thesis by A37, A35, Th58;

      end;

      for i be Element of NAT st 1 <= i & i <= ( len f) holds P[i] from INT_1:sch 7( A29, A6);

      then ex t be finite Subset of cL, g be FinSequence of cPRL st t = ( rng (cs | ( Seg ( len f)))) & g = (f | ( Seg ( len f))) & ( poly_with_roots ((t,1) -bag )) = ( Product g) by A28;

      hence thesis by A1, A4, A27, A3, FINSEQ_2: 20;

    end;

    theorem :: UPROOTS:67

    for L be non trivial comRing, s be non empty finite Subset of L, x be Element of L, f be FinSequence of L st ( len f) = ( card s) & for i be Element of NAT , c be Element of L st i in ( dom f) & c = (( canFS s) . i) holds (f . i) = ( eval ( <%( - c), ( 1. L)%>,x)) holds ( eval (( poly_with_roots ((s,1) -bag )),x)) = ( Product f)

    proof

      let L be non trivial comRing;

      set cL = the carrier of L;

      let s be non empty finite Subset of cL, x be Element of cL, f be FinSequence of L such that

       A1: ( len f) = ( card s) and

       A2: for i be Element of NAT , c be Element of cL st i in ( dom f) & c = (( canFS s) . i) holds (f . i) = ( eval ( <%( - c), ( 1. L)%>,x));

      set cs = ( canFS s);

      

       A3: ( rng cs) = s by FUNCT_2:def 3;

      defpred P[ Nat] means ex t be finite Subset of cL, g be FinSequence of cL st t = ( rng (cs | ( Seg $1))) & g = (f | ( Seg $1)) & ( eval (( poly_with_roots ((t,1) -bag )),x)) = ( Product g);

      

       A4: ( len cs) = ( card s) by FINSEQ_1: 93;

      then

       A5: ( dom f) = ( dom cs) by A1, FINSEQ_3: 29;

      

       A6: for j be Element of NAT st 1 <= j & j < ( len f) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT such that

         A7: 1 <= j and

         A8: j < ( len f);

        reconsider g1 = (f | ( Seg (j + 1))) as FinSequence of cL by FINSEQ_1: 18;

        

         A9: (j + 1) <= ( len f) by A8, NAT_1: 13;

        then ex l be Nat st ( len f) = ((j + 1) + l) by NAT_1: 10;

        then

         A10: ( len g1) = (j + 1) by FINSEQ_3: 53;

        1 <= (j + 1) by A7, NAT_1: 13;

        then

         A11: (j + 1) in ( dom cs) by A1, A4, A9, FINSEQ_3: 25;

        then (cs . (j + 1)) in s by FINSEQ_2: 11;

        then

        reconsider csj1 = (cs . (j + 1)) as Element of cL;

        

         A12: (g1 . (j + 1)) = (f . (j + 1)) by FINSEQ_1: 4, FUNCT_1: 49

        .= ( eval ( <%( - csj1), ( 1. L)%>,x)) by A2, A5, A11;

        reconsider csja1 = (cs | ( Seg (j + 1))) as FinSequence of s by FINSEQ_1: 18;

        reconsider csja = (cs | ( Seg j)) as FinSequence of s by FINSEQ_1: 18;

        given t be finite Subset of cL, g be FinSequence of cL such that

         A13: t = ( rng (cs | ( Seg j))) and

         A14: g = (f | ( Seg j)) and

         A15: ( eval (( poly_with_roots ((t,1) -bag )),x)) = ( Product g);

        j <= (j + 1) by NAT_1: 12;

        then ( Seg j) c= ( Seg (j + 1)) by FINSEQ_1: 5;

        then g = (g1 | ( Seg j)) by A14, RELAT_1: 74;

        then

         A16: g1 = (g ^ <*( eval ( <%( - csj1), ( 1. L)%>,x))*>) by A10, A12, FINSEQ_3: 55;

        reconsider pt = ( poly_with_roots ((t,1) -bag )) as Polynomial of L;

        set t1 = ( rng csja1);

        ( Seg (j + 1)) = (( Seg j) \/ {(j + 1)}) by FINSEQ_1: 9;

        then

         A17: csja1 = (csja \/ (cs | {(j + 1)})) by RELAT_1: 78;

        (cs | {(j + 1)}) = ((j + 1) .--> csj1) by A11, FUNCT_7: 6;

        then ( rng (cs | {(j + 1)})) = {csj1} by FUNCOP_1: 8;

        then

         A18: t1 = (t \/ {csj1}) by A13, A17, RELAT_1: 12;

        then

        reconsider t1 as finite Subset of cL;

        take t1, g1;

        thus t1 = ( rng (cs | ( Seg (j + 1)))) & g1 = (f | ( Seg (j + 1)));

        reconsider pj1 = ( poly_with_roots (( {csj1},1) -bag )) as Polynomial of L;

        

         A19: pj1 = <%( - csj1), ( 1. L)%> by Th58;

        t misses {csj1}

        proof

          assume not thesis;

          then (t /\ {csj1}) <> {} by XBOOLE_0:def 7;

          then

          consider x be object such that

           A20: x in (t /\ {csj1}) by XBOOLE_0:def 1;

          x in {csj1} by A20, XBOOLE_0:def 4;

          then

           A21: x = csj1 by TARSKI:def 1;

          x in t by A20, XBOOLE_0:def 4;

          then

          consider i be object such that

           A22: i in ( dom (cs | ( Seg j))) and

           A23: x = ((cs | ( Seg j)) . i) by A13, FUNCT_1:def 3;

          

           A24: i in ( Seg j) by A22, RELAT_1: 57;

          reconsider i as Element of NAT by A22;

          

           A25: 1 <= i by A24, FINSEQ_1: 1;

          i <= j by A24, FINSEQ_1: 1;

          then

           A26: i < (j + 1) by NAT_1: 13;

          x = (cs . i) by A22, A23, FUNCT_1: 47;

          hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5: 7;

        end;

        then ((t1,1) -bag ) = (((t,1) -bag ) + (( {csj1},1) -bag )) by A18, Th7;

        then ( poly_with_roots ((t1,1) -bag )) = (pt *' pj1) by Th61;

        

        hence ( eval (( poly_with_roots ((t1,1) -bag )),x)) = (( Product g) * ( eval (pj1,x))) by A15, POLYNOM4: 24

        .= ( Product g1) by A16, A19, GROUP_4: 6;

      end;

      (f | ( Seg ( len f))) is FinSequence by FINSEQ_1: 18;

      then

       A27: (cs | ( Seg ( len f))) is FinSequence & (f | ( Seg ( len f))) = f by FINSEQ_1: 18, FINSEQ_2: 20;

      

       A28: ( 0 qua Nat + 1) <= ( len f) by A1, NAT_1: 13;

      

       A29: P[1]

      proof

        1 in ( dom cs) by A1, A4, A28, FINSEQ_3: 25;

        then

        reconsider cs1 = (cs . 1) as Element of s by FINSEQ_2: 11;

        reconsider g = (f | ( Seg 1)) as FinSequence of cL by FINSEQ_1: 18;

        reconsider cs1a = (cs | ( Seg 1)) as FinSequence of s by FINSEQ_1: 18;

        

         A30: cs1 in cL;

        

         A31: 1 in ( Seg 1) by FINSEQ_1: 1;

        then

         A32: (cs1a . 1) = cs1 by FUNCT_1: 49;

        reconsider cs1 = (cs . 1) as Element of cL by A30;

        reconsider t = {cs1} as finite Subset of cL;

        take t, g;

        consider s1 be Element of s such that

         A33: cs1a = <*s1*> by A1, A4, A28, TREES_9: 34;

        (cs1a . 1) = s1 by A33, FINSEQ_1: 40;

        hence t = ( rng (cs | ( Seg 1))) & g = (f | ( Seg 1)) by A33, A32, FINSEQ_1: 39;

        consider p1 be Element of cL such that

         A34: g = <*p1*> by A28, TREES_9: 34;

        

         A35: (g . 1) = p1 & ( Product g) = p1 by A34, FINSEQ_1: 40, FINSOP_1: 11;

        

         A36: 1 in ( dom f) by A28, FINSEQ_3: 25;

        then

        reconsider f1 = (f . 1) as Element of cL by FINSEQ_2: 11;

        

         A37: (g . 1) = f1 by A31, FUNCT_1: 49;

        f1 = ( eval ( <%( - cs1), ( 1. L)%>,x)) by A2, A36;

        hence thesis by A37, A35, Th58;

      end;

      for i be Element of NAT st 1 <= i & i <= ( len f) holds P[i] from INT_1:sch 7( A29, A6);

      then ex t be finite Subset of cL, g be FinSequence of cL st t = ( rng (cs | ( Seg ( len f)))) & g = (f | ( Seg ( len f))) & ( eval (( poly_with_roots ((t,1) -bag )),x)) = ( Product g) by A28;

      hence thesis by A1, A4, A27, A3, FINSEQ_2: 20;

    end;