ratfunc1.miz



    begin

    theorem :: RATFUNC1:1

    

     Th1: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for a be Element of L holds for p,q be FinSequence of L st ( len p) = ( len q) & for i be Element of NAT st i in ( dom p) holds (q /. i) = (a * (p /. i)) holds ( Sum q) = (a * ( Sum p))

    proof

      let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, a be Element of L, p,q be FinSequence of L;

      assume

       A1: ( len p) = ( len q) & for i be Element of NAT st i in ( dom p) holds (q /. i) = (a * (p /. i));

      consider fq be sequence of the carrier of L such that

       A2: ( Sum q) = (fq . ( len q)) and

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

       A4: for j be Nat, v be Element of L st j < ( len q) & v = (q . (j + 1)) holds (fq . (j + 1)) = ((fq . j) + v) by RLVECT_1:def 12;

      consider fp be sequence of the carrier of L such that

       A5: ( Sum p) = (fp . ( len p)) and

       A6: (fp . 0 ) = ( 0. L) and

       A7: for j be Nat, v be Element of L st j < ( len p) & v = (p . (j + 1)) holds (fp . (j + 1)) = ((fp . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means (fq . $1) = (a * (fp . $1));

      

       A8: P[ 0 ] by A6, A3;

      

       A9: for j be Element of NAT st 0 <= j & j < ( len p) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT ;

        assume

         A10: 0 <= j & j < ( len p);

        assume

         A11: P[j];

        

         A12: 1 <= (j + 1) by NAT_1: 11;

        

         A13: (j + 1) <= ( len p) by A10, NAT_1: 13;

        then (j + 1) in ( Seg ( len q)) by A12, A1;

        then

         A14: (j + 1) in ( dom q) by FINSEQ_1:def 3;

        (j + 1) in ( Seg ( len p)) by A12, A13;

        then

         A15: (j + 1) in ( dom p) by FINSEQ_1:def 3;

        set vq = (q /. (j + 1)), vp = (p /. (j + 1));

        

         A16: vq = (q . (j + 1)) by A14, PARTFUN1:def 6;

        

         A17: vp = (p . (j + 1)) by A15, PARTFUN1:def 6;

        (fq . (j + 1)) = ((a * (fp . j)) + vq) by A11, A1, A16, A10, A4

        .= ((a * (fp . j)) + (a * vp)) by A1, A15

        .= (a * ((fp . j) + vp)) by VECTSP_1:def 2

        .= (a * (fp . (j + 1))) by A17, A10, A7;

        hence P[(j + 1)];

      end;

      for j be Element of NAT st 0 <= j & j <= ( len p) holds P[j] from INT_1:sch 7( A8, A9);

      hence thesis by A1, A5, A2;

    end;

    theorem :: RATFUNC1:2

    

     Th2: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for f be FinSequence of L holds for i,j be Element of NAT st i in ( dom f) & j = (i - 1) holds ( Ins (( Del (f,i)),j,(f /. i))) = f

    proof

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

      let f be FinSequence of L;

      let i,j be Element of NAT ;

      set g = ( Ins (( Del (f,i)),j,(f /. i)));

      assume

       A1: i in ( dom f) & j = (i - 1);

      then

      consider n be Nat such that

       A2: ( len f) = (n + 1) & ( len ( Del (f,i))) = n by FINSEQ_3: 104;

      ( dom f) = ( Seg (n + 1)) by A2, FINSEQ_1:def 3;

      then

      consider ii be Nat such that

       A3: i = ii & 1 <= ii & ii <= (n + 1) by A1;

      (i - 1) < (i - 0 ) by XREAL_1: 15;

      then j < (n + 1) by A1, A3, XXREAL_0: 2;

      then

       A4: j <= n by NAT_1: 13;

      

       A5: ( len g) = (( len ( Del (f,i))) + 1) by FINSEQ_5: 69;

      now

        let k be Nat;

        assume

         A6: 1 <= k & k <= ( len g);

        now

          per cases by XXREAL_0: 1;

            suppose

             A8: k < i;

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

            then ((k + 1) - 1) <= (i - 1) by XREAL_1: 9;

            then 1 <= k & k <= ( len (( Del (f,i)) | j)) by A6, A1, A4, A2, FINSEQ_1: 59;

            then k in ( Seg ( len (( Del (f,i)) | j)));

            then k in ( dom (( Del (f,i)) | j)) by FINSEQ_1:def 3;

            

            hence (g . k) = (( Del (f,i)) . k) by FINSEQ_5: 72

            .= (f . k) by A8, FINSEQ_3: 110;

          end;

            suppose

             A11: k = i;

            

             S: (f /. i) = (f . i) by A1, PARTFUN1:def 6;

            k = (j + 1) by A1, A11;

            then (g . k) = (f . i) by S, A2, A4, FINSEQ_5: 73;

            hence (g . k) = (f . k) by A11;

          end;

            suppose

             A13: k > i;

            then

            reconsider k1 = (k - 1) as Element of NAT by A3, INT_1: 5, XXREAL_0: 2;

            

             A14: (k - 1) <= ((n + 1) - 1) by A6, A2, A5, XREAL_1: 9;

            i < (k1 + 1) by A13;

            then

             A16: (j + 1) <= (k - 1) by A1, NAT_1: 13;

            

            then (g . (k1 + 1)) = (( Del (f,i)) . k1) by A14, A2, FINSEQ_5: 74

            .= (f . (k1 + 1)) by A16, A14, A2, A1, FINSEQ_3: 111;

            hence (f . k) = (g . k);

          end;

        end;

        hence (g . k) = (f . k);

      end;

      hence thesis by A2, FINSEQ_5: 69;

    end;

    theorem :: RATFUNC1:3

    

     Th3: for L be add-associative right_zeroed right_complementable associative unital right-distributive commutative non empty doubleLoopStr holds for f be FinSequence of L holds for i be Element of NAT st i in ( dom f) holds ( Product f) = ((f /. i) * ( Product ( Del (f,i))))

    proof

      let L be add-associative right_zeroed right_complementable associative unital right-distributive commutative non empty doubleLoopStr;

      let f be FinSequence of L;

      let i be Element of NAT ;

      assume

       A1: i in ( dom f);

      then i in ( Seg ( len f)) by FINSEQ_1:def 3;

      then

      consider ii be Nat such that

       A2: ii = i & 1 <= ii & ii <= ( len f);

      reconsider j = (i - 1) as Element of NAT by A2, INT_1: 5;

      set g = ( Del (f,i));

      

      thus ( Product f) = ( Product ( Ins (g,j,(f /. i)))) by A1, Th2

      .= (( Product ((g | j) ^ <*(f /. i)*>)) * ( Product (g /^ j))) by GROUP_4: 5

      .= ((( Product (g | j)) * (f /. i)) * ( Product (g /^ j))) by GROUP_4: 6

      .= ((f /. i) * (( Product (g | j)) * ( Product (g /^ j)))) by GROUP_1:def 3

      .= ((f /. i) * ( Product ((g | j) ^ (g /^ j)))) by GROUP_4: 5

      .= ((f /. i) * ( Product g)) by RFINSEQ: 8;

    end;

    registration

      let L be add-associative right_zeroed right_complementable well-unital associative left-distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let x,y be non zero Element of L;

      cluster (x / y) -> non zero;

      coherence

      proof

        x <> ( 0. L) & y <> ( 0. L);

        then ((y " ) * y) = ( 1. L) by VECTSP_1:def 10;

        then (y " ) <> ( 0. L);

        hence (x / y) <> ( 0. L) by VECTSP_2:def 1;

      end;

    end

    registration

      cluster domRing-like -> almost_left_cancelable for add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      coherence

      proof

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

        assume

         A1: L is domRing-like;

        let x be Element of L;

        assume

         A2: x <> ( 0. L);

        let y,z be Element of L;

        assume (x * y) = (x * z);

        then ((x * y) - (x * z)) = ( 0. L) by RLVECT_1: 15;

        then (x * (y - z)) = ( 0. L) by VECTSP_1: 11;

        then (y - z) = ( 0. L) by A2, A1;

        hence y = z by RLVECT_1: 21;

      end;

      cluster domRing-like -> almost_right_cancelable for add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      coherence

      proof

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

        assume

         A3: L is domRing-like;

        let x be Element of L;

        assume

         A4: x <> ( 0. L);

        let y,z be Element of L;

        assume (y * x) = (z * x);

        then ((y * x) - (z * x)) = ( 0. L) by RLVECT_1: 15;

        then ((y - z) * x) = ( 0. L) by VECTSP_1: 13;

        then (y - z) = ( 0. L) by A4, A3;

        hence y = z by RLVECT_1: 21;

      end;

    end

    registration

      let x,y be Integer;

      cluster ( max (x,y)) -> integer;

      coherence by XXREAL_0: 16;

      cluster ( min (x,y)) -> integer;

      coherence by XXREAL_0: 15;

    end

    theorem :: RATFUNC1:4

    

     Th4: for x,y,z be Integer holds ( max ((x + y),(x + z))) = (x + ( max (y,z)))

    proof

      let x,y,z be Integer;

      per cases ;

        suppose

         A1: y <= z;

        then (x + y) <= (x + z) by XREAL_1: 6;

        

        hence ( max ((x + y),(x + z))) = (x + z) by XXREAL_0:def 10

        .= (x + ( max (y,z))) by A1, XXREAL_0:def 10;

      end;

        suppose

         A2: y > z;

        then (x + y) > (x + z) by XREAL_1: 8;

        

        hence ( max ((x + y),(x + z))) = (x + y) by XXREAL_0:def 10

        .= (x + ( max (y,z))) by A2, XXREAL_0:def 10;

      end;

    end;

    begin

    notation

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      antonym p is zero for p is non-zero;

    end

    definition

      ::$Canceled

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      :: RATFUNC1:def2

      attr p is constant means ( deg p) <= 0 ;

    end

    registration

      let L be non empty ZeroStr;

      cluster zero for Polynomial of L;

      existence

      proof

        take ( 0_. L);

        thus thesis;

      end;

    end

    registration

      let L be non trivial ZeroStr;

      cluster non zero for Polynomial of L;

      existence

      proof

        now

          assume

           A1: not (ex x be Element of the carrier of L st x <> ( 0. L));

          now

            let x,y be Element of the carrier of L;

            

            thus y = ( 0. L) by A1

            .= x by A1;

          end;

          hence contradiction by STRUCT_0:def 10;

        end;

        then

        consider x be Element of the carrier of L such that

         A2: x <> ( 0. L);

        set p = (( 0_. L) +* ( 0 ,x));

        ex n be Nat st for i be Nat st i >= n holds (p . i) = ( 0. L)

        proof

          take 1;

          now

            let i be Nat;

            assume

             A3: i >= 1;

            

             A4: i in NAT by ORDINAL1:def 12;

            

            thus (p . i) = (( 0_. L) . i) by A3, FUNCT_7: 32

            .= ( 0. L) by A4, FUNCOP_1: 7;

          end;

          hence thesis;

        end;

        then

        reconsider p as Polynomial of L by ALGSEQ_1:def 1;

        take p;

        now

          let i be Nat;

          assume i < 1;

          then

           A5: i = 0 by NAT_1: 14;

          i in NAT by ORDINAL1:def 12;

          then 0 in ( dom ( 0_. L)) by A5, FUNCT_2:def 1;

          hence (p . i) <> ( 0. L) by A2, A5, FUNCT_7: 31;

        end;

        then ( len p) <> 0 by ALGSEQ_1: 9;

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

      end;

    end

    registration

      let L be non empty ZeroStr;

      cluster ( 0_. L) -> zero constant;

      coherence by HURWITZ: 20;

    end

    registration

      let L be non degenerated multLoopStr_0;

      cluster ( 1_. L) -> non zero;

      coherence

      proof

        

         A1: (( 1_. L) . 0 ) = ( 1. L) by POLYNOM3: 30;

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

        hence thesis by A1;

      end;

    end

    registration

      let L be non empty multLoopStr_0;

      cluster ( 1_. L) -> constant;

      coherence

      proof

        set p = ( 1_. L);

        now

          per cases ;

            suppose

             A1: ( 0. L) = ( 1. L);

            

             A2: ( dom p) = NAT by FUNCT_2:def 1

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

            now

              let x be object;

              assume x in ( dom p);

              then

              reconsider xx = x as Element of NAT ;

              

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

              xx = 0 or xx <> 0 ;

              hence (p . x) = (( 0_. L) . x) by A1, A3, POLYNOM3: 30;

            end;

            hence thesis by A2, FUNCT_1: 2;

          end;

            suppose

             A4: ( 0. L) <> ( 1. L);

            now

              let i be Nat;

              assume

               A5: i >= 1;

              

               A6: i in NAT by ORDINAL1:def 12;

              

              thus (p . i) = (( 0_. L) . i) by A5, FUNCT_7: 32

              .= ( 0. L) by A6, FUNCOP_1: 7;

            end;

            then

             A7: 1 is_at_least_length_of p by ALGSEQ_1:def 2;

            now

              let m be Nat;

              assume

               A8: m is_at_least_length_of p;

              now

                assume m < 1;

                then m < (1 + 0 );

                then m <= 0 by NAT_1: 13;

                then

                 A9: (p . 0 ) = ( 0. L) by A8, ALGSEQ_1:def 2;

                ( dom ( 0_. L)) = NAT by FUNCOP_1: 13;

                hence contradiction by A4, A9, FUNCT_7: 31;

              end;

              hence 1 <= m;

            end;

            then ( len p) = 1 by A7, ALGSEQ_1:def 3;

            then ( deg p) = 0 ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let L be non degenerated multLoopStr_0;

      cluster non zero constant for Polynomial of L;

      existence

      proof

        take ( 1_. L);

        thus thesis;

      end;

    end

    registration

      let L be non empty ZeroStr;

      cluster zero -> constant for Polynomial of L;

      coherence ;

    end

    registration

      let L be non empty ZeroStr;

      cluster non constant -> non zero for Polynomial of L;

      coherence ;

    end

    registration

      let L be non trivial ZeroStr;

      cluster non constant for Polynomial of L;

      existence

      proof

        now

          assume

           A1: not (ex x be Element of the carrier of L st x <> ( 0. L));

          now

            let x,y be Element of the carrier of L;

            

            thus y = ( 0. L) by A1

            .= x by A1;

          end;

          hence contradiction by STRUCT_0:def 10;

        end;

        then

        consider x be Element of the carrier of L such that

         A2: x <> ( 0. L);

        set p = ((( 0_. L) +* ( 0 ,x)) +* (1,x));

        ex n be Nat st for i be Nat st i >= n holds (p . i) = ( 0. L)

        proof

          take 2;

          now

            let i be Nat;

            assume

             A3: i >= 2;

            then

             A4: 1 <> i;

            

             A5: i in NAT by ORDINAL1:def 12;

            

            thus (p . i) = ((( 0_. L) +* ( 0 ,x)) . i) by A4, FUNCT_7: 32

            .= (( 0_. L) . i) by A3, FUNCT_7: 32

            .= ( 0. L) by A5, FUNCOP_1: 7;

          end;

          hence thesis;

        end;

        then

        reconsider p as Polynomial of L by ALGSEQ_1:def 1;

        take p;

        now

          let i be Nat;

          assume

           A6: i >= 2;

          then

           A7: 1 <> i;

          

           A8: i in NAT by ORDINAL1:def 12;

          

          thus (p . i) = ((( 0_. L) +* ( 0 ,x)) . i) by A7, FUNCT_7: 32

          .= (( 0_. L) . i) by A6, FUNCT_7: 32

          .= ( 0. L) by A8, FUNCOP_1: 7;

        end;

        then

         A9: 2 is_at_least_length_of p by ALGSEQ_1:def 2;

        now

          let m be Nat;

          assume

           A10: m is_at_least_length_of p;

          now

            assume m < 2;

            then m < (1 + 1);

            then m <= 1 by NAT_1: 13;

            then

             A11: (p . 1) = ( 0. L) by A10, ALGSEQ_1:def 2;

            ( dom ( 0_. L)) = NAT by FUNCOP_1: 13;

            then ( dom (( 0_. L) +* ( 0 ,x))) = NAT by FUNCT_7: 30;

            hence contradiction by A2, A11, FUNCT_7: 31;

          end;

          hence 2 <= m;

        end;

        then ( len p) = 2 by A9, ALGSEQ_1:def 3;

        then ( deg p) = 1;

        hence thesis;

      end;

    end

    registration

      let L be well-unital non degenerated non empty doubleLoopStr;

      let z be Element of L;

      let k be Element of NAT ;

      cluster ( rpoly (k,z)) -> non zero;

      coherence

      proof

        ( deg ( rpoly (k,z))) = k by HURWITZ: 27;

        then ( rpoly (k,z)) <> ( 0_. L) by HURWITZ: 20;

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive non degenerated doubleLoopStr;

      cluster ( Polynom-Ring L) -> non degenerated;

      coherence

      proof

        set S = ( Polynom-Ring L);

        ( 0. S) = ( 0_. L) & ( 1. S) = ( 1_. L) by POLYNOM3:def 10;

        hence thesis;

      end;

    end

    registration

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

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

      coherence ;

    end

    theorem :: RATFUNC1:5

    for L be add-associative right_zeroed right_complementable right-distributive associative non empty doubleLoopStr holds for p,q be Polynomial of L holds for a be Element of L holds ((a * p) *' q) = (a * (p *' q))

    proof

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

      let p,q be Polynomial of L;

      let a be Element of L;

      set f = ((a * p) *' q), g = (a * (p *' q));

      

       A1: ( dom f) = NAT by FUNCT_2:def 1

      .= ( dom g) by FUNCT_2:def 1;

      now

        let i be object;

        assume i in ( dom f);

        then

        reconsider n = i as Element of NAT ;

        consider fr be FinSequence of the carrier of L such that

         A2: ( len fr) = (n + 1) & (f . i) = ( Sum fr) & for k be Element of NAT st k in ( dom fr) holds (fr . k) = (((a * p) . (k -' 1)) * (q . ((n + 1) -' k))) by POLYNOM3:def 9;

        consider fa be FinSequence of the carrier of L such that

         A3: ( len fa) = (n + 1) & ((p *' q) . i) = ( Sum fa) & for k be Element of NAT st k in ( dom fa) holds (fa . k) = ((p . (k -' 1)) * (q . ((n + 1) -' k))) by POLYNOM3:def 9;

        ( Seg ( len fa)) = ( dom fr) by A2, A3, FINSEQ_1:def 3;

        then

         A4: ( dom fa) = ( dom fr) by FINSEQ_1:def 3;

         A5:

        now

          let k be Element of NAT ;

          assume

           A6: k in ( dom fa);

          then (fa . k) = (fa /. k) by PARTFUN1:def 6;

          then

          reconsider x = (fa . k) as Element of L;

          

          thus (fr /. k) = (fr . k) by A6, A4, PARTFUN1:def 6

          .= (((a * p) . (k -' 1)) * (q . ((n + 1) -' k))) by A4, A6, A2

          .= ((a * (p . (k -' 1))) * (q . ((n + 1) -' k))) by POLYNOM5:def 4

          .= (a * ((p . (k -' 1)) * (q . ((n + 1) -' k)))) by GROUP_1:def 3

          .= (a * x) by A6, A3

          .= (a * (fa /. k)) by A6, PARTFUN1:def 6;

        end;

        (g . n) = (a * ( Sum fa)) by A3, POLYNOM5:def 4

        .= (f . n) by A5, A3, A2, Th1;

        hence (f . i) = (g . i);

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: RATFUNC1:6

    for L be add-associative right_zeroed right_complementable right-distributive commutative associative non empty doubleLoopStr holds for p,q be Polynomial of L holds for a be Element of L holds (p *' (a * q)) = (a * (p *' q))

    proof

      let L be add-associative right_zeroed right_complementable right-distributive commutative associative non empty doubleLoopStr;

      let p,q be Polynomial of L;

      let a be Element of L;

      set f = (p *' (a * q)), g = (a * (p *' q));

      

       A1: ( dom f) = NAT by FUNCT_2:def 1

      .= ( dom g) by FUNCT_2:def 1;

      now

        let i be object;

        assume i in ( dom f);

        then

        reconsider n = i as Element of NAT ;

        consider fr be FinSequence of the carrier of L such that

         A2: ( len fr) = (n + 1) & (f . i) = ( Sum fr) & for k be Element of NAT st k in ( dom fr) holds (fr . k) = ((p . (k -' 1)) * ((a * q) . ((n + 1) -' k))) by POLYNOM3:def 9;

        consider fa be FinSequence of the carrier of L such that

         A3: ( len fa) = (n + 1) & ((p *' q) . i) = ( Sum fa) & for k be Element of NAT st k in ( dom fa) holds (fa . k) = ((p . (k -' 1)) * (q . ((n + 1) -' k))) by POLYNOM3:def 9;

        ( Seg ( len fa)) = ( dom fr) by A2, A3, FINSEQ_1:def 3;

        then

         A4: ( dom fa) = ( dom fr) by FINSEQ_1:def 3;

         A5:

        now

          let k be Element of NAT ;

          assume

           A6: k in ( dom fa);

          then (fa . k) = (fa /. k) by PARTFUN1:def 6;

          then

          reconsider x = (fa . k) as Element of L;

          

          thus (fr /. k) = (fr . k) by A6, A4, PARTFUN1:def 6

          .= ((p . (k -' 1)) * ((a * q) . ((n + 1) -' k))) by A4, A6, A2

          .= ((p . (k -' 1)) * (a * (q . ((n + 1) -' k)))) by POLYNOM5:def 4

          .= (a * ((p . (k -' 1)) * (q . ((n + 1) -' k)))) by GROUP_1:def 3

          .= (a * x) by A6, A3

          .= (a * (fa /. k)) by A6, PARTFUN1:def 6;

        end;

        (g . n) = (a * ( Sum fa)) by A3, POLYNOM5:def 4

        .= (f . n) by A5, Th1, A3, A2;

        hence (f . i) = (g . i);

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    registration

      let L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non trivial doubleLoopStr;

      let p be non zero Polynomial of L;

      let a be non zero Element of L;

      cluster (a * p) -> non zero;

      coherence

      proof

        a <> ( 0. L);

        then ( len (a * p)) = ( len p) by POLYNOM5: 25;

        then (a * p) <> ( 0_. L) by POLYNOM4: 3, POLYNOM4: 5;

        hence thesis;

      end;

    end

    registration

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

      let p1,p2 be non zero Polynomial of L;

      cluster (p1 *' p2) -> non zero;

      coherence

      proof

        reconsider x1 = p1 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

        reconsider x2 = p2 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

        p1 <> ( 0_. L);

        then

         A1: x1 <> ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

        p2 <> ( 0_. L);

        then x2 <> ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

        then (x1 * x2) <> ( 0. ( Polynom-Ring L)) by A1, VECTSP_2:def 1;

        then (p1 *' p2) <> ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

        then (p1 *' p2) <> ( 0_. L) by POLYNOM3:def 10;

        hence thesis;

      end;

    end

    theorem :: RATFUNC1:7

    

     Th7: for L be add-associative right_zeroed right_complementable distributive Abelian domRing-like non trivial doubleLoopStr holds for p1,p2 be Polynomial of L holds for p3 be non zero Polynomial of L st (p1 *' p3) = (p2 *' p3) holds p1 = p2

    proof

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

      let p1,p2 be Polynomial of L;

      let p3 be non zero Polynomial of L;

      assume

       A1: (p1 *' p3) = (p2 *' p3);

      reconsider x1 = p1 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      reconsider x2 = p2 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      reconsider x3 = p3 as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      p3 <> ( 0_. L);

      then

       A2: x3 <> ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

      

       A3: (x1 * x3) = (p2 *' p3) by A1, POLYNOM3:def 10

      .= (x2 * x3) by POLYNOM3:def 10;

      x3 is right_mult-cancelable by A2, ALGSTR_0:def 37;

      hence thesis by A3;

    end;

    registration

      let L be non trivial ZeroStr;

      let p be non zero Polynomial of L;

      cluster ( degree p) -> natural;

      coherence

      proof

        p <> ( 0_. L);

        then ( deg p) <> ( - 1) by HURWITZ: 20;

        then ( len p) <> 0 ;

        then (( deg p) + 1) > 0 ;

        then ( deg p) in NAT by INT_1: 3, INT_1: 7;

        hence thesis;

      end;

    end

    theorem :: RATFUNC1:8

    

     Th8: for L be add-associative right_zeroed right_complementable unital right-distributive non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) = 0 holds for x be Element of L holds ( eval (p,x)) <> ( 0. L)

    proof

      let L be add-associative right_zeroed right_complementable unital right-distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      assume

       A1: ( deg p) = 0 ;

      let x be Element of L;

      assume ( eval (p,x)) = ( 0. L);

      then x is_a_root_of p by POLYNOM5:def 7;

      then p is with_roots by POLYNOM5:def 8;

      hence contradiction by A1, HURWITZ: 24;

    end;

    theorem :: RATFUNC1:9

    

     Th9: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( eval (p,x)) = ( 0. L) iff ( rpoly (1,x)) divides p

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated doubleLoopStr;

      let p be Polynomial of L;

      let x be Element of L;

       A1:

      now

        assume ( rpoly (1,x)) divides p;

        then (p mod ( rpoly (1,x))) = ( 0_. L);

        then ((p - ((p div ( rpoly (1,x))) *' ( rpoly (1,x)))) + ((p div ( rpoly (1,x))) *' ( rpoly (1,x)))) = ((p div ( rpoly (1,x))) *' ( rpoly (1,x))) by POLYNOM3: 28;

        

        then

         A2: ((p div ( rpoly (1,x))) *' ( rpoly (1,x))) = (p + (( - ((p div ( rpoly (1,x))) *' ( rpoly (1,x)))) + ((p div ( rpoly (1,x))) *' ( rpoly (1,x))))) by POLYNOM3: 26

        .= (p + (((p div ( rpoly (1,x))) *' ( rpoly (1,x))) - ((p div ( rpoly (1,x))) *' ( rpoly (1,x)))))

        .= (p + ( 0_. L)) by POLYNOM3: 29

        .= p by POLYNOM3: 28;

        

         A3: ( eval (( rpoly (1,x)),x)) = (x - x) by HURWITZ: 29

        .= ( 0. L) by RLVECT_1: 15;

        

        thus ( eval (p,x)) = (( eval ((p div ( rpoly (1,x))),x)) * ( 0. L)) by A3, A2, POLYNOM4: 24

        .= ( 0. L);

      end;

      ( eval (p,x)) = ( 0. L) implies ( rpoly (1,x)) divides p by HURWITZ: 35, POLYNOM5:def 7;

      hence thesis by A1;

    end;

    theorem :: RATFUNC1:10

    

     Th10: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible domRing-like non degenerated doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L st ( rpoly (1,x)) divides (p *' q) holds ( rpoly (1,x)) divides p or ( rpoly (1,x)) divides q

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive domRing-like almost_left_invertible non degenerated doubleLoopStr;

      let p,q be Polynomial of L;

      let x be Element of L;

      assume ( rpoly (1,x)) divides (p *' q);

      then ( eval ((p *' q),x)) = ( 0. L) by Th9;

      then

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

      per cases by A1, VECTSP_2:def 1;

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

        hence thesis by Th9;

      end;

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

        hence thesis by Th9;

      end;

    end;

    theorem :: RATFUNC1:11

    

     Th11: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated doubleLoopStr holds for f be FinSequence of ( Polynom-Ring L) st for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z)) holds for p be Polynomial of L st p = ( Product f) holds p <> ( 0_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non degenerated doubleLoopStr;

      let f be FinSequence of ( Polynom-Ring L);

      assume

       A1: for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

      let p be Polynomial of L;

      assume

       A2: p = ( Product f);

      defpred P[ Nat] means for f be FinSequence of ( Polynom-Ring L) st ( len f) = $1 & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z)) holds for p be Polynomial of L st p = ( Product f) holds p <> ( 0_. L);

      now

        let f be FinSequence of ( Polynom-Ring L);

        assume

         A3: ( len f) = 0 & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

        let p be Polynomial of L;

        assume

         A4: p = ( Product f);

        f = ( <*> the carrier of ( Polynom-Ring L)) by A3;

        

        then p = ( 1_ ( Polynom-Ring L)) by A4, GROUP_4: 8

        .= ( 1. ( Polynom-Ring L));

        then p <> ( 0. ( Polynom-Ring L));

        hence p <> ( 0_. L) by POLYNOM3:def 10;

      end;

      then

       A5: P[ 0 ];

       A6:

      now

        let n be Nat;

        assume

         A7: P[n];

        now

          let f be FinSequence of ( Polynom-Ring L);

          assume

           A8: ( len f) = (n + 1) & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

          let p be Polynomial of L;

          assume

           A9: p = ( Product f);

          f <> {} by A8;

          then

          consider g be FinSequence, u be object such that

           A10: f = (g ^ <*u*>) by FINSEQ_1: 46;

          reconsider g as FinSequence of ( Polynom-Ring L) by A10, FINSEQ_1: 36;

          

           A11: ( dom f) = ( Seg (n + 1)) by A8, FINSEQ_1:def 3;

          1 <= (n + 1) by NAT_1: 11;

          then

           A12: (n + 1) in ( dom f) by A11;

          

           A13: (n + 1) = (( len g) + ( len <*u*>)) by A8, A10, FINSEQ_1: 22

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

          then (f . (n + 1)) = u by A10, FINSEQ_1: 42;

          then

          consider z be Element of L such that

           A14: u = ( rpoly (1,z)) by A8, A12;

          reconsider u as Element of ( Polynom-Ring L) by A14, POLYNOM3:def 10;

          reconsider q = ( Product g) as Polynomial of L by POLYNOM3:def 10;

          

           A15: ( Product f) = (( Product g) * u) by A10, GROUP_4: 6;

          

           A16: u <> ( 0. ( Polynom-Ring L)) by A14, POLYNOM3:def 10;

          now

            let i be Nat;

            assume

             A17: i in ( dom g);

            then

             A18: (g . i) = (f . i) by A10, FINSEQ_1:def 7;

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

            hence ex z be Element of L st (g . i) = ( rpoly (1,z)) by A17, A18, A8;

          end;

          then q <> ( 0_. L) by A7, A13;

          then q <> ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

          then p <> ( 0. ( Polynom-Ring L)) by A9, A16, A15, VECTSP_2:def 1;

          hence p <> ( 0_. L) by POLYNOM3:def 10;

        end;

        hence P[(n + 1)];

      end;

      

       A19: for n be Nat holds P[n] from NAT_1:sch 2( A5, A6);

      ( len f) is Nat;

      hence thesis by A1, A2, A19;

    end;

    theorem :: RATFUNC1:12

    

     Th12: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible domRing-like non degenerated doubleLoopStr holds for f be FinSequence of ( Polynom-Ring L) st for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z)) holds for p be Polynomial of L st p = ( Product f) holds for x be Element of L holds ( eval (p,x)) = ( 0. L) iff ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x))

    proof

      let L be Field;

      let f be FinSequence of ( Polynom-Ring L);

      assume

       A1: for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

      let p be Polynomial of L;

      assume

       A2: p = ( Product f);

      let x be Element of L;

       A3:

      now

        assume ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x));

        then

        consider i be Nat such that

         A4: i in ( dom f) & (f . i) = ( rpoly (1,x));

        reconsider g = ( Del (f,i)) as FinSequence of ( Polynom-Ring L) by FINSEQ_3: 105;

        reconsider q = ( Product g) as Polynomial of L by POLYNOM3:def 10;

        

         A5: (f /. i) = ( rpoly (1,x)) by A4, PARTFUN1:def 6;

        ( Product f) = ((f /. i) * ( Product g)) by A4, Th3;

        then p = (( rpoly (1,x)) *' q) by A2, A5, POLYNOM3:def 10;

        then

         A6: ( eval (p,x)) = (( eval (( rpoly (1,x)),x)) * ( eval (q,x))) by POLYNOM4: 24;

        ( eval (( rpoly (1,x)),x)) = (x - x) by HURWITZ: 29

        .= ( 0. L) by RLVECT_1: 15;

        hence ( eval (p,x)) = ( 0. L) by A6;

      end;

      now

        assume

         A7: ( eval (p,x)) = ( 0. L);

        defpred P[ Nat] means for f be FinSequence of ( Polynom-Ring L) st ( len f) = $1 & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z)) holds for p be Polynomial of L st p = ( Product f) holds for x be Element of L holds ( eval (p,x)) = ( 0. L) implies ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x));

        now

          let f be FinSequence of ( Polynom-Ring L);

          assume

           A8: ( len f) = 0 & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

          let p be Polynomial of L;

          assume

           A9: p = ( Product f);

          let x be Element of L;

          assume

           A10: ( eval (p,x)) = ( 0. L);

          f = ( <*> the carrier of ( Polynom-Ring L)) by A8;

          

          then p = ( 1_ ( Polynom-Ring L)) by A9, GROUP_4: 8

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

          hence ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x)) by A10, POLYNOM4: 18;

        end;

        then

         A11: P[ 0 ];

         A12:

        now

          let n be Nat;

          assume

           A13: P[n];

          now

            let f be FinSequence of ( Polynom-Ring L);

            assume

             A14: ( len f) = (n + 1) & for i be Nat st i in ( dom f) holds ex z be Element of L st (f . i) = ( rpoly (1,z));

            let p be Polynomial of L;

            assume

             A15: p = ( Product f);

            let x be Element of L;

            assume

             A16: ( eval (p,x)) = ( 0. L);

            f <> {} by A14;

            then

            consider g be FinSequence, u be object such that

             A17: f = (g ^ <*u*>) by FINSEQ_1: 46;

            reconsider g as FinSequence of ( Polynom-Ring L) by A17, FINSEQ_1: 36;

            

             A18: ( dom f) = ( Seg (n + 1)) by A14, FINSEQ_1:def 3;

            1 <= (n + 1) by NAT_1: 11;

            then

             A19: (n + 1) in ( dom f) by A18;

            

             A20: (n + 1) = (( len g) + ( len <*u*>)) by A14, A17, FINSEQ_1: 22

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

            

             A21: (f . (n + 1)) = u by A20, A17, FINSEQ_1: 42;

            then

            consider z be Element of L such that

             A22: u = ( rpoly (1,z)) by A14, A19;

            reconsider u as Element of ( Polynom-Ring L) by A22, POLYNOM3:def 10;

            reconsider q = ( Product g) as Polynomial of L by POLYNOM3:def 10;

            ( Product f) = (( Product g) * u) by A17, GROUP_4: 6

            .= (q *' ( rpoly (1,z))) by A22, POLYNOM3:def 10;

            then

             A23: ( eval (p,x)) = (( eval (q,x)) * ( eval (( rpoly (1,z)),x))) by A15, POLYNOM4: 24;

             A24:

            now

              let i be Nat;

              assume

               A25: i in ( dom g);

              

               A26: ( dom g) c= ( dom f) by A17, FINSEQ_1: 26;

              (g . i) = (f . i) by A25, A17, FINSEQ_1:def 7;

              hence ex z be Element of L st (g . i) = ( rpoly (1,z)) by A25, A26, A14;

            end;

            now

              per cases by A23, A16, VECTSP_2:def 1;

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

                then

                consider i be Nat such that

                 A27: i in ( dom g) & (g . i) = ( rpoly (1,x)) by A20, A24, A13;

                

                 A28: ( dom g) c= ( dom f) by A17, FINSEQ_1: 26;

                (f . i) = ( rpoly (1,x)) by A27, A17, FINSEQ_1:def 7;

                hence ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x)) by A28, A27;

              end;

                suppose ( eval (( rpoly (1,z)),x)) = ( 0. L);

                then (x - z) = ( 0. L) by HURWITZ: 29;

                then x = z by RLVECT_1: 21;

                hence ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x)) by A19, A21, A22;

              end;

            end;

            hence ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x));

          end;

          hence P[(n + 1)];

        end;

        

         A29: for n be Nat holds P[n] from NAT_1:sch 2( A11, A12);

        ( len f) is Nat;

        hence ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x)) by A7, A1, A2, A29;

      end;

      hence thesis by A3;

    end;

    begin

    definition

      let L be unital non empty doubleLoopStr;

      let p1,p2 be Polynomial of L;

      let x be Element of L;

      :: RATFUNC1:def3

      pred x is_a_common_root_of p1,p2 means x is_a_root_of p1 & x is_a_root_of p2;

    end

    definition

      let L be unital non empty doubleLoopStr;

      let p1,p2 be Polynomial of L;

      :: RATFUNC1:def4

      pred p1,p2 have_a_common_root means ex x be Element of L st x is_a_common_root_of (p1,p2);

    end

    notation

      let L be unital non empty doubleLoopStr;

      let p1,p2 be Polynomial of L;

      synonym p1,p2 have_common_roots for p1,p2 have_a_common_root ;

      antonym p1,p2 have_no_common_roots for p1,p2 have_a_common_root ;

    end

    theorem :: RATFUNC1:13

    

     Th13: for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L st x is_a_root_of p holds x is_a_root_of ( - p)

    proof

      let L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      let x be Element of L;

      assume

       A1: x is_a_root_of p;

      ( eval (( - p),x)) = ( - ( eval (p,x))) by POLYNOM4: 20

      .= ( - ( 0. L)) by A1, POLYNOM5:def 7

      .= ( 0. L) by RLVECT_1: 12;

      hence x is_a_root_of ( - p) by POLYNOM5:def 7;

    end;

    theorem :: RATFUNC1:14

    

     Th14: for L be Abelian add-associative right_zeroed right_complementable unital left-distributive non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds for x be Element of L st x is_a_common_root_of (p1,p2) holds x is_a_root_of (p1 + p2)

    proof

      let L be Abelian add-associative right_zeroed right_complementable unital left-distributive non empty doubleLoopStr;

      let p1,p2 be Polynomial of L;

      let x be Element of L;

      assume x is_a_common_root_of (p1,p2);

      then x is_a_root_of p1 & x is_a_root_of p2;

      then

       A1: ( eval (p1,x)) = ( 0. L) & ( eval (p2,x)) = ( 0. L) by POLYNOM5:def 7;

      ( eval ((p1 + p2),x)) = (( 0. L) + ( 0. L)) by A1, POLYNOM4: 19

      .= ( 0. L) by RLVECT_1:def 4;

      hence x is_a_root_of (p1 + p2) by POLYNOM5:def 7;

    end;

    theorem :: RATFUNC1:15

    for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for p1,p2 be Polynomial of L holds for x be Element of L st x is_a_common_root_of (p1,p2) holds x is_a_root_of ( - (p1 + p2)) by Th13, Th14;

    theorem :: RATFUNC1:16

    for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L st x is_a_common_root_of (p,q) holds x is_a_root_of (p + q)

    proof

      let L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr;

      let p,q be Polynomial of L;

      let x be Element of L;

      assume x is_a_common_root_of (p,q);

      then

       A1: x is_a_root_of p & x is_a_root_of q;

      then

       A2: ( eval (p,x)) = ( 0. L) by POLYNOM5:def 7;

      

       A3: ( eval (q,x)) = ( 0. L) by A1, POLYNOM5:def 7;

      ( eval ((p + q),x)) = (( 0. L) + ( 0. L)) by A2, A3, POLYNOM4: 19

      .= ( 0. L) by RLVECT_1:def 4;

      hence thesis by POLYNOM5:def 7;

    end;

    theorem :: RATFUNC1:17

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non trivial doubleLoopStr holds for p1,p2 be Polynomial of L st p1 divides p2 & p1 is with_roots holds (p1,p2) have_common_roots

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non trivial doubleLoopStr;

      let p1,p2 be Polynomial of L;

      assume

       A1: p1 divides p2 & p1 is with_roots;

      per cases ;

        suppose

         A2: p1 = ( 0_. L);

        (p2 mod p1) = ( 0_. L) by A1;

        

        then ( 0_. L) = (p2 - ( 0_. L)) by A2, POLYNOM3: 34

        .= (p2 + ( 0_. L)) by HURWITZ: 9;

        then

         A3: p2 = ( 0_. L) by POLYNOM3: 28;

        ( eval (( 0_. L),( 0. L))) = ( 0. L) by POLYNOM4: 17;

        then ( 0. L) is_a_root_of ( 0_. L) by POLYNOM5:def 7;

        then ( 0. L) is_a_common_root_of (p1,p2) by A2, A3;

        hence thesis;

      end;

        suppose p1 <> ( 0_. L);

        then

        consider s be Polynomial of L such that

         A4: (s *' p1) = p2 by A1, HURWITZ: 34;

        consider x be Element of L such that

         A5: x is_a_root_of p1 by A1, POLYNOM5:def 8;

        

         A6: ( eval (p1,x)) = ( 0. L) by A5, POLYNOM5:def 7;

        ( eval (p2,x)) = (( eval (s,x)) * ( eval (p1,x))) by A4, POLYNOM4: 24

        .= ( 0. L) by A6;

        then x is_a_root_of p2 by POLYNOM5:def 7;

        then x is_a_common_root_of (p1,p2) by A5;

        hence thesis;

      end;

    end;

    definition

      let L be unital non empty doubleLoopStr;

      let p,q be Polynomial of L;

      :: RATFUNC1:def5

      func Common_Roots (p,q) -> Subset of L equals { x where x be Element of L : x is_a_common_root_of (p,q) };

      coherence

      proof

        set M = { x where x be Element of L : x is_a_common_root_of (p,q) };

        now

          let u be object;

          assume u in M;

          then ex x be Element of L st u = x & x is_a_common_root_of (p,q);

          hence u in the carrier of L;

        end;

        hence M is Subset of L by TARSKI:def 3;

      end;

    end

    begin

    definition

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      :: RATFUNC1:def6

      func Leading-Coefficient (p) -> Element of L equals (p . (( len p) -' 1));

      coherence ;

    end

    notation

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      synonym LC p for Leading-Coefficient (p);

    end

    registration

      let L be non trivial doubleLoopStr;

      let p be non zero Polynomial of L;

      cluster ( LC p) -> non zero;

      coherence

      proof

        p <> ( 0_. L);

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

        then ( 0 + 1) < (( len p) + 1) by XREAL_1: 8;

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

        then ((( len p) -' 1) + 1) = ( len p) by XREAL_1: 235;

        then (p . (( len p) -' 1)) <> ( 0. L) by ALGSEQ_1: 10;

        hence thesis;

      end;

    end

    theorem :: RATFUNC1:18

    

     Th18: for L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non empty doubleLoopStr holds for p be Polynomial of L holds for a be Element of L holds ( LC (a * p)) = (a * ( LC p))

    proof

      let L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      let a be Element of L;

      per cases ;

        suppose

         A1: a = ( 0. L);

        then

         A2: (a * ( LC p)) = ( 0. L);

        (a * p) = ( 0_. L) by A1, POLYNOM5: 26;

        hence thesis by A2, FUNCOP_1: 7;

      end;

        suppose

         A3: a <> ( 0. L);

        

        thus ( LC (a * p)) = (a * (p . (( len (a * p)) -' 1))) by POLYNOM5:def 4

        .= (a * ( LC p)) by A3, POLYNOM5: 25;

      end;

    end;

    definition

      let L be non empty doubleLoopStr;

      let p be Polynomial of L;

      :: RATFUNC1:def7

      attr p is normalized means ( LC p) = ( 1. L);

    end

    registration

      let L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non trivial doubleLoopStr;

      let p be non zero Polynomial of L;

      cluster ((( 1. L) / ( LC p)) * p) -> normalized;

      coherence

      proof

        

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

        ( LC ((( 1. L) / ( LC p)) * p)) = ((( 1. L) / ( LC p)) * ( LC p)) by Th18

        .= (( 1. L) * ((( LC p) " ) * ( LC p)))

        .= (( 1. L) * ( 1. L)) by A1, VECTSP_1:def 10

        .= ( 1. L);

        hence thesis;

      end;

    end

    registration

      let L be Field;

      let p be non zero Polynomial of L;

      cluster ( NormPolynomial p) -> normalized;

      coherence

      proof

        set q = ( NormPolynomial p);

        

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

        then (q . (( len p) -' 1)) = ( 1. L) by POLYNOM4: 5, POLYNOM5: 56;

        then ( LC q) = ( 1. L) by A1, POLYNOM4: 5, POLYNOM5: 57;

        hence thesis;

      end;

    end

    begin

    definition

      let L be non trivial multLoopStr_0;

      :: RATFUNC1:def8

      mode rational_function of L -> set means

      : Def8: ex p1 be Polynomial of L st ex p2 be non zero Polynomial of L st it = [p1, p2];

      existence

      proof

        reconsider RF = [ the Polynomial of L, the non zero Polynomial of L] as set by TARSKI: 1;

        take RF;

        thus thesis;

      end;

    end

    definition

      let L be non trivial multLoopStr_0;

      let p1 be Polynomial of L;

      let p2 be non zero Polynomial of L;

      :: original: [

      redefine

      func [p1,p2] -> rational_function of L ;

      coherence

      proof

        reconsider p = [p1, p2] as set by TARSKI: 1;

        ex q1 be Polynomial of L st ex q2 be non zero Polynomial of L st p = [q1, q2];

        hence thesis by Def8;

      end;

    end

    definition

      let L be non trivial multLoopStr_0;

      let z be rational_function of L;

      :: original: `1

      redefine

      func z `1 -> Polynomial of L ;

      coherence

      proof

        consider p1 be Polynomial of L such that

         A1: ex p2 be non zero Polynomial of L st z = [p1, p2] by Def8;

        consider p2 be non zero Polynomial of L such that

         A2: z = [p1, p2] by A1;

        thus thesis by A2;

      end;

      :: original: `2

      redefine

      func z `2 -> non zero Polynomial of L ;

      coherence

      proof

        consider p1 be Polynomial of L such that

         A3: ex p2 be non zero Polynomial of L st z = [p1, p2] by Def8;

        consider p2 be non zero Polynomial of L such that

         A4: z = [p1, p2] by A3;

        thus thesis by A4;

      end;

    end

    definition

      let L be non trivial multLoopStr_0;

      let z be rational_function of L;

      :: RATFUNC1:def9

      attr z is zero means

      : Def9: (z `1 ) = ( 0_. L);

    end

    registration

      let L be non trivial multLoopStr_0;

      cluster non zero for rational_function of L;

      existence

      proof

        set p1 = the non zero Polynomial of L;

        set p2 = the non zero Polynomial of L;

        take [p1, p2];

        thus thesis;

      end;

    end

    theorem :: RATFUNC1:19

    

     Th19: for L be non trivial multLoopStr_0 holds for z be rational_function of L holds z = [(z `1 ), (z `2 )]

    proof

      let L be non trivial multLoopStr_0;

      let z be rational_function of L;

      consider p1 be Polynomial of L such that

       A1: ex p2 be non zero Polynomial of L st z = [p1, p2] by Def8;

      consider p2 be non zero Polynomial of L such that

       A2: z = [p1, p2] by A1;

      thus thesis by A2;

    end;

    definition

      let L be add-associative right_zeroed right_complementable distributive unital non trivial doubleLoopStr;

      let z be rational_function of L;

      :: RATFUNC1:def10

      attr z is irreducible means

      : Def10: ((z `1 ),(z `2 )) have_no_common_roots ;

    end

    notation

      let L be add-associative right_zeroed right_complementable distributive unital non trivial doubleLoopStr;

      let z be rational_function of L;

      antonym z is reducible for z is irreducible;

    end

    definition

      let L be add-associative right_zeroed right_complementable distributive unital non trivial doubleLoopStr;

      let z be rational_function of L;

      :: RATFUNC1:def11

      attr z is normalized means

      : Def11: z is irreducible & (z `2 ) is normalized;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive unital non trivial doubleLoopStr;

      cluster normalized -> irreducible for rational_function of L;

      coherence ;

    end

    registration

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      cluster ( LC (z `2 )) -> non zero;

      coherence ;

    end

    definition

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      :: RATFUNC1:def12

      func NormRationalFunction z -> rational_function of L equals [((( 1. L) / ( LC (z `2 ))) * (z `1 )), ((( 1. L) / ( LC (z `2 ))) * (z `2 ))];

      coherence ;

    end

    notation

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      synonym NormRatF z for NormRationalFunction z;

    end

    registration

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be non zero rational_function of L;

      cluster ( NormRationalFunction z) -> non zero;

      coherence

      proof

        (z `1 ) <> ( 0_. L) by Def9;

        then

        reconsider z1 = (z `1 ) as non zero Polynomial of L by UPROOTS:def 5;

        ((( 1. L) / ( LC (z `2 ))) * z1) is non zero;

        then (( NormRatF z) `1 ) <> ( 0_. L);

        hence thesis;

      end;

    end

    definition

      let L be non degenerated multLoopStr_0;

      :: RATFUNC1:def13

      func 0._ (L) -> rational_function of L equals [( 0_. L), ( 1_. L)];

      coherence ;

      :: RATFUNC1:def14

      func 1._ (L) -> rational_function of L equals [( 1_. L), ( 1_. L)];

      coherence ;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated doubleLoopStr;

      cluster ( 0._ L) -> normalized;

      coherence

      proof

        set z = [( 0_. L), ( 1_. L)];

        set p1 = (z `1 ), p2 = (z `2 );

        now

          assume (p1,p2) have_a_common_root ;

          then

          consider x be Element of L such that

           A1: x is_a_common_root_of (p1,p2);

          x is_a_root_of p2 by A1;

          then ( eval (p2,x)) = ( 0. L) by POLYNOM5:def 7;

          hence contradiction by POLYNOM4: 18;

        end;

        then

         A2: z is irreducible;

        

         A3: ( len ( 1_. L)) = 1 by POLYNOM4: 4;

        (( len ( 1_. L)) -' 1) = (1 - 1) by A3, XREAL_0:def 2;

        then ( LC ( 1_. L)) = ( 1. L) by POLYNOM3: 30;

        then p2 is normalized;

        hence thesis by A2;

      end;

    end

    registration

      let L be non degenerated multLoopStr_0;

      cluster ( 1._ L) -> non zero;

      coherence ;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated doubleLoopStr;

      cluster ( 1._ L) -> irreducible;

      coherence

      proof

        set z = [( 1_. L), ( 1_. L)];

        set p1 = (z `1 ), p2 = (z `2 );

        now

          assume (p1,p2) have_a_common_root ;

          then

          consider x be Element of L such that

           A1: x is_a_common_root_of (p1,p2);

          x is_a_root_of p2 by A1;

          then ( eval (p2,x)) = ( 0. L) by POLYNOM5:def 7;

          hence contradiction by POLYNOM4: 18;

        end;

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated doubleLoopStr;

      cluster irreducible non zero for rational_function of L;

      existence

      proof

        take ( 1._ L);

        thus thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive Abelian associative well-unital non degenerated doubleLoopStr;

      let x be Element of L;

      cluster [( rpoly (1,x)), ( rpoly (1,x))] -> reducible non zero;

      coherence

      proof

        set z = [( rpoly (1,x)), ( rpoly (1,x))];

        x is_a_root_of ( rpoly (1,x)) by HURWITZ: 30;

        then x is_a_root_of (z `1 );

        then x is_a_common_root_of ((z `1 ),(z `2 ));

        then ((z `1 ),(z `2 )) have_common_roots ;

        then z is reducible;

        hence thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive Abelian associative well-unital non degenerated doubleLoopStr;

      cluster reducible non zero for rational_function of L;

      existence

      proof

        set x = the Element of L;

        take z = [( rpoly (1,x)), ( rpoly (1,x))];

        thus thesis;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated doubleLoopStr;

      cluster normalized for rational_function of L;

      existence

      proof

        take ( 0._ L);

        thus thesis;

      end;

    end

    registration

      let L be non degenerated multLoopStr_0;

      cluster ( 0._ L) -> zero;

      coherence ;

    end

    registration

      let L be add-associative right_zeroed right_complementable distributive associative well-unital non degenerated doubleLoopStr;

      cluster ( 1._ L) -> normalized;

      coherence

      proof

        ( len ( 1_. L)) = 1 by POLYNOM4: 4;

        then (( len ( 1_. L)) -' 1) = (1 - 1) by XREAL_0:def 2;

        then ( LC ( 1_. L)) = ( 1. L) by POLYNOM3: 30;

        then ( [( 1_. L), ( 1_. L)] `2 ) is normalized;

        hence ( 1._ L) is normalized;

      end;

    end

    definition

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

      let p,q be rational_function of L;

      :: RATFUNC1:def15

      func p + q -> rational_function of L equals [(((p `1 ) *' (q `2 )) + ((p `2 ) *' (q `1 ))), ((p `2 ) *' (q `2 ))];

      coherence ;

    end

    definition

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

      let p,q be rational_function of L;

      :: RATFUNC1:def16

      func p *' q -> rational_function of L equals [((p `1 ) *' (q `1 )), ((p `2 ) *' (q `2 ))];

      coherence ;

    end

    theorem :: RATFUNC1:20

    

     Th20: for L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non trivial doubleLoopStr holds for p be rational_function of L holds for a be non zero Element of L holds [(a * (p `1 )), (a * (p `2 ))] is irreducible iff p is irreducible

    proof

      let L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non trivial doubleLoopStr;

      let p be rational_function of L;

      let a be non zero Element of L;

      set ap = [(a * (p `1 )), (a * (p `2 ))];

       A1:

      now

        assume

         A2: p is irreducible;

        assume ap is reducible;

        then ((ap `1 ),(ap `2 )) have_common_roots ;

        then

        consider x be Element of L such that

         A3: x is_a_common_root_of ((ap `1 ),(ap `2 ));

        x is_a_root_of (ap `1 ) & x is_a_root_of (ap `2 ) by A3;

        then

         A4: ( eval ((ap `1 ),x)) = ( 0. L) & ( eval ((ap `2 ),x)) = ( 0. L) by POLYNOM5:def 7;

        then ( eval ((a * (p `1 )),x)) = ( 0. L);

        then (a * ( eval ((p `1 ),x))) = ( 0. L) by POLYNOM5: 30;

        then ( eval ((p `1 ),x)) = ( 0. L) by VECTSP_2:def 1;

        then

         A5: x is_a_root_of (p `1 ) by POLYNOM5:def 7;

        ( eval ((a * (p `2 )),x)) = ( 0. L) by A4;

        then (a * ( eval ((p `2 ),x))) = ( 0. L) by POLYNOM5: 30;

        then ( eval ((p `2 ),x)) = ( 0. L) by VECTSP_2:def 1;

        then x is_a_root_of (p `2 ) by POLYNOM5:def 7;

        then x is_a_common_root_of ((p `1 ),(p `2 )) by A5;

        then ((p `1 ),(p `2 )) have_common_roots ;

        hence [(a * (p `1 )), (a * (p `2 ))] is irreducible by A2;

      end;

      now

        assume

         A6: ap is irreducible;

        assume p is reducible;

        then ((p `1 ),(p `2 )) have_common_roots ;

        then

        consider x be Element of L such that

         A7: x is_a_common_root_of ((p `1 ),(p `2 ));

        x is_a_root_of (p `1 ) & x is_a_root_of (p `2 ) by A7;

        then

         A8: ( eval ((p `1 ),x)) = ( 0. L) & ( eval ((p `2 ),x)) = ( 0. L) by POLYNOM5:def 7;

        then (a * ( eval ((p `1 ),x))) = ( 0. L);

        then ( eval ((a * (p `1 )),x)) = ( 0. L) by POLYNOM5: 30;

        then ( eval ((ap `1 ),x)) = ( 0. L);

        then

         A9: x is_a_root_of (ap `1 ) by POLYNOM5:def 7;

        (a * ( eval ((p `2 ),x))) = ( 0. L) by A8;

        then ( eval ((a * (p `2 )),x)) = ( 0. L) by POLYNOM5: 30;

        then ( eval ((ap `2 ),x)) = ( 0. L);

        then x is_a_root_of (ap `2 ) by POLYNOM5:def 7;

        then x is_a_common_root_of ((ap `1 ),(ap `2 )) by A9;

        then ((ap `1 ),(ap `2 )) have_common_roots ;

        hence p is irreducible by A6;

      end;

      hence thesis by A1;

    end;

    begin

    

     Lm1: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative domRing-like non trivial doubleLoopStr holds for z be rational_function of L holds z is irreducible implies ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x))

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      assume

       A1: z is irreducible;

      take z;

      reconsider e = ( 1_. L) as non zero Polynomial of L;

      take e;

      reconsider f = ( <*> the carrier of ( Polynom-Ring L)) as FinSequence of ( Polynom-Ring L);

      

      thus z = [(z `1 ), (z `2 )] by Th19

      .= [(e *' (z `1 )), (z `2 )] by POLYNOM3: 35

      .= [(e *' (z `1 )), (e *' (z `2 ))] by POLYNOM3: 35;

      thus z is irreducible by A1;

      take f;

      ( Product f) = ( 1_ ( Polynom-Ring L)) by GROUP_4: 8;

      hence thesis by POLYNOM3:def 10;

    end;

    theorem :: RATFUNC1:21

    

     Th21: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative domRing-like non trivial doubleLoopStr holds for z be rational_function of L holds ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x))

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      defpred P[ Nat] means for z be rational_function of L st ( max (( deg (z `1 )),( deg (z `2 )))) = $1 holds ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

      now

        let z be rational_function of L;

        assume ( max (( deg (z `1 )),( deg (z `2 )))) = 0 ;

        then ( deg (z `2 )) <= 0 by XXREAL_0: 25;

        then

         A1: ( deg (z `2 )) = 0 ;

         A2:

        now

          assume ex x be Element of L st x is_a_root_of (z `2 );

          then

          consider y be Element of L such that

           A3: y is_a_root_of (z `2 );

          ( eval ((z `2 ),y)) = ( 0. L) by A3, POLYNOM5:def 7;

          hence contradiction by A1, Th8;

        end;

        now

          assume z is reducible;

          then ((z `1 ),(z `2 )) have_common_roots ;

          then

          consider x be Element of L such that

           A4: x is_a_common_root_of ((z `1 ),(z `2 ));

          x is_a_root_of (z `2 ) by A4;

          hence contradiction by A2;

        end;

        hence ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Lm1;

      end;

      then

       A5: P[ 0 ];

       A6:

      now

        let n be Nat;

        assume

         A7: P[n];

        for z be rational_function of L st ( max (( deg (z `1 )),( deg (z `2 )))) = (n + 1) holds ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x))

        proof

          let z be rational_function of L;

          assume

           A8: ( max (( deg (z `1 )),( deg (z `2 )))) = (n + 1);

          per cases ;

            suppose z is irreducible;

            hence thesis by Lm1;

          end;

            suppose z is reducible;

            then ((z `1 ),(z `2 )) have_common_roots ;

            then

            consider x be Element of L such that

             A9: x is_a_common_root_of ((z `1 ),(z `2 ));

            

             A10: x is_a_root_of (z `1 ) & x is_a_root_of (z `2 ) by A9;

            consider q2 be Polynomial of L such that

             A11: (z `2 ) = (( rpoly (1,x)) *' q2) by A10, HURWITZ: 33;

            consider q1 be Polynomial of L such that

             A12: (z `1 ) = (( rpoly (1,x)) *' q1) by A10, HURWITZ: 33;

            q2 <> ( 0_. L) by A11, POLYNOM3: 34;

            then

            reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;

            set q = [q1, q2];

            ( max (( deg (q `1 )),( deg (q `2 )))) = n

            proof

              

               A13: ( deg (z `2 )) = (( deg ( rpoly (1,x))) + ( deg q2)) by A11, HURWITZ: 23

              .= (1 + ( deg q2)) by HURWITZ: 27;

              per cases by XXREAL_0: 16;

                suppose

                 A14: ( max (( deg (z `1 )),( deg (z `2 )))) = ( deg (z `1 ));

                then (z `1 ) <> ( 0_. L) by A8, HURWITZ: 20;

                then q1 <> ( 0_. L) by A12, POLYNOM3: 34;

                

                then

                 A15: ( deg (z `1 )) = (( deg ( rpoly (1,x))) + ( deg q1)) by A12, HURWITZ: 23

                .= (1 + ( deg q1)) by HURWITZ: 27;

                

                 A16: ( deg (z `2 )) <= (n + 1) by A8, XXREAL_0: 25;

                ((( deg q2) + 1) - 1) <= ((n + 1) - 1) by A13, A16, XREAL_1: 9;

                hence thesis by A15, A14, A8, XXREAL_0:def 10;

              end;

                suppose

                 A17: ( max (( deg (z `1 )),( deg (z `2 )))) = ( deg (z `2 ));

                

                 A18: ( deg (z `1 )) <= (n + 1) by A8, XXREAL_0: 25;

                now

                  per cases ;

                    suppose q1 = ( 0_. L);

                    hence ( deg q1) <= ( deg q2) by HURWITZ: 20;

                  end;

                    suppose q1 <> ( 0_. L);

                    

                    then ( deg (z `1 )) = (( deg ( rpoly (1,x))) + ( deg q1)) by A12, HURWITZ: 23

                    .= (1 + ( deg q1)) by HURWITZ: 27;

                    hence ( deg q1) <= ( deg q2) by A18, A13, A17, A8, XREAL_1: 9;

                  end;

                end;

                hence thesis by A17, A13, A8, XXREAL_0:def 10;

              end;

            end;

            then

            consider z1q be rational_function of L, z2q be non zero Polynomial of L such that

             A19: q = [(z2q *' (z1q `1 )), (z2q *' (z1q `2 ))] & z1q is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2q = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (f . i) = ( rpoly (1,x)) by A7;

            take z1 = z1q;

            set z2 = (( rpoly (1,x)) *' z2q);

            reconsider z2 as non zero Polynomial of L;

            take z2;

            consider fq be FinSequence of ( Polynom-Ring L) such that

             A20: z2q = ( Product fq) & for i be Element of NAT st i in ( dom fq) holds ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (fq . i) = ( rpoly (1,x)) by A19;

            reconsider rp = ( rpoly (1,x)) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

            set f = ( <*rp*> ^ fq);

            

             A21: ( Product f) = (rp * ( Product fq)) by GROUP_4: 7

            .= z2 by A20, POLYNOM3:def 10;

            

             A22: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))]

            proof

              

               A23: q1 = (z2q *' (z1q `1 )) by A19, XTUPLE_0:def 2;

              

               A24: q2 = (z2q *' (z1q `2 )) by A19, XTUPLE_0:def 3;

              

               A25: (z2 *' (z1 `1 )) = (z `1 ) by A23, A12, POLYNOM3: 33;

              

               A26: (z2 *' (z1 `2 )) = (z `2 ) by A24, A11, POLYNOM3: 33;

              thus z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] by A25, A26, Th19;

            end;

             A27:

            now

              let i be Element of NAT ;

              assume

               A28: i in ( dom f);

              now

                per cases by A28, FINSEQ_1: 25;

                  suppose

                   A29: i in ( dom <*rp*>);

                  then

                   A30: i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

                  (f . i) = ( <*rp*> . i) by A29, FINSEQ_1:def 7

                  .= ( <*rp*> . 1) by A30, TARSKI:def 1

                  .= ( rpoly (1,x)) by FINSEQ_1: 40;

                  hence ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A9;

                end;

                  suppose ex n be Nat st n in ( dom fq) & i = (( len <*rp*>) + n);

                  then

                  consider n be Nat such that

                   A31: n in ( dom fq) & i = (( len <*rp*>) + n);

                  (f . i) = (fq . n) by A31, FINSEQ_1:def 7;

                  then

                  consider y be Element of L such that

                   A32: y is_a_common_root_of ((q `1 ),(q `2 )) & (f . i) = ( rpoly (1,y)) by A31, A20;

                  

                   A33: y is_a_root_of (q `1 ) & y is_a_root_of (q `2 ) by A32;

                  then

                   A34: ( 0. L) = ( eval (q1,y)) by POLYNOM5:def 7;

                  

                   A35: ( eval ((z `1 ),y)) = (( eval (( rpoly (1,x)),y)) * ( eval (q1,y))) by A12, POLYNOM4: 24

                  .= ( 0. L) by A34;

                  

                   A36: ( 0. L) = ( eval (q2,y)) by A33, POLYNOM5:def 7;

                  ( eval ((z `2 ),y)) = (( eval (( rpoly (1,x)),y)) * ( eval (q2,y))) by A11, POLYNOM4: 24

                  .= ( 0. L) by A36;

                  then y is_a_root_of (z `1 ) & y is_a_root_of (z `2 ) by A35, POLYNOM5:def 7;

                  then y is_a_common_root_of ((z `1 ),(z `2 ));

                  hence ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A32;

                end;

              end;

              hence ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

            end;

            thus thesis by A19, A21, A22, A27;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A37: for n be Nat holds P[n] from NAT_1:sch 2( A5, A6);

      ( max (( deg (z `1 )),( deg (z `2 )))) >= ( deg (z `2 )) by XXREAL_0: 25;

      then ( max (( deg (z `1 )),( deg (z `2 )))) >= 0 ;

      then ( max (( deg (z `1 )),( deg (z `2 )))) in NAT by INT_1: 3;

      hence thesis by A37;

    end;

    

     Lm2: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be rational_function of L st z is irreducible holds for z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds for g1 be rational_function of L, g2 be non zero Polynomial of L st z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st g2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds z2 = ( 1_. L) & g2 = ( 1_. L) & z1 = g1

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      assume

       A1: z is irreducible;

      let z1 be rational_function of L, z2 be non zero Polynomial of L;

      assume

       A2: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

      let g1 be rational_function of L, g2 be non zero Polynomial of L;

      assume

       A3: z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st g2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

      consider f be FinSequence of ( Polynom-Ring L) such that

       A4: z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A2;

      now

        assume f <> ( <*> the carrier of ( Polynom-Ring L));

        then

         A5: ( dom f) <> {} ;

        let i be Element of ( dom f);

        reconsider i as Nat;

        

         A6: i in ( dom f) by A5;

        consider x be Element of L such that

         A7: x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A6, A4;

        ((z `1 ),(z `2 )) have_common_roots by A7;

        hence contradiction by A1;

      end;

      

      hence

       A8: z2 = ( 1_ ( Polynom-Ring L)) by A4, GROUP_4: 8

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

      then

       A9: (z2 *' (z1 `1 )) = (z1 `1 ) by POLYNOM3: 35;

      (z2 *' (z1 `2 )) = (z1 `2 ) by A8, POLYNOM3: 35;

      then

       A10: z = z1 by A9, A2, Th19;

      consider h be FinSequence of ( Polynom-Ring L) such that

       A11: g2 = ( Product h) & for i be Element of NAT st i in ( dom h) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (h . i) = ( rpoly (1,x)) by A3;

      now

        assume h <> ( <*> the carrier of ( Polynom-Ring L));

        then

         A12: ( dom h) <> {} ;

        let i be Element of ( dom h);

        reconsider i as Nat;

        

         A13: i in ( dom h) by A12;

        consider x be Element of L such that

         A14: x is_a_common_root_of ((z `1 ),(z `2 )) & (h . i) = ( rpoly (1,x)) by A13, A11;

        ((z `1 ),(z `2 )) have_common_roots by A14;

        hence contradiction by A1;

      end;

      

      hence

       A15: g2 = ( 1_ ( Polynom-Ring L)) by A11, GROUP_4: 8

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

      then

       A16: (g2 *' (g1 `1 )) = (g1 `1 ) by POLYNOM3: 35;

      (g2 *' (g1 `2 )) = (g1 `2 ) by A15, POLYNOM3: 35;

      hence z1 = g1 by A10, A16, A3, Th19;

    end;

    

     Lm3: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be non zero rational_function of L holds for z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds for g1 be rational_function of L, g2 be non zero Polynomial of L st z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x)) holds z1 = g1

    proof

      let L be Field;

      let z be non zero rational_function of L;

      let z1 be rational_function of L, z2 be non zero Polynomial of L;

      assume

       A1: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

      let g1 be rational_function of L, g2 be non zero Polynomial of L;

      assume

       A2: z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x));

      defpred P[ Nat] means for z be non zero rational_function of L st ( max (( deg (z `1 )),( deg (z `2 )))) = $1 holds for z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds for g1 be rational_function of L, g2 be non zero Polynomial of L st z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x)) holds z1 = g1;

      now

        let z be non zero rational_function of L;

        assume ( max (( deg (z `1 )),( deg (z `2 )))) = 0 ;

        then ( deg (z `2 )) <= 0 by XXREAL_0: 25;

        then

         A3: ( deg (z `2 )) = 0 ;

        let z1 be rational_function of L, z2 be non zero Polynomial of L;

        assume

         A4: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

        let g1 be rational_function of L, g2 be non zero Polynomial of L;

        assume

         A5: z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x));

         A6:

        now

          assume ex x be Element of L st x is_a_root_of (z `2 );

          then

          consider y be Element of L such that

           A7: y is_a_root_of (z `2 );

          ( eval ((z `2 ),y)) = ( 0. L) by A7, POLYNOM5:def 7;

          hence contradiction by A3, Th8;

        end;

         A8:

        now

          assume z is reducible;

          then ((z `1 ),(z `2 )) have_common_roots ;

          then

          consider x be Element of L such that

           A9: x is_a_common_root_of ((z `1 ),(z `2 ));

          x is_a_root_of (z `2 ) by A9;

          hence contradiction by A6;

        end;

        thus g1 = z1 by A8, A4, A5, Lm2;

      end;

      then

       A10: P[ 0 ];

       A11:

      now

        let n be Nat;

        assume

         A12: P[n];

        for z be non zero rational_function of L st ( max (( deg (z `1 )),( deg (z `2 )))) = (n + 1) holds for z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds for g1 be rational_function of L, g2 be non zero Polynomial of L st z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x)) holds z1 = g1

        proof

          let z be non zero rational_function of L;

          assume

           A13: ( max (( deg (z `1 )),( deg (z `2 )))) = (n + 1);

          let z1 be rational_function of L, z2 be non zero Polynomial of L such that

           A14: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x));

          consider f be FinSequence of ( Polynom-Ring L) such that

           A15: z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A14;

          let g1 be rational_function of L, g2 be non zero Polynomial of L such that

           A16: z = [(g2 *' (g1 `1 )), (g2 *' (g1 `2 ))] & g1 is irreducible & ex g be FinSequence of ( Polynom-Ring L) st g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x));

          consider g be FinSequence of ( Polynom-Ring L) such that

           A17: g2 = ( Product g) & for i be Element of NAT st i in ( dom g) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (g . i) = ( rpoly (1,x)) by A16;

          per cases ;

            suppose

             A18: z is irreducible;

            thus g1 = z1 by A18, A14, A16, Lm2;

          end;

            suppose z is reducible;

            then ((z `1 ),(z `2 )) have_common_roots ;

            then

            consider x be Element of L such that

             A19: x is_a_common_root_of ((z `1 ),(z `2 ));

            

             A20: x is_a_root_of (z `1 ) & x is_a_root_of (z `2 ) by A19;

            consider q2 be Polynomial of L such that

             A21: (z `2 ) = (( rpoly (1,x)) *' q2) by A20, HURWITZ: 33;

            consider q1 be Polynomial of L such that

             A22: (z `1 ) = (( rpoly (1,x)) *' q1) by A20, HURWITZ: 33;

            q2 <> ( 0_. L) by A21, POLYNOM3: 34;

            then

            reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;

            set q = [q1, q2];

            (z `1 ) <> ( 0_. L) by Def9;

            then q1 <> ( 0_. L) by A22, POLYNOM3: 34;

            then (q `1 ) <> ( 0_. L);

            then

            reconsider q as non zero rational_function of L by Def9;

            

             A23: ( max (( deg (q `1 )),( deg (q `2 )))) = n

            proof

              

               A24: ( deg (z `2 )) = (( deg ( rpoly (1,x))) + ( deg q2)) by A21, HURWITZ: 23

              .= (1 + ( deg q2)) by HURWITZ: 27;

              per cases by XXREAL_0: 16;

                suppose

                 A25: ( max (( deg (z `1 )),( deg (z `2 )))) = ( deg (z `1 ));

                then (z `1 ) <> ( 0_. L) by A13, HURWITZ: 20;

                then q1 <> ( 0_. L) by A22, POLYNOM3: 34;

                

                then

                 A26: ( deg (z `1 )) = (( deg ( rpoly (1,x))) + ( deg q1)) by A22, HURWITZ: 23

                .= (1 + ( deg q1)) by HURWITZ: 27;

                ( deg (z `2 )) <= (n + 1) by A13, XXREAL_0: 25;

                then ((( deg q2) + 1) - 1) <= ((n + 1) - 1) by A24, XREAL_1: 9;

                hence thesis by A26, A25, A13, XXREAL_0:def 10;

              end;

                suppose

                 A27: ( max (( deg (z `1 )),( deg (z `2 )))) = ( deg (z `2 ));

                

                 A28: ( deg (z `1 )) <= (n + 1) by A13, XXREAL_0: 25;

                now

                  per cases ;

                    suppose q1 = ( 0_. L);

                    hence ( deg q1) <= ( deg q2) by HURWITZ: 20;

                  end;

                    suppose q1 <> ( 0_. L);

                    

                    then ( deg (z `1 )) = (( deg ( rpoly (1,x))) + ( deg q1)) by A22, HURWITZ: 23

                    .= (1 + ( deg q1)) by HURWITZ: 27;

                    hence ( deg q1) <= ( deg q2) by A28, A27, A24, A13, XREAL_1: 9;

                  end;

                end;

                hence thesis by A24, A27, A13, XXREAL_0:def 10;

              end;

            end;

             A29:

            now

              let i be Nat;

              assume i in ( dom f);

              then ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A15;

              hence ex z be Element of L st (f . i) = ( rpoly (1,z));

            end;

            ex i be Nat st i in ( dom f) & (f . i) = ( rpoly (1,x))

            proof

              (z2 *' (z1 `1 )) = (( rpoly (1,x)) *' q1) by A22, A14;

              then

               A30: ( rpoly (1,x)) divides (z2 *' (z1 `1 )) by HURWITZ: 34;

              (z2 *' (z1 `2 )) = (( rpoly (1,x)) *' q2) by A21, A14;

              then

               A31: ( rpoly (1,x)) divides (z2 *' (z1 `2 )) by HURWITZ: 34;

              now

                per cases by A30, A31, Th10;

                  case ( rpoly (1,x)) divides z2;

                  then ( eval (z2,x)) = ( 0. L) by Th9;

                  then

                  consider i be Nat such that

                   A32: i in ( dom f) & (f . i) = ( rpoly (1,x)) by Th12, A15, A29;

                  take i;

                  thus thesis by A32;

                end;

                  case ( rpoly (1,x)) divides (z1 `1 ) & ( rpoly (1,x)) divides (z1 `2 );

                  then ( eval ((z1 `1 ),x)) = ( 0. L) & ( eval ((z1 `2 ),x)) = ( 0. L) by Th9;

                  then x is_a_root_of (z1 `1 ) & x is_a_root_of (z1 `2 ) by POLYNOM5:def 7;

                  then

                   A33: x is_a_common_root_of ((z1 `1 ),(z1 `2 ));

                  ((z1 `1 ),(z1 `2 )) have_no_common_roots by A14;

                  hence thesis by A33;

                end;

              end;

              hence thesis;

            end;

            then

            consider i be Nat such that

             A34: i in ( dom f) & (f . i) = ( rpoly (1,x));

             A35:

            now

              let j be Nat;

              assume j in ( dom g);

              then

              consider x be Element of L such that

               A36: x is_a_common_root_of ((z `1 ),(z `2 )) & (g . j) = ( rpoly (1,x)) by A17;

              thus ex z be Element of L st (g . j) = ( rpoly (1,z)) by A36;

            end;

            ex j be Nat st j in ( dom g) & (g . j) = ( rpoly (1,x))

            proof

              (g2 *' (g1 `1 )) = (( rpoly (1,x)) *' q1) by A22, A16;

              then

               A37: ( rpoly (1,x)) divides (g2 *' (g1 `1 )) by HURWITZ: 34;

              (g2 *' (g1 `2 )) = (( rpoly (1,x)) *' q2) by A21, A16;

              then

               A38: ( rpoly (1,x)) divides (g2 *' (g1 `2 )) by HURWITZ: 34;

              now

                per cases by A37, A38, Th10;

                  case ( rpoly (1,x)) divides g2;

                  then ( eval (g2,x)) = ( 0. L) by Th9;

                  then

                  consider i be Nat such that

                   A39: i in ( dom g) & (g . i) = ( rpoly (1,x)) by Th12, A17, A35;

                  take i;

                  thus thesis by A39;

                end;

                  case ( rpoly (1,x)) divides (g1 `1 ) & ( rpoly (1,x)) divides (g1 `2 );

                  then ( eval ((g1 `1 ),x)) = ( 0. L) & ( eval ((g1 `2 ),x)) = ( 0. L) by Th9;

                  then x is_a_root_of (g1 `1 ) & x is_a_root_of (g1 `2 ) by POLYNOM5:def 7;

                  then

                   A40: x is_a_common_root_of ((g1 `1 ),(g1 `2 ));

                  ((g1 `1 ),(g1 `2 )) have_no_common_roots by A16;

                  hence thesis by A40;

                end;

              end;

              hence thesis;

            end;

            then

            consider j be Nat such that

             A41: j in ( dom g) & (g . j) = ( rpoly (1,x));

            reconsider fq = ( Del (f,i)) as FinSequence of ( Polynom-Ring L) by FINSEQ_3: 105;

            reconsider gq = ( Del (g,j)) as FinSequence of ( Polynom-Ring L) by FINSEQ_3: 105;

             A42:

            now

              let k be Nat;

              assume

               A43: k in ( dom fq);

              consider m be Nat such that

               A44: ( len f) = (m + 1) & ( len fq) = m by A34, FINSEQ_3: 104;

              

               A45: k in ( Seg m) by A43, A44, FINSEQ_1:def 3;

              ( Seg m) c= ( Seg (m + 1)) by FINSEQ_3: 18;

              then k in ( Seg (m + 1)) by A45;

              then

               A46: k in ( dom f) by A44, FINSEQ_1:def 3;

              

               A47: k <= m by A45, FINSEQ_1: 1;

              then

               A48: (k + 1) <= (m + 1) by XREAL_1: 6;

              1 <= (k + 1) by NAT_1: 11;

              then (k + 1) in ( Seg (m + 1)) by A48;

              then

               A49: (k + 1) in ( dom f) by A44, FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A50: k < i;

                  ex y be Element of L st y is_a_common_root_of ((z `1 ),(z `2 )) & (f . k) = ( rpoly (1,y)) by A46, A15;

                  hence ex x be Element of L st (fq . k) = ( rpoly (1,x)) by A50, FINSEQ_3: 110;

                end;

                  suppose

                   A51: i <= k;

                  ex y be Element of L st y is_a_common_root_of ((z `1 ),(z `2 )) & (f . (k + 1)) = ( rpoly (1,y)) by A15, A49;

                  hence ex x be Element of L st (fq . k) = ( rpoly (1,x)) by A51, A47, A34, A44, FINSEQ_3: 111;

                end;

              end;

              hence ex x be Element of L st (fq . k) = ( rpoly (1,x));

            end;

             A52:

            now

              let k be Nat;

              assume

               A53: k in ( dom gq);

              consider m be Nat such that

               A54: ( len g) = (m + 1) & ( len gq) = m by A41, FINSEQ_3: 104;

              

               A55: k in ( Seg m) by A53, A54, FINSEQ_1:def 3;

              ( Seg m) c= ( Seg (m + 1)) by FINSEQ_3: 18;

              then k in ( Seg (m + 1)) by A55;

              then

               A56: k in ( dom g) by A54, FINSEQ_1:def 3;

              

               A57: k <= m by A55, FINSEQ_1: 1;

              then

               A58: (k + 1) <= (m + 1) by XREAL_1: 6;

              1 <= (k + 1) by NAT_1: 11;

              then (k + 1) in ( Seg (m + 1)) by A58;

              then

               A59: (k + 1) in ( dom g) by A54, FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A60: k < j;

                  ex y be Element of L st y is_a_common_root_of ((z `1 ),(z `2 )) & (g . k) = ( rpoly (1,y)) by A56, A17;

                  hence ex x be Element of L st (gq . k) = ( rpoly (1,x)) by A60, FINSEQ_3: 110;

                end;

                  suppose

                   A61: j <= k;

                  ex y be Element of L st y is_a_common_root_of ((z `1 ),(z `2 )) & (g . (k + 1)) = ( rpoly (1,y)) by A17, A59;

                  hence ex x be Element of L st (gq . k) = ( rpoly (1,x)) by A61, A57, A41, A54, FINSEQ_3: 111;

                end;

              end;

              hence ex x be Element of L st (gq . k) = ( rpoly (1,x));

            end;

            reconsider z2q = ( Product fq) as Polynomial of L by POLYNOM3:def 10;

            z2q <> ( 0_. L) by A42, Th11;

            then

            reconsider z2q as non zero Polynomial of L by UPROOTS:def 5;

            reconsider g2q = ( Product gq) as Polynomial of L by POLYNOM3:def 10;

            g2q <> ( 0_. L) by A52, Th11;

            then

            reconsider g2q as non zero Polynomial of L by UPROOTS:def 5;

            

             A62: ( Product f) = ((f /. i) * ( Product fq)) by A34, Th3;

            

             A63: ( Product g) = ((g /. j) * ( Product gq)) by A41, Th3;

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

            then 1 <= i & i <= ( len f) by A34, FINSEQ_1: 1;

            then (f /. i) = ( rpoly (1,x)) by A34, FINSEQ_4: 15;

            then

             A64: (( rpoly (1,x)) *' z2q) = ( Product f) by A62, POLYNOM3:def 10;

            

            then

             A65: (( rpoly (1,x)) *' (z2q *' (z1 `1 ))) = (z2 *' (z1 `1 )) by A15, POLYNOM3: 33

            .= (( rpoly (1,x)) *' q1) by A22, A14

            .= (( rpoly (1,x)) *' (q `1 ));

            then

             A66: (z2q *' (z1 `1 )) = (q `1 ) by Th7;

            

             A67: (( rpoly (1,x)) *' (z2q *' (z1 `2 ))) = (z2 *' (z1 `2 )) by A64, A15, POLYNOM3: 33

            .= (( rpoly (1,x)) *' q2) by A21, A14

            .= (( rpoly (1,x)) *' (q `2 ));

            then (z2q *' (z1 `2 )) = (q `2 ) by Th7;

            then

             A68: q = [(z2q *' (z1 `1 )), (z2q *' (z1 `2 ))] by A66;

             A69:

            now

              let k be Element of NAT ;

              assume

               A70: k in ( dom fq);

              consider m be Nat such that

               A71: ( len f) = (m + 1) & ( len fq) = m by A34, FINSEQ_3: 104;

              

               A72: k in ( Seg m) by A70, A71, FINSEQ_1:def 3;

              ( Seg m) c= ( Seg (m + 1)) by FINSEQ_3: 18;

              then k in ( Seg (m + 1)) by A72;

              then

               A73: k in ( dom f) by A71, FINSEQ_1:def 3;

              

               A74: k <= m by A72, FINSEQ_1: 1;

              then

               A75: (k + 1) <= (m + 1) by XREAL_1: 6;

              1 <= (k + 1) by NAT_1: 11;

              then (k + 1) in ( Seg (m + 1)) by A75;

              then

               A76: (k + 1) in ( dom f) by A71, FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A77: k < i;

                  then

                   A78: (f . k) = (fq . k) by FINSEQ_3: 110;

                  consider y be Element of L such that

                   A79: y is_a_common_root_of ((z `1 ),(z `2 )) & (f . k) = ( rpoly (1,y)) by A73, A15;

                  

                   A80: ( eval (z2q,y)) = ( 0. L) by A78, A79, A70, A42, Th12;

                  

                  then ( 0. L) = (( eval (z2q,y)) * ( eval ((z1 `1 ),y)))

                  .= ( eval ((z2q *' (z1 `1 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `1 ),y)) by A65, Th7;

                  then

                   A81: y is_a_root_of (q `1 ) by POLYNOM5:def 7;

                  ( 0. L) = (( eval (z2q,y)) * ( eval ((z1 `2 ),y))) by A80

                  .= ( eval ((z2q *' (z1 `2 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `2 ),y)) by A67, Th7;

                  then y is_a_root_of (q `2 ) by POLYNOM5:def 7;

                  then y is_a_common_root_of ((q `1 ),(q `2 )) by A81;

                  hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (fq . k) = ( rpoly (1,x)) by A79, A77, FINSEQ_3: 110;

                end;

                  suppose

                   A82: i <= k;

                  then

                   A83: (f . (k + 1)) = (fq . k) by A74, A34, A71, FINSEQ_3: 111;

                  consider y be Element of L such that

                   A84: y is_a_common_root_of ((z `1 ),(z `2 )) & (f . (k + 1)) = ( rpoly (1,y)) by A15, A76;

                  

                   A85: ( eval (z2q,y)) = ( 0. L) by A83, A84, A70, A42, Th12;

                  

                  then ( 0. L) = (( eval (z2q,y)) * ( eval ((z1 `1 ),y)))

                  .= ( eval ((z2q *' (z1 `1 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `1 ),y)) by A65, Th7;

                  then

                   A86: y is_a_root_of (q `1 ) by POLYNOM5:def 7;

                  ( 0. L) = (( eval (z2q,y)) * ( eval ((z1 `2 ),y))) by A85

                  .= ( eval ((z2q *' (z1 `2 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `2 ),y)) by A67, Th7;

                  then y is_a_root_of (q `2 ) by POLYNOM5:def 7;

                  then y is_a_common_root_of ((q `1 ),(q `2 )) by A86;

                  hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (fq . k) = ( rpoly (1,x)) by A84, A82, A74, A34, A71, FINSEQ_3: 111;

                end;

              end;

              hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (fq . k) = ( rpoly (1,x));

            end;

            ( Seg ( len g)) = ( dom g) by FINSEQ_1:def 3;

            then 1 <= j & j <= ( len g) by A41, FINSEQ_1: 1;

            then (g /. j) = ( rpoly (1,x)) by A41, FINSEQ_4: 15;

            then

             A87: (( rpoly (1,x)) *' g2q) = ( Product g) by A63, POLYNOM3:def 10;

            

            then

             A88: (( rpoly (1,x)) *' (g2q *' (g1 `1 ))) = (g2 *' (g1 `1 )) by A17, POLYNOM3: 33

            .= (z `1 ) by A16

            .= (( rpoly (1,x)) *' (q `1 )) by A22;

            then

             A89: (g2q *' (g1 `1 )) = (q `1 ) by Th7;

            

             A90: (( rpoly (1,x)) *' (g2q *' (g1 `2 ))) = (g2 *' (g1 `2 )) by A87, A17, POLYNOM3: 33

            .= (z `2 ) by A16

            .= (( rpoly (1,x)) *' (q `2 )) by A21;

            then (g2q *' (g1 `2 )) = (q `2 ) by Th7;

            then

             A91: q = [(g2q *' (g1 `1 )), (g2q *' (g1 `2 ))] by A89;

             A92:

            now

              let k be Element of NAT ;

              assume

               A93: k in ( dom gq);

              consider m be Nat such that

               A94: ( len g) = (m + 1) & ( len gq) = m by A41, FINSEQ_3: 104;

              

               A95: k in ( Seg m) by A93, A94, FINSEQ_1:def 3;

              ( Seg m) c= ( Seg (m + 1)) by FINSEQ_3: 18;

              then k in ( Seg (m + 1)) by A95;

              then

               A96: k in ( dom g) by A94, FINSEQ_1:def 3;

              

               A97: k <= m by A95, FINSEQ_1: 1;

              then

               A98: (k + 1) <= (m + 1) by XREAL_1: 6;

              1 <= (k + 1) by NAT_1: 11;

              then (k + 1) in ( Seg (m + 1)) by A98;

              then

               A99: (k + 1) in ( dom g) by A94, FINSEQ_1:def 3;

              now

                per cases ;

                  suppose

                   A100: k < j;

                  then

                   A101: (g . k) = (gq . k) by FINSEQ_3: 110;

                  consider y be Element of L such that

                   A102: y is_a_common_root_of ((z `1 ),(z `2 )) & (g . k) = ( rpoly (1,y)) by A96, A17;

                  

                   A103: ( eval (g2q,y)) = ( 0. L) by A101, A102, A93, A52, Th12;

                  

                  then ( 0. L) = (( eval (g2q,y)) * ( eval ((g1 `1 ),y)))

                  .= ( eval ((g2q *' (g1 `1 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `1 ),y)) by A88, Th7;

                  then

                   A104: y is_a_root_of (q `1 ) by POLYNOM5:def 7;

                  ( 0. L) = (( eval (g2q,y)) * ( eval ((g1 `2 ),y))) by A103

                  .= ( eval ((g2q *' (g1 `2 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `2 ),y)) by A90, Th7;

                  then y is_a_root_of (q `2 ) by POLYNOM5:def 7;

                  then y is_a_common_root_of ((q `1 ),(q `2 )) by A104;

                  hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (gq . k) = ( rpoly (1,x)) by A102, A100, FINSEQ_3: 110;

                end;

                  suppose

                   A105: j <= k;

                  then

                   A106: (g . (k + 1)) = (gq . k) by A97, A41, A94, FINSEQ_3: 111;

                  consider y be Element of L such that

                   A107: y is_a_common_root_of ((z `1 ),(z `2 )) & (g . (k + 1)) = ( rpoly (1,y)) by A17, A99;

                  

                   A108: ( eval (g2q,y)) = ( 0. L) by A106, A107, A93, A52, Th12;

                  

                  then ( 0. L) = (( eval (g2q,y)) * ( eval ((g1 `1 ),y)))

                  .= ( eval ((g2q *' (g1 `1 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `1 ),y)) by A88, Th7;

                  then

                   A109: y is_a_root_of (q `1 ) by POLYNOM5:def 7;

                  ( 0. L) = (( eval (g2q,y)) * ( eval ((g1 `2 ),y))) by A108

                  .= ( eval ((g2q *' (g1 `2 )),y)) by POLYNOM4: 24

                  .= ( eval ((q `2 ),y)) by A90, Th7;

                  then y is_a_root_of (q `2 ) by POLYNOM5:def 7;

                  then y is_a_common_root_of ((q `1 ),(q `2 )) by A109;

                  hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (gq . k) = ( rpoly (1,x)) by A107, A105, A97, A41, A94, FINSEQ_3: 111;

                end;

              end;

              hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (gq . k) = ( rpoly (1,x));

            end;

            thus z1 = g1 by A14, A16, A68, A91, A69, A92, A23, A12;

          end;

        end;

        hence P[(n + 1)];

      end;

      

       A110: for n be Nat holds P[n] from NAT_1:sch 2( A10, A11);

      ( max (( deg (z `1 )),( deg (z `2 )))) >= ( deg (z `2 )) by XXREAL_0: 25;

      then ( max (( deg (z `1 )),( deg (z `2 )))) >= 0 ;

      then ( max (( deg (z `1 )),( deg (z `2 )))) in NAT by INT_1: 3;

      hence z1 = g1 by A110, A1, A2;

    end;

    definition

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      :: RATFUNC1:def17

      func NF z -> rational_function of L means

      : Def17: ex z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & it = ( NormRationalFunction z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) if z is non zero

      otherwise it = ( 0._ L);

      existence

      proof

        per cases ;

          suppose z is non zero;

          consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

           A1: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Th21;

          reconsider nfz = ( NormRatF z1) as rational_function of L;

          ex zz1 be rational_function of L, zz2 be non zero Polynomial of L st nfz = ( NormRatF zz1) & zz1 is irreducible & (ex f be FinSequence of ( Polynom-Ring L) st zz2 = ( Product f) & z = [(zz2 *' (zz1 `1 )), (zz2 *' (zz1 `2 ))] & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x))) by A1;

          hence thesis;

        end;

          suppose z is zero;

          hence thesis;

        end;

      end;

      uniqueness by Lm3;

      consistency ;

    end

    registration

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      cluster ( NF z) -> normalized irreducible;

      coherence

      proof

        per cases ;

          suppose z is non zero;

          then

          consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

           A1: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ( NF z) = ( NormRatF z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Def17;

          

           A2: ( NF z) is irreducible by A1, Th20;

          (( NF z) `2 ) = ((( 1. L) / ( LC (z1 `2 ))) * (z1 `2 )) by A1;

          hence thesis by A2;

        end;

          suppose z is zero;

          then ( NF z) = ( 0._ L) by Def17;

          hence thesis;

        end;

      end;

    end

    registration

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be non zero rational_function of L;

      cluster ( NF z) -> non zero;

      coherence

      proof

        consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

         A1: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ( NF z) = ( NormRatF z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Def17;

        (z1 `1 ) <> ( 0_. L) by A1, POLYNOM3: 34, Def9;

        then z1 is non zero;

        hence thesis by A1;

      end;

    end

    

     Lm4: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be irreducible non zero rational_function of L holds ( NF z) = ( NormRationalFunction z)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be irreducible non zero rational_function of L;

      consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

       A1: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ( NF z) = ( NormRatF z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Def17;

      consider f be FinSequence of ( Polynom-Ring L) such that

       A2: z2 = ( Product f) & z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A1;

      now

        assume

         A3: f <> ( <*> the carrier of ( Polynom-Ring L));

        let i be Element of ( dom f);

        ( dom f) <> {} by A3;

        then i in ( dom f);

        then

        reconsider i as Element of NAT ;

        consider x be Element of L such that

         A4: x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A2, A3;

        ((z `1 ),(z `2 )) have_common_roots by A4;

        hence contradiction by Def10;

      end;

      

      then

       A5: ( Product f) = ( 1_ ( Polynom-Ring L)) by GROUP_4: 8

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

      

      then z = [(z1 `1 ), (z2 *' (z1 `2 ))] by A2, POLYNOM3: 35

      .= [(z1 `1 ), (z1 `2 )] by A2, A5, POLYNOM3: 35

      .= z1 by Th19;

      hence thesis by A1;

    end;

    theorem :: RATFUNC1:22

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be non zero rational_function of L holds for z1 be rational_function of L, z2 be non zero Polynomial of L st z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) holds ( NF z) = ( NormRationalFunction z1) by Def17;

    theorem :: RATFUNC1:23

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds ( NF ( 0._ L)) = ( 0._ L) by Def17;

    theorem :: RATFUNC1:24

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds ( NF ( 1._ L)) = ( 1._ L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      set z = ( 1._ L);

      

       A1: ( NF z) = ( NormRatF z) by Lm4

      .= [((( 1. L) / ( LC (z `2 ))) * (z `1 )), ((( 1. L) / ( LC (z `2 ))) * (z `2 ))];

      (z `2 ) is normalized by Def11;

      then

       A2: ( LC (z `2 )) = ( 1. L);

      

       A3: (( 1. L) / ( LC (z `2 ))) = ((( LC (z `2 )) " ) * ( LC (z `2 ))) by A2

      .= ( 1. L) by VECTSP_1:def 10;

      

      hence ( NF z) = [(z `1 ), ((( 1. L) / ( LC (z `2 ))) * (z `2 ))] by A1, POLYNOM5: 27

      .= [(z `1 ), (z `2 )] by A3, POLYNOM5: 27

      .= z;

    end;

    theorem :: RATFUNC1:25

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be irreducible non zero rational_function of L holds ( NF z) = ( NormRationalFunction z) by Lm4;

    

     Lm5: for L be Abelian add-associative right_zeroed right_complementable unital domRing-like left_zeroed distributive non trivial doubleLoopStr holds for p1,p2 be Polynomial of L holds (p1 *' p2) = ( 0_. L) implies p1 = ( 0_. L) or p2 = ( 0_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable unital domRing-like left_zeroed distributive non trivial doubleLoopStr;

      let p1,p2 be Polynomial of L;

      assume

       A1: (p1 *' p2) = ( 0_. L);

      now

        assume p1 <> ( 0_. L) & p2 <> ( 0_. L);

        then

        reconsider x1 = p1, x2 = p2 as non zero Polynomial of L by UPROOTS:def 5;

        (x1 *' x2) is non zero;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: RATFUNC1:26

    

     Th26: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be rational_function of L holds for x be Element of L holds ( NF [(( rpoly (1,x)) *' (z `1 )), (( rpoly (1,x)) *' (z `2 ))]) = ( NF z)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      let x be Element of L;

      per cases ;

        suppose

         A1: z is non zero;

        then

        consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

         A2: z = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ( NF z) = ( NormRatF z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by Def17;

        consider f be FinSequence of ( Polynom-Ring L) such that

         A3: z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . i) = ( rpoly (1,x)) by A2;

        set q = [(( rpoly (1,x)) *' (z `1 )), (( rpoly (1,x)) *' (z `2 ))];

        (q `1 ) <> ( 0_. L) by A1, Lm5;

        then

        reconsider q as non zero rational_function of L by Def9;

        reconsider rp = ( rpoly (1,x)) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

        set g = ( <*rp*> ^ f);

        reconsider g as FinSequence of ( Polynom-Ring L);

        set g2 = ( Product g);

        now

          let i be Nat;

          assume

           A4: i in ( dom g);

          now

            per cases by A4, FINSEQ_1: 25;

              suppose

               A5: i in ( dom <*rp*>);

              then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

              then i = 1 by TARSKI:def 1;

              

              then (g . i) = ( <*rp*> . 1) by A5, FINSEQ_1:def 7

              .= rp by FINSEQ_1: 40;

              hence ex z be Element of L st (g . i) = ( rpoly (1,z));

            end;

              suppose ex n be Nat st n in ( dom f) & i = (( len <*rp*>) + n);

              then

              consider n be Nat such that

               A6: n in ( dom f) & i = (( len <*rp*>) + n);

              

               A7: (g . i) = (f . n) by A6, FINSEQ_1:def 7;

              ex x be Element of L st x is_a_common_root_of ((z `1 ),(z `2 )) & (f . n) = ( rpoly (1,x)) by A6, A3;

              hence ex z be Element of L st (g . i) = ( rpoly (1,z)) by A7;

            end;

          end;

          hence ex z be Element of L st (g . i) = ( rpoly (1,z));

        end;

        then g2 <> ( 0_. L) by Th11;

        then

        reconsider g2 as non zero Polynomial of L by UPROOTS:def 5, POLYNOM3:def 10;

         A8:

        now

          let i be Element of NAT ;

          assume

           A9: i in ( dom g);

          now

            per cases by A9, FINSEQ_1: 25;

              suppose

               A10: i in ( dom <*rp*>);

              then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

              then i = 1 by TARSKI:def 1;

              

              then

               A11: (g . i) = ( <*rp*> . 1) by A10, FINSEQ_1:def 7

              .= rp by FINSEQ_1: 40;

              

               A12: ( eval (( rpoly (1,x)),x)) = (x - x) by HURWITZ: 29

              .= ( 0. L) by RLVECT_1: 15;

              

              then ( 0. L) = (( eval (( rpoly (1,x)),x)) * ( eval ((z `1 ),x)))

              .= ( eval ((( rpoly (1,x)) *' (z `1 )),x)) by POLYNOM4: 24;

              then x is_a_root_of (( rpoly (1,x)) *' (z `1 )) by POLYNOM5:def 7;

              then

               A13: x is_a_root_of (q `1 );

              ( 0. L) = (( eval (( rpoly (1,x)),x)) * ( eval ((z `2 ),x))) by A12

              .= ( eval ((( rpoly (1,x)) *' (z `2 )),x)) by POLYNOM4: 24;

              then x is_a_root_of (( rpoly (1,x)) *' (z `2 )) by POLYNOM5:def 7;

              then x is_a_root_of (q `2 );

              then x is_a_common_root_of ((q `1 ),(q `2 )) by A13;

              hence ex z be Element of L st z is_a_common_root_of ((q `1 ),(q `2 )) & (g . i) = ( rpoly (1,z)) by A11;

            end;

              suppose ex n be Nat st n in ( dom f) & i = (( len <*rp*>) + n);

              then

              consider n be Nat such that

               A14: n in ( dom f) & i = (( len <*rp*>) + n);

              

               A15: (g . i) = (f . n) by A14, FINSEQ_1:def 7;

              consider y be Element of L such that

               A16: y is_a_common_root_of ((z `1 ),(z `2 )) & (f . n) = ( rpoly (1,y)) by A14, A3;

              y is_a_root_of (z `1 ) by A16;

              then ( eval ((z `1 ),y)) = ( 0. L) by POLYNOM5:def 7;

              

              then ( 0. L) = (( eval (( rpoly (1,x)),y)) * ( eval ((z `1 ),y)))

              .= ( eval ((( rpoly (1,x)) *' (z `1 )),y)) by POLYNOM4: 24;

              then y is_a_root_of (( rpoly (1,x)) *' (z `1 )) by POLYNOM5:def 7;

              then

               A17: y is_a_root_of (q `1 );

              y is_a_root_of (z `2 ) by A16;

              then ( eval ((z `2 ),y)) = ( 0. L) by POLYNOM5:def 7;

              

              then ( 0. L) = (( eval (( rpoly (1,x)),y)) * ( eval ((z `2 ),y)))

              .= ( eval ((( rpoly (1,x)) *' (z `2 )),y)) by POLYNOM4: 24;

              then y is_a_root_of (( rpoly (1,x)) *' (z `2 )) by POLYNOM5:def 7;

              then y is_a_root_of (q `2 );

              then y is_a_common_root_of ((q `1 ),(q `2 )) by A17;

              hence ex z be Element of L st z is_a_common_root_of ((q `1 ),(q `2 )) & (g . i) = ( rpoly (1,z)) by A15, A16;

            end;

          end;

          hence ex x be Element of L st x is_a_common_root_of ((q `1 ),(q `2 )) & (g . i) = ( rpoly (1,x));

        end;

        

         A18: ( Product g) = (rp * ( Product f)) by GROUP_4: 7;

        

         A19: (q `1 ) = (( rpoly (1,x)) *' (z `1 ))

        .= (( rpoly (1,x)) *' (z2 *' (z1 `1 ))) by A2

        .= ((( rpoly (1,x)) *' z2) *' (z1 `1 )) by POLYNOM3: 33

        .= (g2 *' (z1 `1 )) by A18, A3, POLYNOM3:def 10;

        (q `2 ) = (( rpoly (1,x)) *' (z `2 ))

        .= (( rpoly (1,x)) *' (z2 *' (z1 `2 ))) by A2

        .= ((( rpoly (1,x)) *' z2) *' (z1 `2 )) by POLYNOM3: 33

        .= (g2 *' (z1 `2 )) by A18, A3, POLYNOM3:def 10;

        then q = [(g2 *' (z1 `1 )), (g2 *' (z1 `2 ))] by A19;

        hence thesis by A2, A8, Def17;

      end;

        suppose

         A20: z is zero;

        then (z `1 ) = ( 0_. L);

        then (( rpoly (1,x)) *' (z `1 )) = ( 0_. L) by POLYNOM3: 34;

        then ( [(( rpoly (1,x)) *' (z `1 )), (( rpoly (1,x)) *' (z `2 ))] `1 ) = ( 0_. L);

        then [(( rpoly (1,x)) *' (z `1 )), (( rpoly (1,x)) *' (z `2 ))] is zero;

        then ( NF [(( rpoly (1,x)) *' (z `1 )), (( rpoly (1,x)) *' (z `2 ))]) = ( 0._ L) by Def17;

        hence thesis by A20, Def17;

      end;

    end;

    theorem :: RATFUNC1:27

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be rational_function of L holds ( NF ( NF z)) = ( NF z)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      set nfz = ( NF z);

      per cases ;

        suppose z is zero;

        then

         A1: ( NF z) = ( 0._ L) by Def17;

        thus thesis by A1, Def17;

      end;

        suppose

         A2: z is non zero;

        

         A3: ( 1. L) <> ( 0. L);

        

         A4: ( NF nfz) = ( NormRatF nfz) by A2, Lm4

        .= [((( 1. L) / ( LC (nfz `2 ))) * (nfz `1 )), ((( 1. L) / ( LC (nfz `2 ))) * (nfz `2 ))];

        (nfz `2 ) is normalized by Def11;

        then

         A5: ( LC (nfz `2 )) = ( 1. L);

        

         A6: (( 1. L) / ( LC (nfz `2 ))) = ((( LC (nfz `2 )) " ) * ( LC (nfz `2 ))) by A5

        .= ( 1. L) by VECTSP_1:def 10, A3;

        

        then ( NF nfz) = [(nfz `1 ), ((( 1. L) / ( LC (nfz `2 ))) * (nfz `2 ))] by A4, POLYNOM5: 27

        .= [(nfz `1 ), (nfz `2 )] by A6, POLYNOM5: 27

        .= nfz by Th19;

        hence thesis;

      end;

    end;

    theorem :: RATFUNC1:28

    

     Th28: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non degenerated doubleLoopStr holds for z be non zero rational_function of L holds z is irreducible iff ex a be Element of L st a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non degenerated doubleLoopStr;

      let z be non zero rational_function of L;

      set q = (z `2 );

      set a = (( LC (z `2 )) " );

      now

        assume

         A1: a = ( 0. L);

        then

         A2: (a * ( LC q)) = ( 0. L);

        a <> ( 1. L) by A1;

        hence contradiction by A2, VECTSP_1:def 10;

      end;

      then

      reconsider a as non zero Element of L by STRUCT_0:def 12;

      reconsider x = [(a * (z `1 )), (a * (z `2 ))] as rational_function of L;

       A3:

      now

        assume z is irreducible;

        

        then ( NF z) = ( NormRatF z) by Lm4

        .= [((( 1. L) / ( LC (z `2 ))) * (z `1 )), ((( 1. L) / ( LC (z `2 ))) * (z `2 ))];

        hence ex a be Element of L st a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z);

      end;

      now

        assume ex a be Element of L st a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z);

        then

        consider a be Element of L such that

         A4: a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z);

        reconsider x = [(a * (z `1 )), (a * (z `2 ))] as rational_function of L by A4;

        now

          assume ((z `1 ),(z `2 )) have_a_common_root ;

          then

          consider u be Element of L such that

           A5: u is_a_common_root_of ((z `1 ),(z `2 ));

          u is_a_root_of (z `1 ) & u is_a_root_of (z `2 ) by A5;

          then

           A6: ( eval ((z `1 ),u)) = ( 0. L) & ( eval ((z `2 ),u)) = ( 0. L) by POLYNOM5:def 7;

          ( eval ((x `1 ),u)) = (a * ( eval ((z `1 ),u))) by POLYNOM5: 30;

          then ( eval ((x `1 ),u)) = ( 0. L) by A6;

          then

           A7: u is_a_root_of (x `1 ) by POLYNOM5:def 7;

          ( eval ((x `2 ),u)) = (a * ( eval ((z `2 ),u))) by POLYNOM5: 30;

          then ( eval ((x `2 ),u)) = ( 0. L) by A6;

          then u is_a_root_of (x `2 ) by POLYNOM5:def 7;

          then u is_a_common_root_of ((x `1 ),(x `2 )) by A7;

          then ((x `1 ),(x `2 )) have_a_common_root ;

          hence contradiction by Def10, A4;

        end;

        hence z is irreducible;

      end;

      hence thesis by A3;

    end;

    begin

    definition

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      :: RATFUNC1:def18

      func degree z -> Integer equals ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 ))));

      coherence ;

    end

    notation

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      synonym deg z for degree z;

    end

    

     Lm6: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be non zero rational_function of L st z is irreducible holds ( degree z) = ( max (( degree (z `1 )),( degree (z `2 ))))

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be non zero rational_function of L;

      assume z is irreducible;

      then

      consider a be Element of L such that

       A1: a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z) by Th28;

      a is non zero by A1;

      then

      reconsider az2 = (a * (z `2 )) as non zero Polynomial of L;

      

      thus ( degree z) = ( max (( deg (a * (z `1 ))),( deg (a * (z `2 ))))) by A1

      .= ( max (( deg (z `1 )),( deg az2))) by A1, POLYNOM5: 25

      .= ( max (( degree (z `1 )),( degree (z `2 )))) by A1, POLYNOM5: 25;

    end;

    theorem :: RATFUNC1:29

    

     Th29: for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be rational_function of L holds ( degree z) <= ( max (( degree (z `1 )),( degree (z `2 ))))

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be rational_function of L;

      per cases ;

        suppose

         A1: z is zero;

        

        then

         A2: ( NF z) = ( 0._ L) by Def17

        .= [( 0_. L), ( 1_. L)];

        (z `1 ) = ( 0_. L) by A1;

        then

         A3: ( deg (z `1 )) = ( - 1) by HURWITZ: 20;

        

         A4: ( deg ( 1_. L)) = (1 - 1) by POLYNOM4: 4;

        ( deg z) = ( max (( deg ( 0_. L)),( degree (( NF z) `2 )))) by A2

        .= ( max (( deg ( 0_. L)),( deg ( 1_. L)))) by A2

        .= ( max (( - 1),( deg ( 1_. L)))) by HURWITZ: 20

        .= 0 by A4, XXREAL_0:def 10;

        hence thesis by A3, XXREAL_0:def 10;

      end;

        suppose

         A5: z is non zero;

        defpred P[ Nat] means for z be non zero rational_function of L st ( max (( degree (z `1 )),( degree (z `2 )))) = $1 holds ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 )))) <= ( max (( degree (z `1 )),( degree (z `2 ))));

        now

          let z be non zero rational_function of L, z1 be rational_function of L, z2 be non zero Polynomial of L;

          let f be FinSequence of ( Polynom-Ring L);

          assume

           A6: ( max (( degree (z `1 )),( degree (z `2 )))) = 0 ;

          now

            per cases by A6, XXREAL_0: 16;

              suppose

               A7: ( degree (z `1 )) = 0 ;

              now

                assume ((z `1 ),(z `2 )) have_common_roots ;

                then

                consider x be Element of L such that

                 A8: x is_a_common_root_of ((z `1 ),(z `2 ));

                x is_a_root_of (z `1 ) by A8;

                then (z `1 ) is with_roots by POLYNOM5:def 8;

                hence contradiction by A7, HURWITZ: 24;

              end;

              hence ((z `1 ),(z `2 )) have_no_common_roots ;

            end;

              suppose

               A9: ( degree (z `2 )) = 0 ;

              now

                assume ((z `1 ),(z `2 )) have_common_roots ;

                then

                consider x be Element of L such that

                 A10: x is_a_common_root_of ((z `1 ),(z `2 ));

                x is_a_root_of (z `2 ) by A10;

                then (z `2 ) is with_roots by POLYNOM5:def 8;

                hence contradiction by A9, HURWITZ: 24;

              end;

              hence ((z `1 ),(z `2 )) have_no_common_roots ;

            end;

          end;

          then z is irreducible;

          then ( degree z) = ( max (( degree (z `1 )),( degree (z `2 )))) by Lm6;

          hence ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 )))) <= ( max (( degree (z `1 )),( degree (z `2 ))));

        end;

        then

         A11: P[ 0 ];

         A12:

        now

          let n be Nat;

          assume

           A13: P[n];

          now

            let z be non zero rational_function of L;

            assume

             A14: ( max (( degree (z `1 )),( degree (z `2 )))) = (n + 1);

            per cases ;

              suppose z is irreducible;

              then ( degree z) = ( max (( degree (z `1 )),( degree (z `2 )))) by Lm6;

              hence ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 )))) <= ( max (( degree (z `1 )),( degree (z `2 ))));

            end;

              suppose z is reducible;

              then ((z `1 ),(z `2 )) have_common_roots ;

              then

              consider x be Element of L such that

               A15: x is_a_common_root_of ((z `1 ),(z `2 ));

              

               A16: x is_a_root_of (z `1 ) & x is_a_root_of (z `2 ) by A15;

              consider q2 be Polynomial of L such that

               A17: (z `2 ) = (( rpoly (1,x)) *' q2) by A16, HURWITZ: 33;

              consider q1 be Polynomial of L such that

               A18: (z `1 ) = (( rpoly (1,x)) *' q1) by A16, HURWITZ: 33;

              q1 <> ( 0_. L) by Def9, A18, POLYNOM3: 34;

              then

              reconsider q1 as non zero Polynomial of L by UPROOTS:def 5;

              q2 <> ( 0_. L) by A17, POLYNOM3: 34;

              then

              reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;

              set q = [q1, q2];

              q is non zero;

              then

              reconsider q as non zero rational_function of L;

              z = [(( rpoly (1,x)) *' q1), (( rpoly (1,x)) *' q2)] by Th19, A18, A17

              .= [(( rpoly (1,x)) *' (q `1 )), (( rpoly (1,x)) *' q2)]

              .= [(( rpoly (1,x)) *' (q `1 )), (( rpoly (1,x)) *' (q `2 ))];

              then

               A19: ( NF z) = ( NF q) by Th26;

              

               A20: n <= (n + 1) by NAT_1: 11;

              

               A21: ( deg (z `1 )) = (( deg ( rpoly (1,x))) + ( deg q1)) by A18, HURWITZ: 23

              .= (1 + ( deg q1)) by HURWITZ: 27

              .= (1 + ( deg (q `1 )));

              ( deg (z `2 )) = (( deg ( rpoly (1,x))) + ( deg q2)) by A17, HURWITZ: 23

              .= (1 + ( deg q2)) by HURWITZ: 27

              .= (1 + ( deg (q `2 )));

              then

               A22: ( max (( degree (z `1 )),( degree (z `2 )))) = (1 + ( max (( degree (q `1 )),( degree (q `2 ))))) by A21, Th4;

              then ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 )))) <= ( max (( degree (q `1 )),( degree (q `2 )))) by A13, A19, A14;

              hence ( max (( degree (( NF z) `1 )),( degree (( NF z) `2 )))) <= ( max (( degree (z `1 )),( degree (z `2 )))) by A20, A22, A14, XXREAL_0: 2;

            end;

          end;

          hence P[(n + 1)];

        end;

        

         A23: for n be Nat holds P[n] from NAT_1:sch 2( A11, A12);

        ( max (( degree (z `1 )),( degree (z `2 )))) >= 0 by XXREAL_0: 25;

        then ( max (( degree (z `1 )),( degree (z `2 )))) in NAT by INT_1: 3;

        hence thesis by A5, A23;

      end;

    end;

    theorem :: RATFUNC1:30

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr holds for z be non zero rational_function of L holds z is irreducible iff ( degree z) = ( max (( degree (z `1 )),( degree (z `2 ))))

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative distributive commutative almost_left_invertible domRing-like non trivial doubleLoopStr;

      let z be non zero rational_function of L;

      set p1 = (z `1 ), p2 = (z `2 );

       A1:

      now

        assume z is irreducible;

        then

        consider a be Element of L such that

         A2: a <> ( 0. L) & [(a * (z `1 )), (a * (z `2 ))] = ( NF z) by Th28;

        

         A3: ( degree (a * (z `1 ))) = ( degree (z `1 )) by A2, POLYNOM5: 25;

        

         A4: ( degree (a * (z `2 ))) = ( degree (z `2 )) by A2, POLYNOM5: 25;

        ( degree (( NF z) `1 )) = ( degree (z `1 )) by A3, A2;

        hence ( degree z) = ( max (( degree (z `1 )),( degree (z `2 )))) by A4, A2;

      end;

      now

        assume

         A5: ( degree z) = ( max (( degree (z `1 )),( degree (z `2 ))));

        now

          assume not (z is irreducible);

          then (p1,p2) have_a_common_root ;

          then

          consider x be Element of L such that

           A6: x is_a_common_root_of (p1,p2);

          

           A7: x is_a_root_of p1 & x is_a_root_of p2 by A6;

          then

          consider q1 be Polynomial of L such that

           A8: p1 = (( rpoly (1,x)) *' q1) by HURWITZ: 33;

          consider q2 be Polynomial of L such that

           A9: p2 = (( rpoly (1,x)) *' q2) by A7, HURWITZ: 33;

          q2 <> ( 0_. L) by A9, POLYNOM3: 34;

          then

          reconsider q2 as non zero Polynomial of L by UPROOTS:def 5;

          set zz = [q1, q2];

          

           A10: (zz `1 ) = q1 & (zz `2 ) = q2;

          z = [(( rpoly (1,x)) *' (zz `1 )), (( rpoly (1,x)) *' (zz `2 ))] by Th19, A8, A9;

          then ( NF z) = ( NF zz) by Th26;

          then ( degree z) = ( degree zz);

          then

           A11: ( degree z) <= ( max (( degree q1),( degree q2))) by Th29, A10;

          now

            per cases ;

              suppose

               A12: p1 = ( 0_. L);

              

               A13: q1 = ( 0_. L) by A12, A8, Lm5;

              (( deg (( rpoly (1,x)) *' q2)) + 0 ) = (( deg ( rpoly (1,x))) + ( deg q2)) by HURWITZ: 23

              .= (1 + ( deg q2)) by HURWITZ: 27;

              then

               A14: ( deg q2) < ( deg p2) by A9, XREAL_1: 8;

              ( deg p1) <= ( deg p2) by A12, HURWITZ: 20;

              then

               A15: ( max (( deg p1),( deg p2))) = ( deg p2) by XXREAL_0:def 10;

              ( deg q1) <= ( deg q2) by A13, HURWITZ: 20;

              hence contradiction by A15, A14, A5, A11, XXREAL_0:def 10;

            end;

              suppose p1 <> ( 0_. L);

              then

              reconsider p1 as non zero Polynomial of L by UPROOTS:def 5;

              now

                assume q1 = ( 0_. L);

                then p1 = ( 0_. L) by A8, POLYNOM3: 34;

                hence contradiction;

              end;

              then

              reconsider q1 as non zero Polynomial of L by UPROOTS:def 5;

              (( deg p1) + 0 ) = (( deg ( rpoly (1,x))) + ( deg q1)) by A8, HURWITZ: 23

              .= (1 + ( deg q1)) by HURWITZ: 27;

              then

               A16: ( deg q1) < ( deg p1) by XREAL_1: 8;

              (( deg p2) + 0 ) = (( deg ( rpoly (1,x))) + ( deg q2)) by A9, HURWITZ: 23

              .= (1 + ( deg q2)) by HURWITZ: 27;

              then ( deg q2) < ( deg p2) by XREAL_1: 8;

              hence contradiction by A5, A11, A16, XXREAL_0: 27;

            end;

          end;

          hence contradiction;

        end;

        hence z is irreducible;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let L be Field;

      let z be rational_function of L;

      let x be Element of L;

      :: RATFUNC1:def19

      func eval (z,x) -> Element of L equals (( eval ((z `1 ),x)) / ( eval ((z `2 ),x)));

      coherence ;

    end

    theorem :: RATFUNC1:31

    

     Th31: for L be Field holds for x be Element of L holds ( eval (( 0._ L),x)) = ( 0. L)

    proof

      let L be Field;

      let x be Element of L;

      

      thus ( eval (( 0._ L),x)) = (( eval (( 0_. L),x)) * (( eval ((( 0._ L) `2 ),x)) " ))

      .= (( 0. L) * (( eval ((( 0._ L) `2 ),x)) " )) by POLYNOM4: 17

      .= ( 0. L);

    end;

    theorem :: RATFUNC1:32

    for L be Field holds for x be Element of L holds ( eval (( 1._ L),x)) = ( 1. L)

    proof

      let L be Field;

      let x be Element of L;

      

       A1: ( 1. L) <> ( 0. L);

      

      thus ( eval (( 1._ L),x)) = (( eval (( 1_. L),x)) * (( eval ((( 1._ L) `2 ),x)) " ))

      .= (( 1. L) * (( eval ((( 1._ L) `2 ),x)) " )) by POLYNOM4: 18

      .= (( 1. L) * (( eval (( 1_. L),x)) " ))

      .= (( 1. L) * (( 1. L) " )) by POLYNOM4: 18

      .= ( 1. L) by A1, VECTSP_1:def 10;

    end;

    theorem :: RATFUNC1:33

    for L be Field holds for p,q be rational_function of L holds for x be Element of L st ( eval ((p `2 ),x)) <> ( 0. L) & ( eval ((q `2 ),x)) <> ( 0. L) holds ( eval ((p + q),x)) = (( eval (p,x)) + ( eval (q,x)))

    proof

      let L be Field;

      let p,q be rational_function of L;

      let x be Element of L;

      assume

       A1: ( eval ((p `2 ),x)) <> ( 0. L) & ( eval ((q `2 ),x)) <> ( 0. L);

      

      thus ( eval ((p + q),x)) = (( eval ((((p `1 ) *' (q `2 )) + ((p `2 ) *' (q `1 ))),x)) * (( eval (((p + q) `2 ),x)) " ))

      .= (( eval ((((p `1 ) *' (q `2 )) + ((p `2 ) *' (q `1 ))),x)) * (( eval (((p `2 ) *' (q `2 )),x)) " ))

      .= (( eval ((((p `1 ) *' (q `2 )) + ((p `2 ) *' (q `1 ))),x)) * ((( eval ((p `2 ),x)) * ( eval ((q `2 ),x))) " )) by POLYNOM4: 24

      .= (( eval ((((p `1 ) *' (q `2 )) + ((p `2 ) *' (q `1 ))),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) by A1, VECTSP_2: 11

      .= ((( eval (((p `1 ) *' (q `2 )),x)) + ( eval (((p `2 ) *' (q `1 )),x))) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) by POLYNOM4: 19

      .= ((( eval (((p `1 ) *' (q `2 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by VECTSP_1:def 3

      .= (((( eval ((p `1 ),x)) * ( eval ((q `2 ),x))) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by POLYNOM4: 24

      .= ((( eval ((p `1 ),x)) * (( eval ((q `2 ),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by GROUP_1:def 3

      .= ((( eval ((p `1 ),x)) * ((( eval ((q `2 ),x)) * (( eval ((q `2 ),x)) " )) * (( eval ((p `2 ),x)) " ))) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by GROUP_1:def 3

      .= ((( eval ((p `1 ),x)) * (( 1. L) * (( eval ((p `2 ),x)) " ))) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by A1, VECTSP_1:def 10

      .= ((( eval ((p `1 ),x)) * (( eval ((p `2 ),x)) " )) + (( eval (((p `2 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))))

      .= ((( eval ((p `1 ),x)) * (( eval ((p `2 ),x)) " )) + ((( eval ((p `2 ),x)) * ( eval ((q `1 ),x))) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by POLYNOM4: 24

      .= ((( eval ((p `1 ),x)) * (( eval ((p `2 ),x)) " )) + (( eval ((q `1 ),x)) * (( eval ((p `2 ),x)) * ((( eval ((p `2 ),x)) " ) * (( eval ((q `2 ),x)) " ))))) by GROUP_1:def 3

      .= ((( eval ((p `1 ),x)) * (( eval ((p `2 ),x)) " )) + (( eval ((q `1 ),x)) * ((( eval ((p `2 ),x)) * (( eval ((p `2 ),x)) " )) * (( eval ((q `2 ),x)) " )))) by GROUP_1:def 3

      .= ((( eval ((p `1 ),x)) * (( eval ((p `2 ),x)) " )) + (( eval ((q `1 ),x)) * (( 1. L) * (( eval ((q `2 ),x)) " )))) by A1, VECTSP_1:def 10

      .= (( eval (p,x)) + ( eval (q,x)));

    end;

    theorem :: RATFUNC1:34

    for L be Field holds for p,q be rational_function of L holds for x be Element of L st ( eval ((p `2 ),x)) <> ( 0. L) & ( eval ((q `2 ),x)) <> ( 0. L) holds ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)))

    proof

      let L be Field;

      let p,q be rational_function of L;

      let x be Element of L;

      assume

       A1: ( eval ((p `2 ),x)) <> ( 0. L) & ( eval ((q `2 ),x)) <> ( 0. L);

      

      thus ( eval ((p *' q),x)) = (( eval (((p `1 ) *' (q `1 )),x)) * (( eval (((p *' q) `2 ),x)) " ))

      .= (( eval (((p `1 ) *' (q `1 )),x)) * (( eval (((p `2 ) *' (q `2 )),x)) " ))

      .= (( eval (((p `1 ) *' (q `1 )),x)) * ((( eval ((p `2 ),x)) * ( eval ((q `2 ),x))) " )) by POLYNOM4: 24

      .= (( eval (((p `1 ) *' (q `1 )),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) by A1, VECTSP_2: 11

      .= ((( eval ((p `1 ),x)) * ( eval ((q `1 ),x))) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " ))) by POLYNOM4: 24

      .= (( eval ((p `1 ),x)) * (( eval ((q `1 ),x)) * ((( eval ((q `2 ),x)) " ) * (( eval ((p `2 ),x)) " )))) by GROUP_1:def 3

      .= (( eval ((p `1 ),x)) * ((( eval ((p `2 ),x)) " ) * ((( eval ((q `2 ),x)) " ) * ( eval ((q `1 ),x))))) by GROUP_1:def 3

      .= (( eval (p,x)) * ( eval (q,x))) by GROUP_1:def 3;

    end;

    theorem :: RATFUNC1:35

    

     Th35: for L be Field holds for p be rational_function of L holds for x be Element of L st ( eval ((p `2 ),x)) <> ( 0. L) holds ( eval (( NormRationalFunction p),x)) = ( eval (p,x))

    proof

      let L be Field;

      let p be rational_function of L;

      let x be Element of L;

      assume

       A1: ( eval ((p `2 ),x)) <> ( 0. L);

      set np = ( NormRationalFunction p);

      

       A2: (( 1. L) / ( LC (p `2 ))) <> ( 0. L);

      

      thus ( eval (np,x)) = (( eval (((( 1. L) / ( LC (p `2 ))) * (p `1 )),x)) * (( eval ((np `2 ),x)) " ))

      .= (( eval (((( 1. L) / ( LC (p `2 ))) * (p `1 )),x)) * (( eval (((( 1. L) / ( LC (p `2 ))) * (p `2 )),x)) " ))

      .= (((( 1. L) / ( LC (p `2 ))) * ( eval ((p `1 ),x))) * (( eval (((( 1. L) / ( LC (p `2 ))) * (p `2 )),x)) " )) by POLYNOM5: 30

      .= (((( 1. L) / ( LC (p `2 ))) * ( eval ((p `1 ),x))) * (((( 1. L) / ( LC (p `2 ))) * ( eval ((p `2 ),x))) " )) by POLYNOM5: 30

      .= (((( 1. L) / ( LC (p `2 ))) * ( eval ((p `1 ),x))) * (((( 1. L) / ( LC (p `2 ))) " ) * (( eval ((p `2 ),x)) " ))) by A1, VECTSP_2: 11

      .= (( eval ((p `1 ),x)) * ((( 1. L) / ( LC (p `2 ))) * (((( 1. L) / ( LC (p `2 ))) " ) * (( eval ((p `2 ),x)) " )))) by GROUP_1:def 3

      .= (( eval ((p `1 ),x)) * (((( 1. L) / ( LC (p `2 ))) * ((( 1. L) / ( LC (p `2 ))) " )) * (( eval ((p `2 ),x)) " ))) by GROUP_1:def 3

      .= (( eval ((p `1 ),x)) * (( 1. L) * (( eval ((p `2 ),x)) " ))) by A2, VECTSP_1:def 10

      .= ( eval (p,x));

    end;

    theorem :: RATFUNC1:36

    for L be Field holds for p be rational_function of L holds for x be Element of L st ( eval ((p `2 ),x)) <> ( 0. L) holds x is_a_common_root_of ((p `1 ),(p `2 )) or ( eval (( NF p),x)) = ( eval (p,x))

    proof

      let L be Field;

      let p be rational_function of L;

      let x be Element of L;

      assume

       A1: ( eval ((p `2 ),x)) <> ( 0. L);

      assume

       A2: not (x is_a_common_root_of ((p `1 ),(p `2 )));

      per cases ;

        suppose

         A3: p is zero;

        then

         A4: (p `1 ) = ( 0_. L);

        

         A5: ( NF p) = ( 0._ L) by A3, Def17;

        

        thus ( eval (p,x)) = (( 0. L) * (( eval ((p `2 ),x)) " )) by A4, POLYNOM4: 17

        .= ( 0. L)

        .= ( eval (( NF p),x)) by A5, Th31;

      end;

        suppose p is non zero;

        then

        consider z1 be rational_function of L, z2 be non zero Polynomial of L such that

         A6: p = [(z2 *' (z1 `1 )), (z2 *' (z1 `2 ))] & z1 is irreducible & ( NF p) = ( NormRatF z1) & ex f be FinSequence of ( Polynom-Ring L) st z2 = ( Product f) & for i be Element of NAT st i in ( dom f) holds ex x be Element of L st x is_a_common_root_of ((p `1 ),(p `2 )) & (f . i) = ( rpoly (1,x)) by Def17;

        

         A7: (p `1 ) = (z2 *' (z1 `1 )) by A6;

        

         A8: (p `2 ) = (z2 *' (z1 `2 )) by A6;

         A9:

        now

          assume

           A10: ( eval (z2,x)) = ( 0. L);

          ( eval ((z2 *' (z1 `1 )),x)) = (( eval (z2,x)) * ( eval ((z1 `1 ),x))) by POLYNOM4: 24

          .= ( 0. L) by A10;

          then

           A11: x is_a_root_of (p `1 ) by A7, POLYNOM5:def 7;

          ( eval ((z2 *' (z1 `2 )),x)) = (( eval (z2,x)) * ( eval ((z1 `2 ),x))) by POLYNOM4: 24

          .= ( 0. L) by A10;

          then x is_a_root_of (p `2 ) by A8, POLYNOM5:def 7;

          hence contradiction by A2, A11;

        end;

         A12:

        now

          assume ( eval ((z1 `2 ),x)) = ( 0. L);

          

          then ( 0. L) = (( eval (z2,x)) * ( eval ((z1 `2 ),x)))

          .= ( eval ((z2 *' (z1 `2 )),x)) by POLYNOM4: 24;

          hence contradiction by A6, A1;

        end;

        ( eval (p,x)) = (( eval ((z2 *' (z1 `1 )),x)) * (( eval ((z2 *' (z1 `2 )),x)) " )) by A6

        .= ((( eval (z2,x)) * ( eval ((z1 `1 ),x))) * (( eval ((z2 *' (z1 `2 )),x)) " )) by POLYNOM4: 24

        .= ((( eval (z2,x)) * ( eval ((z1 `1 ),x))) * ((( eval (z2,x)) * ( eval ((z1 `2 ),x))) " )) by POLYNOM4: 24

        .= ((( eval (z2,x)) * ( eval ((z1 `1 ),x))) * ((( eval ((z1 `2 ),x)) " ) * (( eval (z2,x)) " ))) by A9, A12, VECTSP_2: 11

        .= (( eval (z2,x)) * (( eval ((z1 `1 ),x)) * ((( eval ((z1 `2 ),x)) " ) * (( eval (z2,x)) " )))) by GROUP_1:def 3

        .= (( eval (z2,x)) * ((( eval ((z1 `1 ),x)) * (( eval ((z1 `2 ),x)) " )) * (( eval (z2,x)) " ))) by GROUP_1:def 3

        .= ((( eval (z2,x)) * (( eval (z2,x)) " )) * (( eval ((z1 `1 ),x)) * (( eval ((z1 `2 ),x)) " ))) by GROUP_1:def 3

        .= (( 1. L) * (( eval ((z1 `1 ),x)) * (( eval ((z1 `2 ),x)) " ))) by A9, VECTSP_1:def 10

        .= ( eval (z1,x));

        hence ( eval (( NF p),x)) = ( eval (p,x)) by A6, A12, Th35;

      end;

    end;