RATFUNC1

:: Introduction to Rational Functions
::  by Christoph Schwarzweller
::
:: Received February 8, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ARYTM_3, POLYNOM2, POLYNOM1, ARYTM_1, FUNCT_1, FINSEQ_5,
      POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, GCD_1, VECTSP_1, CARD_1, ALGSEQ_1,
      ALGSTR_1, CARD_3, SGRAPH1, INT_1, FUNCT_4, ALGSTR_0, POLYNOM5, RFINSEQ,
      MCART_1, HURWITZ, ZFMISC_1, XBOOLE_0, TARSKI, YELLOW_8, LATTICES,
      XCMPLX_0, VECTSP_2, MSALIMIT, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1,
      NUMBERS, MESFUNC1, XXREAL_0, RATFUNC1, GROUP_1, FINSEQ_3, BINOP_1,
      PARTFUN1, ORDINAL4, ORDINAL1, VALUED_0;
 notations TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, PARTFUN1, XXREAL_0, NAT_D,
      GROUP_4, FUNCT_7, VECTSP_2, NUMBERS, XTUPLE_0, MCART_1, ALGSTR_0,
      ALGSTR_1, VECTSP_1, RLVECT_1, ARYTM_3, RELSET_1, FINSEQ_1, FUNCT_1,
      FUNCT_2, GROUP_1, INT_1, NAT_1, FINSEQ_3, VFUNCT_1, RFINSEQ, NORMSP_1,
      WSIERP_1,
      POLYNOM3, POLYNOM4, FINSEQ_5, POLYNOM5, STRUCT_0, ALGSEQ_1, UPROOTS,
      HURWITZ;
 constructors BINOP_1, REAL_1, SQUARE_1, VECTSP_2, POLYNOM4, POLYNOM5,
      XTUPLE_0, ALGSTR_2, HURWITZ, FUNCT_4, RELSET_1, ARYTM_3, FUNCT_7,
      GROUP_4, NAT_D, VFUNCT_1, RFINSEQ, FINSEQ_5, NAT_1, ALGSEQ_1, UPROOTS,
      WSIERP_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
      NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3,
      POLYNOM4, POLYNOM5, POLYNOM1, FUNCT_2, VFUNCT_1, CARD_1, RELAT_1,
      XTUPLE_0, UPROOTS;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
 definitions STRUCT_0, ALGSTR_0, UPROOTS;
 equalities FINSEQ_1, POLYNOM3, FINSEQ_5, HURWITZ, ALGSTR_0;
 expansions FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_2, HURWITZ, UPROOTS;
 theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1,
      VECTSP_2, INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, FUNCT_7, TARSKI, POLYNOM3,
      POLYNOM2, FUNCOP_1, POLYNOM5, XXREAL_0, FINSEQ_3, ORDINAL1, PARTFUN1,
      HURWITZ, STRUCT_0, XREAL_0, FINSEQ_4, GROUP_4, ALGSTR_0, FINSEQ_5,
      RFINSEQ, XTUPLE_0, UPROOTS;
 schemes NAT_1, INT_1;

begin :: Preliminaries

theorem Th1:
for L being add-associative right_zeroed right_complementable
            right-distributive non empty doubleLoopStr
for a being Element of L
for p,q being FinSequence of L
st len p = len q &
   for i being 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 being Element of NAT st i in dom p
           holds q/.i = a * (p/.i);
consider fq being sequence of the carrier of L such that
A2: Sum q = fq.(len q) and
A3: fq.0 = 0.L and
A4: for j being Nat, v being 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 being sequence of the carrier of L such that
A5: Sum p = fp.(len p) and
A6: fp.0 = 0.L and
A7: for j being Nat, v being 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 being 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 being 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 Th2:
for L being add-associative right_zeroed right_complementable
            right-distributive non empty doubleLoopStr
for f being FinSequence of L
for i,j being 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 being 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 being 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 Th3:
for L being add-associative right_zeroed right_complementable
            associative unital right-distributive commutative
            non empty doubleLoopStr
for f being FinSequence of L
for i being 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 being 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 Th4:
for x,y,z being 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 :: More on Polynomials

notation
let L be non empty ZeroStr;
let p be Polynomial of L;
antonym p is zero for p is non-zero;
end;

definition
::$CD
let L be non empty ZeroStr;
let p be Polynomial of L;
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 being 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 being Element of the carrier of L such that
 A2: x <> 0.L;
 set p = 0_.(L)+*(0,x);
 ex n being Nat st for i being 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 being 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 being Element of the carrier of L such that
 A2: x <> 0.L;
 set p = (0_.(L)+*(0,x))+*(1,x);
 ex n being Nat st for i being 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
for L being add-associative right_zeroed right_complementable
            right-distributive associative non empty doubleLoopStr
for p,q being Polynomial of L
for a being 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 being 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 being FinSequence of the carrier of L such that
  A2: len fr = n+1 & f.i = Sum fr &
      for k being 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 being FinSequence of the carrier of L such that
  A3: len fa = n+1 & (p *' q).i = Sum fa &
      for k being 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
for L being add-associative right_zeroed right_complementable
            right-distributive commutative associative
            non empty doubleLoopStr
for p,q being Polynomial of L
for a being 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 being 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 being FinSequence of the carrier of L such that
  A2: len fr = n+1 & f.i = Sum fr &
      for k being 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 being FinSequence of the carrier of L such that
  A3: len fa = n+1 & (p *' q).i = Sum fa &
      for k being 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,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 Th7:
for L being add-associative right_zeroed right_complementable distributive
            Abelian domRing-like non trivial doubleLoopStr
for p1,p2 being Polynomial of L
for p3 being 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,7;
 hence thesis;
 end;
end;

theorem Th8:
for L being add-associative right_zeroed right_complementable
            unital right-distributive non empty doubleLoopStr
for p being Polynomial of L st deg p = 0
for x being 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 Th9:
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative commutative distributive
            almost_left_invertible non degenerated doubleLoopStr
for p being Polynomial of L
for x being 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 Th10:
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative commutative distributive
            almost_left_invertible domRing-like
            non degenerated doubleLoopStr
for p,q being Polynomial of L
for x being 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 Th11:
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative commutative distributive
            almost_left_invertible non degenerated doubleLoopStr
for f being FinSequence of Polynom-Ring(L)
st for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being 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 being Nat st i in dom f ex z being 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 being FinSequence of Polynom-Ring(L)
st len f = $1 &
   for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being 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 being Nat st i in dom f ex z being 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 being Nat st i in dom f ex z being 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 being FinSequence, u being 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 being 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 being 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 being Nat holds P[n] from NAT_1:sch 2(A5,A6);
 len f is Nat;
hence thesis by A1,A2,A19;
end;

theorem Th12:
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative commutative distributive
            almost_left_invertible domRing-like
            non degenerated doubleLoopStr
for f being FinSequence of Polynom-Ring(L)
st for i being Nat st i in dom f ex z being Element of L st f.i = rpoly(1,z)
for p being Polynomial of L st p = Product f
for x being Element of L
holds eval(p,x) = 0.L iff
      ex i being 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 being Nat st i in dom f
            ex z being 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 being Nat st i in dom f & f.i = rpoly(1,x); then
   consider i being Nat such that
   A4: i in dom f & f.i = rpoly(1,x);
   reconsider g = Del(f,i) as FinSequence of Polynom-Ring(L);
   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 being FinSequence of Polynom-Ring(L)
  st len f = $1 & for i being Nat st i in dom f
                  ex z being Element of L st f.i = rpoly(1,z)
  for p being Polynomial of L st p = Product f
  for x being Element of L holds
  eval(p,x) = 0.L implies ex i being 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 being Nat st i in dom f
                         ex z being 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 being 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 being Nat st i in dom f
                           ex z being 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 being FinSequence, u being 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 being 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 being 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 being 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 being 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 being Nat st i in dom f & f.i = rpoly(1,x)
       by A19,A21,A22;
    end;
  end;
  hence ex i being Nat st i in dom f & f.i = rpoly(1,x);
  end;
  hence P[n+1];
  end;
A29: for n being Nat holds P[n] from NAT_1:sch 2(A11,A12);
len f is Nat;
hence ex i being Nat st i in dom f & f.i = rpoly(1,x) by A7,A1,A2,A29;
  end;
hence thesis by A3;
end;


begin :: Common Roots of Polynomials

definition
let L be unital non empty doubleLoopStr;
let p1,p2 be Polynomial of L;
let x be Element of L;
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;
pred p1,p2 have_a_common_root means
ex x being 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 Th13:
for L being Abelian add-associative right_zeroed right_complementable
            unital distributive non empty doubleLoopStr
for p being Polynomial of L
for x being 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 Th14:
for L being Abelian add-associative right_zeroed right_complementable
            unital left-distributive non empty doubleLoopStr
for p1,p2 being Polynomial of L
for x being 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
for L being Abelian add-associative right_zeroed right_complementable
            unital distributive non empty doubleLoopStr
for p1,p2 being Polynomial of L
for x being Element of L
st x is_a_common_root_of p1,p2 holds x is_a_root_of -(p1 + p2)
by Th13,Th14;

theorem
for L being Abelian add-associative right_zeroed right_complementable
            unital distributive non empty doubleLoopStr
for p,q being Polynomial of L
for x being 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
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative commutative distributive
            almost_left_invertible non trivial doubleLoopStr
for p1,p2 being 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 being Polynomial of L such that
  A4: s *' p1 = p2 by A1,HURWITZ:34;
  consider x being 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;
func Common_Roots(p,q) -> Subset of L equals
  { x where x is Element of L : x is_a_common_root_of p,q };
coherence
 proof
 set M = { x where x is Element of L : x is_a_common_root_of p,q };
 now let u be object;
   assume u in M;
   then ex x being 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 :: Normalized Polynomials

definition
let L be non empty ZeroStr;
let p be Polynomial of L;
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 Th18:
for L being add-associative right_zeroed right_complementable
            well-unital commutative associative distributive
            almost_left_invertible non empty doubleLoopStr
for p being Polynomial of L
for a being 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;
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 :: Rational Functions

definition
let L be non trivial multLoopStr_0;
mode rational_function of L -> set means :Def8:
  ex p1 being Polynomial of L st
  ex p2 being 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;
redefine func [p1,p2] -> rational_function of L;  :: redefines [ (TARSKI, definition)
coherence
 proof
   reconsider p = [p1,p2] as set by TARSKI:1;
  ex q1 being Polynomial of L st
  ex q2 being 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;
redefine func z`1 -> Polynomial of L;  :: redefines `1 (XTUPLE_0, definition)
coherence
 proof
 consider p1 being Polynomial of L such that
 A1: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
 consider p2 being non zero Polynomial of L such that
 A2: z = [p1,p2] by A1;
 thus thesis by A2;
 end;
redefine func z`2 -> non zero Polynomial of L;  :: redefines `2 (XTUPLE_0, definition)
coherence
 proof
 consider p1 being Polynomial of L such that
 A3: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
 consider p2 being 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;
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 Th19:
for L being non trivial multLoopStr_0
for z being 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 being Polynomial of L such that
A1: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being 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;
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;
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;
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;
func 0._(L) -> rational_function of L equals
  [ 0_.(L), 1_.(L) ];
coherence;
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 being 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 being 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
        for rational_function of L;
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;
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;
func p *' q -> rational_function of L equals
  [ p`1 *' q`1, p`2  *' q`2];
coherence;
end;

theorem Th20:
for L being add-associative right_zeroed right_complementable
            well-unital commutative associative distributive
            almost_left_invertible non trivial doubleLoopStr
for p being rational_function of L
for a being 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 being 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 being 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 :: Normalized Rational Functions

Lm1:
for L be Abelian add-associative right_zeroed right_complementable
             well-unital associative distributive commutative
             domRing-like non trivial doubleLoopStr
for z be rational_function of L holds
z is irreducible implies
ex z1 being rational_function of L,
   z2 being non zero Polynomial of L
  st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 Th21:
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative distributive commutative
            domRing-like non trivial doubleLoopStr
for z being rational_function of L
ex z1 being rational_function of L,
   z2 being non zero Polynomial of L
st z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
   ex f being FinSequence of Polynom-Ring(L)
   st z2 = Product f &
      for i being Element of NAT st i in dom f
      ex x being 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 being rational_function of L st max(deg(z`1),deg(z`2)) = $1
  ex z1 being rational_function of L,
     z2 being non zero Polynomial of L
  st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being 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 being 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 being rational_function of L,
     z2 being non zero Polynomial of L
  st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being rational_function of L st max(deg(z`1),deg(z`2)) = n+1
  ex z1 being rational_function of L,
     z2 being non zero Polynomial of L
  st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                   f.i = rpoly(1,x)
  proof
  let z being 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 being 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 being Polynomial of L such that
    A11: z`2 = rpoly(1,x) *' q2 by A10,HURWITZ:33;
    consider q1 being 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 being rational_function of L,
                  z2q being non zero Polynomial of L such that
    A19: q = [z2q*'z1q`1,z2q*'z1q`2] & z1q is irreducible &
        ex f being FinSequence of Polynom-Ring(L)
        st z2q = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being FinSequence of Polynom-Ring(L) such that
    A20: z2q = Product fq &
         for i being Element of NAT st i in dom fq
         ex x being 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,38;
           f.i = <*rp*>.i by A29,FINSEQ_1:def 7
              .= <*rp*>.1 by A30,TARSKI:def 1
              .= rpoly(1,x);
           hence ex x being 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 being Nat st n in dom fq & i = len<*rp*> + n;
           then consider n being 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 being 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 being 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 being 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 being 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
for z be rational_function of L st z is irreducible
for z1 being rational_function of L,
    z2 being non zero Polynomial of L
  st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                   f.i = rpoly(1,x)
for g1 being rational_function of L,
     g2 being non zero Polynomial of L
  st z = [g2*'g1`1,g2*'g1`2] & g1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st g2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being FinSequence of Polynom-Ring(L)
     st g2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                   f.i = rpoly(1,x);
consider f being FinSequence of Polynom-Ring(L) such that
     A4: z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being 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 being FinSequence of Polynom-Ring(L) such that
     A11: g2 = Product h &
        for i being Element of NAT st i in dom h
        ex x being 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 being 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
for z be non zero rational_function of L
for z1 being rational_function of L,
    z2 being non zero Polynomial of L
     st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
       ex f being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                     f.i = rpoly(1,x)
for g1 being rational_function of L,
    g2 being non zero Polynomial of L
     st z = [g2*'g1`1,g2*'g1`2] & g1 is irreducible &
        ex g being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being 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 being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being 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 being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being 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
for z1 being rational_function of L,
    z2 being non zero Polynomial of L
     st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
       ex f being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                     f.i = rpoly(1,x)
for g1 being rational_function of L,
    g2 being non zero Polynomial of L
     st z = [g2*'g1`1,g2*'g1`2] & g1 is irreducible &
        ex g being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being 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 being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being 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 being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being 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 being 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 being 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
  for z1 being rational_function of L,
      z2 being non zero Polynomial of L
     st z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
       ex f being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                     f.i = rpoly(1,x)
  for g1 being rational_function of L,
      g2 being non zero Polynomial of L
     st z = [g2*'g1`1,g2*'g1`2] & g1 is irreducible &
        ex g being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being 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 being FinSequence of Polynom-Ring(L)
       st z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                     f.i = rpoly(1,x);
  consider f being FinSequence of Polynom-Ring(L) such that
     A15: z2 = Product f &
          for i being Element of NAT st i in dom f
          ex x being 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 being FinSequence of Polynom-Ring(L)
        st g2 = Product g &
           for i being Element of NAT st i in dom g
           ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                      g.i = rpoly(1,x);

  consider g being FinSequence of Polynom-Ring(L) such that
     A17: g2 = Product g &
          for i being Element of NAT st i in dom g
          ex x being 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 being 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 being Polynomial of L such that
    A21: z`2 = rpoly(1,x) *' q2 by A20,HURWITZ:33;
    consider q1 being 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 being Element of L st
         x is_a_common_root_of z`1,z`2 & f.i = rpoly(1,x) by A15;
         hence ex z being Element of L st f.i = rpoly(1,z);
         end;
    ex i being 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 being 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 being 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 being 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 being Element of L st g.j = rpoly(1,z) by A36;
         end;
    ex j being 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 being 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 being Nat such that A41: j in dom g & g.j = rpoly(1,x);

    reconsider fq = Del(f,i) as FinSequence of Polynom-Ring(L);
    reconsider gq = Del(g,j) as FinSequence of Polynom-Ring(L);

    A42: now let k be Nat;
        assume A43: k in dom fq;
        consider m being 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 being 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 being Element of L
           st fq.k = rpoly(1,x) by A50,FINSEQ_3:110;
           end;
        suppose A51: i <= k;
           ex y being 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 being Element of L
           st fq.k = rpoly(1,x) by A51,A47,A34,A44,FINSEQ_3:111;
           end;
        end;
        hence ex x being Element of L st fq.k = rpoly(1,x);
        end;
    A52: now let k be Nat;
        assume A53: k in dom gq;
        consider m being 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 being 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 being Element of L
           st gq.k = rpoly(1,x) by A60,FINSEQ_3:110;
           end;
        suppose A61: j <= k;
           ex y being 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 being Element of L
           st gq.k = rpoly(1,x) by A61,A57,A41,A54,FINSEQ_3:111;
           end;
        end;
        hence ex x being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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;
func NF z -> rational_function of L means :Def17:
  ex z1 being rational_function of L,
     z2 being non zero Polynomial of L
  st z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
     it = NormRationalFunction z1 &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being rational_function of L,
           z2 being non zero Polynomial of L such that
  A1: z = [z2*'z1`1,z2*'z1`2] & z1 is irreducible &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being rational_function of L,
     zz2 being non zero Polynomial of L
  st nfz = NormRatF zz1 & zz1 is irreducible &
     (ex f being FinSequence of Polynom-Ring(L)
     st zz2 = Product f & z = [zz2*'zz1`1,zz2*'zz1`2] &
        for i being Element of NAT st i in dom f
        ex x being 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 being rational_function of L,
                z2 being non zero Polynomial of L such that
  A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
     NF z = NormRatF z1 &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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 being rational_function of L,
         z2 being non zero Polynomial of L such that
A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
   NF z = NormRatF z1 &
   ex f being FinSequence of Polynom-Ring(L)
   st z2 = Product f &
      for i being Element of NAT st i in dom f
      ex x being 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 being Abelian add-associative right_zeroed right_complementable
            well-unital associative distributive commutative
            almost_left_invertible domRing-like non trivial doubleLoopStr
for z being 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 being rational_function of L,
         z2 being non zero Polynomial of L such that
A1: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
    NF z = NormRatF z1 &
   ex f being FinSequence of Polynom-Ring(L)
   st z2 = Product f &
      for i being Element of NAT st i in dom f
      ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                 f.i = rpoly(1,x) by Def17;
consider f being FinSequence of Polynom-Ring(L) such that
A2: z2 = Product f & z = [z2 *' z1`1, z2 *' z1`2] &
    for i being Element of NAT st i in dom f
    ex x being 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 being 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
for L be Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z be non zero rational_function of L
for z1 being rational_function of L,
    z2 being non zero Polynomial of L
st z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
   ex f being FinSequence of Polynom-Ring(L)
   st z2 = Product f &
      for i being Element of NAT st i in dom f
      ex x being 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
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
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
for L being Abelian add-associative right_zeroed right_complementable
            well-unital associative distributive commutative
            almost_left_invertible domRing-like non trivial doubleLoopStr
for z being irreducible non zero rational_function of L
holds NF z = NormRationalFunction z by Lm4;

Lm5:
for L being Abelian add-associative right_zeroed right_complementable unital
            domRing-like left_zeroed distributive non trivial doubleLoopStr
for p1,p2 being 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 Th26:
for L be Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z be rational_function of L
for x being 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 being rational_function of L,
         z2 being non zero Polynomial of L such that
A2: z = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
    NF z = NormRatF z1 &
   ex f being FinSequence of Polynom-Ring(L)
   st z2 = Product f &
      for i being Element of NAT st i in dom f
      ex x being Element of L st x is_a_common_root_of z`1,z`2 &
                                 f.i = rpoly(1,x) by Def17;
consider f being FinSequence of Polynom-Ring(L) such that
A3: z2 = Product f &
    for i being Element of NAT st i in dom f
    ex x being 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,38;
       then i = 1 by TARSKI:def 1;
       then g.i = <*rp*>.1 by A5,FINSEQ_1:def 7
               .= rp;
       hence ex z being Element of L st g.i = rpoly(1,z);
       end;
    suppose ex n being Nat st n in dom f & i = len(<*rp*>) + n;
       then consider n being 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 being 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 being Element of L st g.i = rpoly(1,z) by A7;
       end;
    end;
  hence ex z being 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,38;
       then i = 1 by TARSKI:def 1;
       then A11: g.i = <*rp*>.1 by A10,FINSEQ_1:def 7
               .= rp;
       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 being 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 being Nat st n in dom f & i = len(<*rp*>) + n;
       then consider n being 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 being 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 being 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 being 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
for L being Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z being 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 Th28:
for L being Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non degenerated doubleLoopStr
for z being non zero rational_function of L
holds z is irreducible iff
ex a being 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 being Element of L st a <> 0.L &
                          [a * (z`1), a * (z`2)] = NF(z);
   end;
now assume
  ex a being Element of L st a <> 0.L & [a * (z`1), a * (z`2)] = NF(z);
  then consider a being 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 being 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  :: Degree of Rational Functions

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;
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 being Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z being 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 being 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 Th29:
for L being Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z being 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 being 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 being 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 being 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 being Polynomial of L such that
       A17: z`2 = rpoly(1,x) *' q2 by A16,HURWITZ:33;
       consider q1 being 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 being 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
for L being Abelian add-associative right_zeroed right_complementable
         well-unital associative distributive commutative
         almost_left_invertible domRing-like non trivial doubleLoopStr
for z being 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 being 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 being 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 being Polynomial of L such that
     A8: p1 = rpoly(1,x) *' q1 by HURWITZ:33;
     consider q2 being 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 :: Evaluation of Rational Functions

definition
let L be Field;
let z be rational_function of L;
let x be Element of L;
func eval(z,x) -> Element of L equals
  eval(z`1,x) / eval(z`2,x);
coherence;
end;

theorem Th31:
for L being Field
for x being 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
for L being Field
for x being 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
for L being Field
for p,q being rational_function of L
for x being 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
for L being Field
for p,q being rational_function of L
for x being 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 Th35:
for L being Field
for p being rational_function of L
for x being 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
for L being Field
for p being rational_function of L
for x being 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 being rational_function of L,
                z2 being non zero Polynomial of L such that
  A6: p = [z2 *' z1`1, z2 *' z1`2] & z1 is irreducible &
     NF p = NormRatF z1 &
     ex f being FinSequence of Polynom-Ring(L)
     st z2 = Product f &
        for i being Element of NAT st i in dom f
        ex x being 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;