The Mizar article:

More on Multivariate Polynomials: Monomials and Constant Polynomials

by
Christoph Schwarzweller

Received November 28, 2001

Copyright (c) 2001 Association of Mizar Users

MML identifier: POLYNOM7
[ MML identifier index ]


environ

 vocabulary POLYNOM1, POLYNOM2, POLYNOM7, BOOLE, FUNCT_1, CAT_1, TRIANG_1,
      FINSEQ_1, ALGSTR_1, ALGSTR_2, VECTSP_1, RLVECT_1, ORDINAL1, LATTICES,
      ALGSEQ_1, QUOFIELD, ORDERS_2, ANPROJ_1, QC_LANG1, FUNCOP_1, FINSET_1,
      PRE_TOPC, CAT_3, FUNCT_4, GRCAT_1, ENDALG, GROUP_1, ARYTM_3, RELAT_1,
      REALSET1, BINOP_1, FINSEQ_4, COHSP_1, VECTSP_2, BINOM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, STRUCT_0, RELAT_1,
      BINOM, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4,
      NAT_1, ALGSTR_1, RLVECT_1, ORDERS_2, FINSEQ_1, CQC_LANG, FUNCOP_1,
      GROUP_1, QUOFIELD, PRE_TOPC, GRCAT_1, ENDALG, TRIANG_1, REALSET1,
      VECTSP_2, POLYNOM1, POLYNOM2, VECTSP_1, FINSEQ_4;
 constructors ORDERS_2, CQC_LANG, WELLFND1, ALGSTR_2, QUOFIELD, BINOM, GRCAT_1,
      TRIANG_1, ENDALG, MONOID_0, POLYNOM2, MEMBERED;
 clusters STRUCT_0, FINSET_1, RELSET_1, FUNCOP_1, CQC_LANG, ORDINAL1, VECTSP_2,
      CARD_1, ALGSTR_1, BINOM, POLYNOM1, POLYNOM2, MONOID_0, VECTSP_1,
      MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 theorems TARSKI, RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1,
      VECTSP_1, POLYNOM1, PBOOLE, STRUCT_0, QUOFIELD, REAL_1, FUNCT_7, FUNCT_4,
      CQC_LANG, ENDALG, FINSEQ_4, GRCAT_1, BINOM, TRIANG_1, FINSEQ_3, RLVECT_1,
      FUNCOP_1, REALSET1, VECTSP_2, GROUP_1, FINSET_1, NAT_1, FINSEQ_2, AXIOMS,
      FSM_1, GROUP_7, FINSEQ_5, MATRLIN, POLYNOM2, XBOOLE_0, XCMPLX_1;
 schemes FUNCT_2;

begin

definition
cluster non trivial (non empty ZeroStr);
existence
proof
 consider R being non degenerated comRing;
 take R;
 thus thesis;
 end;
end;

definition
cluster non trivial -> non empty ZeroStr;
coherence
 proof
 let R be ZeroStr;
 assume R is non trivial;
 then the carrier of R is non trivial by REALSET1:def 13;
 then not(the carrier of R is empty or
          ex x being set st the carrier of R = {x}) by REALSET1:def 12;
 hence thesis by STRUCT_0:def 1;
 end;
end;

definition
cluster Abelian left_zeroed right_zeroed add-associative
        right_complementable unital associative commutative
        distributive domRing-like (non trivial doubleLoopStr);
existence
 proof
 consider R being domRing;
 take R;
 thus thesis;
 end;
end;

definition
let R be non trivial ZeroStr;
cluster non-zero Element of R;
existence
 proof
 consider a being Element of (the carrier of R)\{0.R};
   the carrier of R is non trivial by REALSET1:def 13;
 then (the carrier of R)\{0.R} is non empty by REALSET1:32;
 then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
 then reconsider a as Element of R;
 take a;
   a <> 0.R by A1,TARSKI:def 1;
 hence thesis by RLVECT_1:def 13;
 end;
end;

definition
let X be set,
    R be non empty ZeroStr,
    p be Series of X,R;
 canceled;

attr p is non-zero means :Def2:
  p <> 0_(X,R);
end;

definition
let X be set,
    R be non trivial ZeroStr;
cluster non-zero Series of X,R;
existence
 proof
 consider a being Element of (the carrier of R)\{0.R};
   the carrier of R is non trivial by REALSET1:def 13;
 then (the carrier of R)\{0.R} is non empty by REALSET1:32;
 then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
 then reconsider a as Element of R;
 set p = 0_(X,R)+*(EmptyBag X,a);
 reconsider p as Function of Bags X, the carrier of R;
 reconsider p as Function of Bags X, R;
 reconsider p as Series of X,R;
 take p;
   0_(X,R) = (Bags X --> 0.R) by POLYNOM1:def 24;
 then dom 0_(X,R) = Bags X by FUNCOP_1:19;
 then A2: p.(EmptyBag X) = a by FUNCT_7:33;
   a <> 0.R by A1,TARSKI:def 1;
 then p <> 0_(X,R) by A2,POLYNOM1:81;
 hence thesis by Def2;
 end;
end;

definition
let n be Ordinal,
    R be non trivial ZeroStr;
cluster non-zero Polynomial of n,R;
existence
 proof
 consider a being Element of (the carrier of R)\{0.R};
   the carrier of R is non trivial by REALSET1:def 13;
 then (the carrier of R)\{0.R} is non empty by REALSET1:32;
 then A1: a in the carrier of R & not(a in {0.R}) by XBOOLE_0:def 4;
 then reconsider a as Element of R;
 set p = 0_(n,R)+*(EmptyBag n,a);
 reconsider p as Function of Bags n, the carrier of R;
 reconsider p as Function of Bags n, R ;
 reconsider p as Series of n,R ;
   0_(n,R) = (Bags n --> 0.R) by POLYNOM1:def 24;
 then dom 0_(n,R) = Bags n by FUNCOP_1:19;
 then A2: p.(EmptyBag n) = a by FUNCT_7:33;
 A3: now let u be set;
    assume u in {EmptyBag n};
    then A4: u = EmptyBag n by TARSKI:def 1;
      a <> 0.R by A1,TARSKI:def 1;
    hence u in Support p by A2,A4,POLYNOM1:def 9;
    end;
   now let u be set;
    assume A5: u in Support p;
    then A6: u is Element of Bags n;
      now assume u <> EmptyBag n;
      then p.u = (0_(n,R)).u by FUNCT_7:34
              .= 0.R by A6,POLYNOM1:81;
      hence contradiction by A5,POLYNOM1:def 9;
      end;
    hence u in {EmptyBag n} by TARSKI:def 1;
    end;
 then Support p = {EmptyBag n} by A3,TARSKI:2;
 then reconsider p as Polynomial of n,R by POLYNOM1:def 10;
 take p;
   a <> 0.R by A1,TARSKI:def 1;
 then p <> 0_(n,R) by A2,POLYNOM1:81;
 hence thesis by Def2;
 end;
end;

theorem Th1:
for X being set,
    R being non empty ZeroStr,
    s being Series of X,R
holds s = 0_(X,R) iff Support s = {}
proof
let X be set,
    R be (non empty ZeroStr),
    s be Series of X,R;
A1: now assume A2: s = 0_(X,R);
     now assume A3: Support s <> {};
     consider x being Element of Support s;
     A4: x in Support s by A3;
     then reconsider x as bag of X by POLYNOM1:def 14;
       s.x <> 0.R by A4,POLYNOM1:def 9;
     hence contradiction by A2,POLYNOM1:81;
     end;
   hence Support s = {};
   end;
  now assume A5: Support s = {};
   A6: dom s = Bags X & dom 0_(X,R) = Bags X by FUNCT_2:def 1;
     now let x be set;
     assume x in Bags X;
     then reconsider x' = x as Element of Bags X;
       s.x' = 0.R by A5,POLYNOM1:def 9;
     hence s.x = (0_(X,R)).x by POLYNOM1:81;
     end;
   hence s = 0_(X,R) by A6,FUNCT_1:9;
   end;
hence thesis by A1;
end;

theorem
  for X being set,
    R being non empty ZeroStr
holds R is non trivial iff ex s being Series of X,R st Support(s) <> {}
proof
let X be set,
    R be non empty ZeroStr;
A1: now assume ex s being Series of X,R st Support(s) <> {};
then consider s being Series of X,R such that
A2: Support(s) <> {};
consider b being Element of Support s;
  b in Support s by A2;
then reconsider b as Element of Bags X;
  now assume ex x being set st the carrier of R = {x};
  then consider x being set such that
  A3: the carrier of R = {x};
    0.R = x by A3,TARSKI:def 1 .= s.b by A3,TARSKI:def 1;
  hence contradiction by A2,POLYNOM1:def 9;
  end;
then the carrier of R is non trivial by REALSET1:def 12;
hence R is non trivial by REALSET1:def 13;
end;
  now assume R is non trivial;
then A4: the carrier of R is non trivial by REALSET1:def 13;
  now assume A5: not(ex a being Element of R st a <> 0.R);
  A6: for a be Element of R holds a = 0.R by A5;
    ex x being set st the carrier of R = {x}
    proof
    take 0.R;
    A7: for u being set holds u in {0.R} implies u in the carrier of R;
      now let u be set;
      assume u in the carrier of R;
      then u = 0.R by A6;
      hence u in {0.R} by TARSKI:def 1;
      end;
    hence thesis by A7,TARSKI:2;
    end;
  hence contradiction by A4,REALSET1:def 12;
  end;
then consider a being Element of R such that
A8: a <> 0.R;
set s = (Bags X) --> a;
reconsider s as Function of Bags X,the carrier of R by FUNCOP_1:57;
reconsider s as Function of Bags X,R ;
reconsider s as Series of X,R ;
take s;
set x = EmptyBag X;
  s.x = a by FUNCOP_1:13;
then EmptyBag X in Support s by A8,POLYNOM1:def 9;
hence ex s being Series of X,R st Support(s) <> {};
end;
hence thesis by A1;
end;

definition
let X be set,
    b be bag of X;
attr b is univariate means :Def3:
  ex u being Element of X st support b = {u};
end;

definition
let X be non empty set;
cluster univariate bag of X;
existence
proof
consider x being Element of X;
set b = EmptyBag X +* (x,1);
take b;
A1: dom (x.-->1) = {x} by CQC_LANG:5;
then A2: x in dom (x.-->1) by TARSKI:def 1;
A3: dom (EmptyBag X) = X by PBOOLE:def 3;
then b.x = ((EmptyBag X)+*(x.-->1)).x by FUNCT_7:def 3;
then A4: b.x = (x.-->1).x by A2,FUNCT_4:14
      .= 1 by CQC_LANG:6;
A5: for u being set holds u in {x} implies u in support b
   proof
   let u be set;
   assume u in {x};
   then u = x by TARSKI:def 1;
   hence thesis by A4,POLYNOM1:def 7;
   end;
  for u being set holds u in support b implies u in {x}
  proof
  let u be set;
  assume A6: u in support b;
    now assume u <> x;
    then A7: not(u in dom (x.-->1)) by A1,TARSKI:def 1;
      b.u = ((EmptyBag X)+*(x.-->1)).u by A3,FUNCT_7:def 3;
    then b.u = (EmptyBag X).u by A7,FUNCT_4:12
            .= 0 by POLYNOM1:56;
    hence contradiction by A6,POLYNOM1:def 7;
    end;
  hence thesis by TARSKI:def 1;
  end;
then support b = {x} by A5,TARSKI:2;
hence thesis by Def3;
end;
end;

definition
let X be non empty set;
cluster univariate -> non empty bag of X;
coherence
proof
let b be bag of X;
assume b is univariate;
then consider x being Element of X such that
A1: support b = {x} by Def3;
  x in support b by A1,TARSKI:def 1;
then b.x <> 0 by POLYNOM1:def 7;
then b.x <> (EmptyBag X).x by POLYNOM1:56;
hence thesis by POLYNOM2:def 1;
end;
end;


::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Polynomials without Variables

begin

theorem
  for b being bag of {} holds b = EmptyBag {}
proof
let b be bag of {};
set n = {};
A1: for b being bag of n holds b = {}
     proof
     let b be bag of n;
       b in Bags n by POLYNOM1:def 14;
     hence thesis by POLYNOM1:55,TARSKI:def 1;
     end;
then EmptyBag n = {};
hence thesis by A1;
end;

Lm1:
for L being (non empty doubleLoopStr),
    p being Polynomial of {},L
holds ex a being Element of L
      st p = {EmptyBag {}} --> a
proof
let L be (non empty doubleLoopStr),
    p be Polynomial of {},L;
set n = {};
A1: for b being bag of {} holds b = {}
     proof
     let b be bag of {};
       b in Bags {} by POLYNOM1:def 14;
     hence thesis by POLYNOM1:55,TARSKI:def 1;
     end;
then A2: EmptyBag n = {};
reconsider p as Function of Bags {},L;
reconsider p as Function of {{}},the carrier of L by POLYNOM1:55;
A3: dom p = {{}} by FUNCT_2:def 1 .= {EmptyBag n} by A1;
set a = p/.{};
take a;
A4: for u being set holds u in p implies u in [:{EmptyBag n},{a}:]
    proof
    let u be set;
    assume A5: u in p;
    then consider p1,p2 being set such that
    A6: u = [p1,p2] by RELAT_1:def 1;
    A7: p1 in dom p & p2 in rng p by A5,A6,RELAT_1:def 4,def 5;
    then reconsider p1 as bag of n by A3,TARSKI:def 1;
    A8: p1 = {} by A1;
    then p2 = p.{} by A5,A6,A7,FUNCT_1:def 4
      .= p/.{} by A7,A8,FINSEQ_4:def 4;
    then p2 in {a} by TARSKI:def 1;
    hence thesis by A3,A6,A7,ZFMISC_1:def 2;
    end;
  for u being set holds u in [:{EmptyBag n},{a}:] implies u in p
  proof
  let u be set;
  assume u in [:{EmptyBag n},{a}:];
  then consider u1,u2 being set such that
  A9: u1 in {EmptyBag n} & u2 in {a} & u = [u1,u2] by ZFMISC_1:def 2;
  A10: u1 = {} by A2,A9,TARSKI:def 1;
    u2 = a by A9,TARSKI:def 1 .= p.{} by A3,A9,A10,FINSEQ_4:def 4;
  hence thesis by A3,A9,A10,FUNCT_1:8;
  end;
then p = [:{EmptyBag n},{a}:] by A4,TARSKI:2;
hence thesis by FUNCOP_1:def 2;
end;

theorem
  for L being right_zeroed add-associative right_complementable
            well-unital distributive (non trivial doubleLoopStr),
    p being Polynomial of {},L,
    x being Function of {},L
holds eval(p,x) = p.(EmptyBag{})
proof
let L be right_zeroed add-associative right_complementable
         well-unital distributive
         (non trivial doubleLoopStr),
    p be Polynomial of {},L,
    x be Function of {},L;
set n = {};
A1: for b being bag of n holds b = {}
     proof
     let b be bag of n;
       b in Bags n by POLYNOM1:def 14;
     hence thesis by POLYNOM1:55,TARSKI:def 1;
     end;
then A2: EmptyBag n = {};
consider a being Element of L such that
A3: p = {EmptyBag n} --> a by Lm1;
A4: dom p = {EmptyBag n} by A3,FUNCOP_1:19;
A5: EmptyBag n in {EmptyBag n} by TARSKI:def 1;
then A6: p.(EmptyBag n) = a by A3,FUNCOP_1:13;
  now per cases;
case A7: a = 0.L;
    Support p = {}
     proof
     assume A8: Support p <> {};
     consider u being Element of Support p;
       u in Support p by A8;
     then reconsider u as Element of Bags n;
       p.u <> 0.L by A8,POLYNOM1:def 9;
     hence thesis by A1,A2,A6,A7;
     end;
  then reconsider Sp = Support p as empty Subset of Bags n;
    BagOrder n linearly_orders Sp by POLYNOM2:20;
  then A9: SgmX(BagOrder n, Sp) = {} by POLYNOM2:9;
  consider y being FinSequence of the carrier of L such that
  A10: len y = len SgmX(BagOrder n, Support p) &
     eval(p,x) = Sum y &
     for i being Nat st 1 <= i & i <= len y holds
         y/.i = (p * SgmX(BagOrder n, Support p))/.i *
                eval(((SgmX(BagOrder n, Support p))/.i)@,x)
     by POLYNOM2:def 4;
    len y = 0 by A9,A10,FINSEQ_1:25;
  then y = <*>(the carrier of L) by FINSEQ_1:32;
  hence eval(p,x) = a by A7,A10,RLVECT_1:60;
case A11: a <> 0.L;
  A12: for u being set holds u in Support p implies u in {{}}
      proof
      let u be set;
      assume u in Support p;
      then reconsider u as Element of Bags n;
        u = {} by A1;
      hence thesis by TARSKI:def 1;
      end;
    for u being set holds u in {{}} implies u in Support p
     proof
     let u be set;
     assume u in {{}};
     then u = EmptyBag n by A2,TARSKI:def 1;
     hence thesis by A6,A11,POLYNOM1:def 9;
     end;
  then A13: Support p = {{}} by A12,TARSKI:2;
  reconsider sp = Support p as finite Subset of Bags n;
  set sg = SgmX(BagOrder n, sp);
  A14: BagOrder n linearly_orders sp by POLYNOM2:20;
  then A15: rng sg = {{}} &
      for l,m being Nat st l in dom sg & m in dom sg & l < m
      holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n)
      by A13,TRIANG_1:def 2;
  then {} in rng sg by TARSKI:def 1;
  then A16: 1 in dom sg by FINSEQ_3:33;
  then A17: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
    for u being set holds u in dom sg implies u in {1}
     proof
     let u be set;
     assume A18: u in dom sg;
     assume A19: not(u in {1});
     reconsider u as Nat by A18;
     A20: u <> 1 by A19,TARSKI:def 1;
     A21: 1 < u
        proof
        consider k being Nat such that A22: dom sg = Seg k by FINSEQ_1:def 2;
          Seg k = {m where m is Nat : 1 <= m & m <= k} by FINSEQ_1:def 1;
        then consider m' being Nat such that
        A23: m' = u & 1 <= m' & m' <= k by A18,A22;
        thus thesis by A20,A23,REAL_1:def 5;
        end;
       sg/.1 = sg.1 & sg/.u = sg.u by A16,A18,FINSEQ_4:def 4;
     then A24: sg/.1 in rng sg & sg/.u in rng sg by A16,A18,FUNCT_1:12;
     then sg/.1 = {} by A15,TARSKI:def 1 .= sg/.u by A15,A24,TARSKI:def 1;
     hence thesis by A14,A16,A18,A21,TRIANG_1:def 2;
     end;
  then dom sg = Seg 1 by A17,FINSEQ_1:4,TARSKI:2;
  then A25: len sg = 1 by FINSEQ_1:def 3;
  consider y being FinSequence of the carrier of L such that
  A26: len y = len sg &
     Sum y = eval(p,x) &
     for i being Nat st 1 <= i & i <= len y holds
       y/.i = (p * sg)/.i * eval((sg/.i)@,x) by POLYNOM2:def 4;
  A27: sg.1 in rng sg by A16,FUNCT_1:12;
    sg.1 in dom p by A2,A4,A15,A16,FUNCT_1:12;
  then 1 in dom (p * sg) by A16,FUNCT_1:21;
  then A28: (p * sg)/.1 = (p * sg).1 by FINSEQ_4:def 4
                       .= p.(sg.1) by A16,FUNCT_1:23
                       .= a by A2,A3,A15,A27,FUNCOP_1:13;
    dom y = Seg(len y) by FINSEQ_1:def 3
       .= dom sg by A26,FINSEQ_1:def 3;
  then y.1 = y/.1 by A16,FINSEQ_4:def 4
     .= (p * sg)/.1 * eval((sg/.1)@,x) by A25,A26
     .= (p * sg)/.1 * eval(EmptyBag n,x) by A1,A2
     .= (p * sg)/.1 * 1.L by POLYNOM2:16
     .= (p * sg)/.1 * 1_ L by POLYNOM2:3
     .= a by A28,VECTSP_1:def 13;
  then y = <* a *> by A25,A26,FINSEQ_1:57;
  hence eval(p,x) = a by A26,RLVECT_1:61;
  end;
hence thesis by A3,A5,FUNCOP_1:13;
end;

theorem
  for L being right_zeroed add-associative right_complementable
            well-unital distributive (non trivial doubleLoopStr)
holds Polynom-Ring({},L) is_ringisomorph_to L
proof
let L be right_zeroed add-associative right_complementable
         well-unital distributive
         (non trivial doubleLoopStr);
set n = {};
set PL = Polynom-Ring(n,L);
A1: for b being bag of {} holds b = {}
   proof
   let b be bag of {};
     b in Bags {} by POLYNOM1:def 14;
   hence thesis by POLYNOM1:55,TARSKI:def 1;
   end;
then A2: EmptyBag n = {};
then reconsider i = {} as bag of n;
defpred P[set,set] means
  ex p being Polynomial of n,L st p = $1 & p.{} = $2;
A3: for x being Element of PL
   ex y being Element of L st P[x,y]
   proof
   let x be Element of PL;
   reconsider p = x as Polynomial of n,L by POLYNOM1:def 27;
   take p.{};
     dom p = Bags n by FUNCT_2:def 1;
   then A4: p.{} in rng p by A2,FUNCT_1:12;
     rng p c= the carrier of L by RELSET_1:12;
   hence thesis by A4;
   end;
consider f being Function of the carrier of PL,the carrier of L
such that A5: for x being Element of PL holds P[x,f.x]

  from FuncExD(A3);
A6: dom f = the carrier of PL by FUNCT_2:def 1;
reconsider f as map of PL,L;
  for x,y being Element of PL holds f.(x+y) = f.x + f.y
  proof
  let x,y be Element of PL;
  consider p being Polynomial of n,L such that
  A7: p = x & p.{} = f.x by A5;
  consider q being Polynomial of n,L such that
  A8: q = y & q.{} = f.y by A5;
  consider a being Element of L such that
  A9: p = {EmptyBag n} --> a by Lm1;
  A10: EmptyBag n in {EmptyBag n} by TARSKI:def 1;
  then A11: p.{} = a by A2,A9,FUNCOP_1:13;
  consider b being Element of L such that
  A12: q = {EmptyBag n} --> b by Lm1;
    q.{} = b by A2,A10,A12,FUNCOP_1:13;
  then A13: f.x + f.y = a + b by A2,A7,A8,A9,A10,FUNCOP_1:13;
  consider pq being Polynomial of n,L such that
  A14: pq = x + y & pq.{} = f.(x+y) by A5;
    (p+q).{} = p.i + q.i by POLYNOM1:def 21 .= a + b by A2,A10,A11,A12,FUNCOP_1
:13;
  hence thesis by A7,A8,A13,A14,POLYNOM1:def 27;
  end;
then A15: f is additive by GRCAT_1:def 13;
  for x,y being Element of PL holds f.(x*y) = f.x * f.y
  proof
  let x,y be Element of PL;
  consider p being Polynomial of n,L such that
  A16: p = x & p.{} = f.x by A5;
  consider q being Polynomial of n,L such that
  A17: q = y & q.{} = f.y by A5;
  consider pq being Polynomial of n,L such that
  A18: pq = x * y & pq.{} = f.(x*y) by A5;
    (p*'q).{} = p.i * q.i
    proof
    set z = p.i * q.i;
    A19: decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> by POLYNOM1:77;
    then A20: len decomp EmptyBag n = 1 by FINSEQ_1:56;
    consider s being FinSequence of the carrier of L such that
    A21: (p*'q).(EmptyBag n) = Sum s &
        len s = len decomp EmptyBag n &
        for k being Nat st k in dom s
        ex b1, b2 being bag of n st (decomp EmptyBag n)/.k = <*b1, b2*> &
                                    s/.k = p.b1*q.b2 by POLYNOM1:def 26;
      len s = 1 by A19,A21,FINSEQ_1:56;
    then Seg 1 = dom s by FINSEQ_1:def 3;
    then A22: 1 in dom s by FINSEQ_1:4,TARSKI:def 1;
    then consider b1,b2 being bag of n such that
    A23: (decomp EmptyBag n)/.1 = <*b1, b2*> &
        s/.1 = p.b1*q.b2 by A21;
      s.1 = p.b1 * q.b2 by A22,A23,FINSEQ_4:def 4
       .= p.i * q.b2 by A1
       .= p.i * q.i by A1;
    then s = <* z *> by A20,A21,FINSEQ_1:57;
    then Sum s = z by RLVECT_1:61;
    hence thesis by A1,A21;
    end;
  hence thesis by A16,A17,A18,POLYNOM1:def 27;
  end;
then A24: f is multiplicative by ENDALG:def 7;
consider p being Polynomial of n,L such that
A25: p = 1_ PL & p.{} = f.(1_ PL) by A5;
A26: p = 1_(n,L) by A25,POLYNOM1:def 27
 .= 0_(n,L)+*(EmptyBag n,1.L) by POLYNOM1:def 25;
A27: dom 0_(n,L) = Bags n by FUNCT_2:def 1;
  dom(EmptyBag n .--> 1.L) = {EmptyBag n} by CQC_LANG:5;
then A28: EmptyBag n in dom(EmptyBag n .--> 1.L) by TARSKI:def 1;
  p.i = p.(EmptyBag n) by A1
   .= (0_(n,L)+*(EmptyBag n .--> 1.L)).(EmptyBag n) by A26,A27,FUNCT_7:def 3
   .= (EmptyBag n .--> 1.L).(EmptyBag n) by A28,FUNCT_4:14
   .= 1.L by CQC_LANG:6
   .= 1_ L by POLYNOM2:3;
then f is unity-preserving by A25,ENDALG:def 8;
then A29: f is RingHomomorphism by A15,A24,QUOFIELD:def 21;
  for x1,x2 being set
st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2
  proof
  let x1,x2 be set;
  assume A30: x1 in dom f & x2 in dom f & f.x1 = f.x2;
  then reconsider x1,x2 as Element of PL;
  consider p being Polynomial of n,L such that
  A31: p = x1 & p.{} = f.x1 by A5;
  consider q being Polynomial of n,L such that
  A32: q = x2 & q.{} = f.x2 by A5;
  consider a1 being Element of L such that
  A33: p = {EmptyBag n} --> a1 by Lm1;
  consider a2 being Element of L such that
  A34: q = {EmptyBag n} --> a2 by Lm1;
    EmptyBag n in {EmptyBag n} by TARSKI:def 1;
  then A35: p.(EmptyBag n) = a1 & q.(EmptyBag n) = a2 by A33,A34,FUNCOP_1:13;
    p.{} = p.(EmptyBag n) & q.{} = q.(EmptyBag n) by A1;
  hence thesis by A30,A31,A32,A33,A34,A35;
  end;
then f is one-to-one by FUNCT_1:def 8;
then A36: f is RingMonomorphism by A29,QUOFIELD:def 23;
  rng f c= the carrier of L by RELSET_1:12;
then A37: for u being set holds u in rng f implies u in the carrier of L;
  for u being set holds u in the carrier of L implies u in rng f
  proof
  let u be set;
  assume u in the carrier of L;
  then reconsider u as Element of L;
  set p = EmptyBag n .--> u;
  reconsider p as Function;
    dom p = {EmptyBag n} & rng p = {u} by CQC_LANG:5;
  then dom p = Bags n & rng p c= the carrier of L by POLYNOM1:55,TARSKI:def 1;
  then reconsider p as Function of Bags n, the carrier of L by FUNCT_2:4;
  reconsider p as Function of Bags n, L ;
  reconsider p as Series of n, L ;
    now per cases;
  case A38: u = 0.L;
      Support p = {}
     proof
     assume A39: Support p <> {};
     consider v being Element of Support p;
     A40: v in Support p by A39;
     then v is bag of n by POLYNOM1:def 14;
     then p.v = p.(EmptyBag n) by A1,A2 .= u by CQC_LANG:6;
     hence thesis by A38,A40,POLYNOM1:def 9;
     end;
    hence Support p is finite;
  case A41: u <> 0.L;
    A42: for v being set holds v in Support p implies v in {EmptyBag n}
        proof
        let v be set;
        assume v in Support p;
        then reconsider v as bag of n by POLYNOM1:def 14;
          v = EmptyBag n by A1,A2;
        hence thesis by TARSKI:def 1;
        end;
      for v being set holds v in {EmptyBag n} implies v in Support p
       proof
       let v be set;
       assume A43: v in {EmptyBag n};
       then reconsider v as Element of Bags n by TARSKI:def 1;
         p.v = p.(EmptyBag n) by A43,TARSKI:def 1 .= u by CQC_LANG:6;
       hence thesis by A41,POLYNOM1:def 9;
       end;
    hence Support p is finite by A42,TARSKI:2;
  end;
  then reconsider p as Polynomial of n,L by POLYNOM1:def 10;
  reconsider p' = p as Element of PL by POLYNOM1:def 27;
  consider q being Polynomial of n,L such that
  A44: q = p' & q.{} = f.p' by A5;
    q.{} = p.(EmptyBag n) by A1,A44
     .= u by CQC_LANG:6;
  hence thesis by A6,A44,FUNCT_1:12;
  end;
then rng f = the carrier of L by A37,TARSKI:2;
then f is RingEpimorphism by A29,QUOFIELD:def 22;
then f is RingIsomorphism by A36,QUOFIELD:def 24;
hence thesis by QUOFIELD:def 26;
end;

begin :: Monomials

definition
let X be set,
    L be non empty ZeroStr,
    p be Series of X,L;
attr p is monomial-like means :Def4:
  ex b being bag of X
  st for b' being bag of X st b' <> b holds p.b' = 0.L;
end;

definition
let X be set,
    L be non empty ZeroStr;
cluster monomial-like Series of X,L;
existence
 proof
 set p = 0_(X,L);
 take p;
   for b' being bag of X st b' <> EmptyBag X holds p.b' = 0.L by POLYNOM1:81;
 hence thesis by Def4;
 end;
end;

definition
let X be set,
    L be non empty ZeroStr;
mode Monomial of X,L is monomial-like Series of X,L;
end;

definition
let X be set,
    L be non empty ZeroStr;
cluster monomial-like -> finite-Support Series of X,L;
coherence
 proof
 let s be Series of X,L;
 assume s is monomial-like;
 then consider b being bag of X such that
 A1: for b' being bag of X st b' <> b holds s.b' = 0.L by Def4;
 per cases;
 suppose A2: s.b = 0.L;
     now assume Support s <> {};
     then reconsider sp = Support s as non empty Subset of Bags X;
     consider c being Element of sp;
       c in Support s;
     then s.c <> 0.L by POLYNOM1:def 9;
     hence contradiction by A1,A2;
     end;
   hence thesis by POLYNOM1:def 10;
 suppose A3: s.b <> 0.L;
   A4: now let u be set;
      assume u in {b};
      then A5: u = b by TARSKI:def 1;
      then reconsider u' = u as Element of Bags X by POLYNOM1:def 14;
        u' in Support s by A3,A5,POLYNOM1:def 9;
      hence u in Support s;
      end;
     now let u be set;
      assume A6: u in Support s;
      then reconsider u' = u as Element of Bags X;
        s.u' <> 0.L by A6,POLYNOM1:def 9;
      then u' = b by A1;
      hence u in {b} by TARSKI:def 1;
      end;
   then Support s = {b} by A4,TARSKI:2;
   hence thesis by POLYNOM1:def 10;
 end;
end;

theorem Th6:
for X being set,
    L being non empty ZeroStr,
    p being Series of X,L
holds p is Monomial of X,L iff
      (Support p = {} or ex b being bag of X st Support p = {b})
proof
let n be set,
    L be non empty ZeroStr,
    p be Series of n,L;
A1: now assume A2: Support p = {};
   consider b being bag of n;
     for b' being bag of n st b' <> b holds p.b' = 0.L
     proof
     let b' be bag of n;
     assume b' <> b;
     assume A3: p.b' <> 0.L;
     reconsider c = b' as Element of Bags n by POLYNOM1:def 14;
       c in Support p by A3,POLYNOM1:def 9;
     hence thesis by A2;
     end;
   hence p is Monomial of n,L by Def4;
   end;
A4: now assume ex b being bag of n st Support p = {b};
   then consider b being bag of n such that
   A5: Support p = {b};
     for b' being bag of n st b' <> b holds p.b' = 0.L
     proof
     let b' be bag of n;
     assume A6: b' <> b;
     assume A7: p.b' <> 0.L;
     reconsider b' as Element of Bags n by POLYNOM1:def 14;
       b' in Support p by A7,POLYNOM1:def 9;
     hence thesis by A5,A6,TARSKI:def 1;
     end;
   hence p is Monomial of n,L by Def4;
   end;
  now assume p is Monomial of n,L;
   then consider b being bag of n such that
   A8: for b' being bag of n st b' <> b holds p.b' = 0.L by Def4;
     now per cases;
   case A9: p.b <> 0.L;
   A10: for u being set holds u in Support p implies u in {b}
       proof
       let u be set;
       assume A11: u in Support p;
       then A12: p.u <> 0.L by POLYNOM1:def 9;
       reconsider u' = u as bag of n by A11,POLYNOM1:def 14;
         u' = b by A8,A12;
       hence thesis by TARSKI:def 1;
       end;
     for u being set holds u in {b} implies u in Support p
       proof
       let u be set;
       assume A13: u in {b};
       then u = b by TARSKI:def 1;
       then reconsider u' = u as Element of Bags n by POLYNOM1:def 14;
         p.u' <> 0.L by A9,A13,TARSKI:def 1;
       hence thesis by POLYNOM1:def 9;
       end;
   then Support p = {b} by A10,TARSKI:2;
   hence ex b being bag of n st Support p = {b};
   case A14: p.b = 0.L;
   thus Support p = {}
     proof
     assume Support p <> {};
     then reconsider sp = Support p as non empty Subset of Bags n;
     consider c being Element of sp;
       c in Support p;
     then p.c <> 0.L by POLYNOM1:def 9;
     hence thesis by A8,A14;
     end;
   end;
   hence Support p = {} or ex b being bag of n st Support p = {b};
   end;
hence thesis by A1,A4;
end;

definition
let X be set,
    L be non empty ZeroStr,
    a be Element of L,
    b be bag of X;
func Monom(a,b) -> Monomial of X,L equals :Def5:
  0_(X,L)+*(b,a);
coherence
 proof
 set m = 0_(X,L)+*(b,a);
 reconsider m as Function of Bags X, the carrier of L;
 reconsider m as Function of Bags X, L ;
 reconsider m as Series of X, L ;
 A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                  .= Bags X by FUNCOP_1:19;
 A2: b in Bags X by POLYNOM1:def 14;
 then A3: m = 0_(X,L)+*(b .--> a) by A1,FUNCT_7:def 3;
   dom(b .--> a) = {b} by CQC_LANG:5;
 then A4: b in dom(b .--> a) by TARSKI:def 1;
 A5: m.b = (0_(X,L)+*(b .--> a)).b by A1,A2,FUNCT_7:def 3
         .= (b .--> a).b by A4,FUNCT_4:14
         .= a by CQC_LANG:6;
   now per cases;
 case a <> 0.L;
 then b in Support m by A2,A5,POLYNOM1:def 9;
 then A6: for u being set holds u in {b} implies u in Support m by TARSKI:def 1
;
   for u being set holds u in Support m implies u in {b}
   proof
   let u be set;
   assume A7: u in Support m;
   assume not(u in {b});
   then A8: not(u in dom(b .--> a)) by CQC_LANG:5;
   reconsider u as bag of X by A7,POLYNOM1:def 14;
     m.u = (0_(X,L)).u by A3,A8,FUNCT_4:12
      .= 0.L by POLYNOM1:81;
   hence thesis by A7,POLYNOM1:def 9;
   end;
 then Support m = {b} by A6,TARSKI:2;
 hence thesis by Th6;
 case A9: a = 0.L;
   now assume Support m <> {};
    then reconsider sm = Support m as non empty Subset of Bags X;
    consider c being Element of sm;
    A10: c in Support m;
    then m.c <> 0.L by POLYNOM1:def 9;
    then not(c in {b}) by A5,A9,TARSKI:def 1;
    then A11: not(c in dom(b .--> a)) by CQC_LANG:5;
    reconsider c as bag of X;
      m.c = (0_(X,L)).c by A3,A11,FUNCT_4:12
       .= 0.L by POLYNOM1:81;
    hence contradiction by A10,POLYNOM1:def 9;
    end;
 hence thesis by Th6;
 end;
 hence thesis;
 end;
end;

definition
let X be set,
    L be non empty ZeroStr,
    m be Monomial of X,L;
func term(m) -> bag of X means :Def6:
  m.it <> 0.L or (Support m = {} & it = EmptyBag X);
existence
 proof
 consider b being bag of X such that
 A1: for b' being bag of X st b' <> b holds m.b' = 0.L by Def4;
   now per cases;
 case m.b <> 0.L;
   hence thesis;
 case A2: m.b = 0.L;
     Support m = {}
      proof
      assume Support m <> {};
      then reconsider sm = Support m as non empty Subset of Bags X;
      consider c being Element of sm;
        c in Support m;
      then m.c <> 0.L by POLYNOM1:def 9;
      hence thesis by A1,A2;
      end;
   hence thesis;
   end;
 hence thesis;
 end;
uniqueness
 proof
 let b1,b2 be bag of X;
 assume A3: m.b1 <> 0.L or (Support m = {} & b1 = EmptyBag X);
 assume A4: m.b2 <> 0.L or (Support m = {} & b2 = EmptyBag X);
 consider b being bag of X such that
 A5: for b' being bag of X st b' <> b holds m.b' = 0.L by Def4;
   now per cases;
 case A6: m.b1 <> 0.L;
   reconsider b1' = b1 as Element of Bags X by POLYNOM1:def 14;
   A7: b1' in Support m by A6,POLYNOM1:def 9;
   thus b1 = b by A5,A6 .= b2 by A4,A5,A7;
 case A8: m.b1 = 0.L;
     now per cases by A4;
   case A9: m.b2 <> 0.L;
     reconsider b2' = b2 as Element of Bags X by POLYNOM1:def 14;
       b2' in Support m by A9,POLYNOM1:def 9;
     hence b1 = b2 by A3,A8;
   case Support m = {} & b2 = EmptyBag X;
     hence b1 = b2 by A3,A8;
   end;
   hence b1 = b2;
 end;
 hence thesis;
 end;
end;

definition
let X be set,
    L be non empty ZeroStr,
    m be Monomial of X,L;
func coefficient(m) -> Element of L equals :Def7:
  m.(term(m));
coherence;
end;

theorem Th7:
for X being set,
    L being non empty ZeroStr,
    m being Monomial of X,L
holds Support(m) = {} or Support(m) = {term(m)}
proof
let X be set,
    L be non empty ZeroStr,
    m be Monomial of X,L;
assume A1: Support(m) <> {};
then consider b being bag of X such that
A2: Support(m) = {b} by Th6;
A3: m.term(m) <> 0.L by A1,Def6;
  term(m) is Element of Bags X by POLYNOM1:def 14;
then term(m) in Support(m) by A3,POLYNOM1:def 9;
hence thesis by A2,TARSKI:def 1;
end;

theorem Th8:
for X being set,
    L being non empty ZeroStr,
    b being bag of X
holds coefficient(Monom(0.L,b)) = 0.L & term(Monom(0.L,b)) = EmptyBag X
proof
let n be set,
    L be non empty ZeroStr,
    b be bag of n;
A1: Monom(0.L,b) = 0_(n,L)+*(b,0.L) by Def5;
set m = 0_(n,L)+*(b,0.L);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L ;
reconsider m as Series of n, L ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
                 .= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
then A4: m = 0_(n,L)+*(b .--> 0.L) by A2,FUNCT_7:def 3;
A5: dom(b .--> 0.L) = {b} by CQC_LANG:5;
then A6: b in dom(b .--> 0.L) by TARSKI:def 1;
A7: m.b = (0_(n,L)+*(b .--> 0.L)).b by A2,A3,FUNCT_7:def 3
        .= (b .--> 0.L).b by A6,FUNCT_4:14
        .= 0.L by CQC_LANG:6;
A8: now let b' be bag of n;
     now per cases;
   case b' = b;
     hence m.b' = 0.L by A7;
   case b' <> b;
     then not(b' in dom(b .--> 0.L)) by A5,TARSKI:def 1;
     hence m.b' = (0_(n,L)).b' by A4,FUNCT_4:12 .= 0.L by POLYNOM1:81;
   end;
   hence m.b' = 0.L;
   end;
thus coefficient(Monom(0.L,b)) = (Monom(0.L,b)).(term(Monom(0.L,b))) by Def7
                              .= 0.L by A1,A8;
  (Monom(0.L,b)).(term(Monom(0.L,b))) = 0.L by A1,A8;
hence thesis by Def6;
end;

theorem Th9:
for X being set,
    L being non empty ZeroStr,
    a being Element of L,
    b being bag of X
holds coefficient(Monom(a,b)) = a
proof
let n be set,
    L be non empty ZeroStr,
    a be Element of L,
    b be bag of n;
A1: Monom(a,b) = 0_(n,L)+*(b,a) by Def5;
set m = 0_(n,L)+*(b,a);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L ;
reconsider m as Series of n, L ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
                 .= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
  dom(b .--> a) = {b} by CQC_LANG:5;
then A4: b in dom(b .--> a) by TARSKI:def 1;
A5: m.b = (0_(n,L)+*(b .--> a)).b by A2,A3,FUNCT_7:def 3
         .= (b .--> a).b by A4,FUNCT_4:14
         .= a by CQC_LANG:6;
per cases;
suppose A6: m.b <> 0.L;
  thus coefficient(Monom(a,b)) = Monom(a,b).(term(Monom(a,b))) by Def7
                              .= a by A1,A5,A6,Def6;
suppose m.b = 0.L;
  hence thesis by A5,Th8;
end;

theorem Th10:
for X being set,
    L being non trivial ZeroStr,
    a being non-zero Element of L,
    b being bag of X
holds term(Monom(a,b)) = b
proof
let n be set,
    L be (non trivial ZeroStr),
    a be non-zero Element of L,
    b be bag of n;
A1: Monom(a,b) = 0_(n,L)+*(b,a) by Def5;
set m = 0_(n,L)+*(b,a);
reconsider m as Function of Bags n, the carrier of L;
reconsider m as Function of Bags n, L ;
reconsider m as Series of n, L ;
A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
                 .= Bags n by FUNCOP_1:19;
A3: b in Bags n by POLYNOM1:def 14;
  dom(b .--> a) = {b} by CQC_LANG:5;
then A4: b in dom(b .--> a) by TARSKI:def 1;
  m.b = (0_(n,L)+*(b .--> a)).b by A2,A3,FUNCT_7:def 3
         .= (b .--> a).b by A4,FUNCT_4:14
         .= a by CQC_LANG:6;
then m.b <> 0.L by RLVECT_1:def 13;
hence term(Monom(a,b)) = b by A1,Def6;
end;

theorem
  for X being set,
    L being non empty ZeroStr,
    m being Monomial of X,L
holds Monom(coefficient(m),term(m)) = m
proof
let X be set,
    L be (non empty ZeroStr),
    m be Monomial of X,L;
A1: dom m = Bags X & dom Monom(coefficient(m),term(m)) = Bags X
   by FUNCT_2:def 1;
per cases by Th6;
suppose A2: Support m = {};
  then A3: term(m) = EmptyBag X by Def6;
  A4: m = 0_(X,L) by A2,Th1;
  set m' = Monom(coefficient(m),term(m));
  A5: now assume coefficient(m) <> 0.L;
      then A6: m.(term(m)) <> 0.L by Def7;
        term(m) is Element of Bags X by POLYNOM1:def 14;
      hence contradiction by A2,A6,POLYNOM1:def 9;
      end;
  then A7: Monom(coefficient(m),term(m)) = 0_(X,L)+*(EmptyBag X,0.L)
    by A3,Def5;
  A8: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                   .= Bags X by FUNCOP_1:19;
  A9: dom(EmptyBag X .--> 0.L) = {EmptyBag X} by CQC_LANG:5;
  then A10: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
  A11: m'.EmptyBag X
    = (0_(X,L)+*(EmptyBag X .--> 0.L)).EmptyBag X by A7,A8,FUNCT_7:def 3
   .= (EmptyBag X .--> 0.L).EmptyBag X by A10,FUNCT_4:14
   .= 0.L by CQC_LANG:6;
    now let x be set;
    assume x in Bags X;
    then reconsider x'= x as Element of Bags X;
      now per cases;
    case x' = EmptyBag X;
      hence m'.x' = 0.L by A11;
    case x <> EmptyBag X;
      then A12: not(x' in dom(EmptyBag X .--> 0.L)) by A9,TARSKI:def 1;
        m'.x' = (0_(X,L)+*(EmptyBag X,0.L)).x' by A3,A5,Def5
           .= (0_(X,L)+*(EmptyBag X .--> 0.L)).x' by A8,FUNCT_7:def 3
           .= 0_(X,L).x' by A12,FUNCT_4:12;
      hence m'.x' = 0.L by POLYNOM1:81;
    end;
    hence m.x = m'.x by A4,POLYNOM1:81;
    end;
  hence thesis by A1,FUNCT_1:9;
suppose ex b being bag of X st Support m = {b};
  then consider b being bag of X such that
  A13: Support m = {b};
  set a = m.b;
  A14: b in Support m by A13,TARSKI:def 1;
  then a <> 0.L by POLYNOM1:def 9;
  then A15: term(m) = b by Def6;
  then A16: coefficient(m) = a by Def7;
  then A17: Monom(coefficient(m),term(m)) = 0_(X,L)+*(b,a) by A15,Def5;
  set m' = Monom(coefficient(m),term(m));
  A18: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                   .= Bags X by FUNCOP_1:19;
  A19: b in Bags X by POLYNOM1:def 14;
    dom(b .--> a) = {b} by CQC_LANG:5;
  then A20: b in dom(b .--> a) by TARSKI:def 1;
  A21: m'.b = (0_(X,L)+*(b .--> a)).b by A17,A18,A19,FUNCT_7:def 3
           .= (b .--> a).b by A20,FUNCT_4:14
           .= a by CQC_LANG:6;
  A22: now let u be set;
     assume u in {b};
     then A23: u = b by TARSKI:def 1;
       m'.b <> 0.L & b is Element of Bags X by A14,A21,POLYNOM1:def 9;
     hence u in Support(Monom(coefficient(m),term(m))) by A23,POLYNOM1:def 9;
     end;
    now let u be set;
     assume A24: u in Support(Monom(coefficient(m),term(m)));
     then reconsider u' = u as Element of Bags X;
       now assume A25: u <> b;
        A26: b in dom 0_(X,L) by A18,POLYNOM1:def 14;
          dom(b .--> a) = {b} by CQC_LANG:5;
        then A27: not(u' in dom(b .--> a)) by A25,TARSKI:def 1;
          m'.u' = (0_(X,L)+*(b,a)).u' by A15,A16,Def5
             .= (0_(X,L)+*(b .--> a)).u' by A26,FUNCT_7:def 3
             .= 0_(X,L).u' by A27,FUNCT_4:12;
        hence m'.u' = 0.L by POLYNOM1:81;
        end;
     hence u in {b} by A24,POLYNOM1:def 9,TARSKI:def 1;
     end;
  then A28: Support(Monom(coefficient(m),term(m))) = {b} by A22,TARSKI:2;
    now let x be set;
    assume x in Bags X;
    then reconsider x' = x as Element of Bags X;
      now per cases;
    case x = b;
      hence Monom(coefficient(m),term(m)).x' = m.x' by A21;
    case A29: x <> b;
      then A30: not(x in Support m) by A13,TARSKI:def 1;
           A31: not(x in Support(Monom(coefficient(m),term(m))))
        by A28,A29,TARSKI:def 1;
      thus m.x' = 0.L by A30,POLYNOM1:def 9
         .= Monom(coefficient(m),term(m)).x' by A31,POLYNOM1:def 9;
    end;
    hence m.x = Monom(coefficient(m),term(m)).x;
  end;
  hence thesis by A1,FUNCT_1:9;
end;

theorem Th12:
for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive (non trivial doubleLoopStr),
    m being Monomial of n,L,
    x being Function of n,L
holds eval(m,x) = coefficient(m) * eval(term(m),x)
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive
         (non trivial doubleLoopStr),
    m be Monomial of n,L,
    x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support m) &
    eval(m,x) = Sum y &
    for i being Nat st 1 <= i & i <= len y holds
         y/.i = (m * SgmX(BagOrder n, Support m))/.i *
                eval(((SgmX(BagOrder n, Support m))/.i)@,x)
    by POLYNOM2:def 4;
consider b being bag of n such that
A2: for b' being bag of n st b' <> b holds m.b' = 0.L by Def4;
  now per cases;
case A3: m.b <> 0.L;
A4: for u being set holds u in Support m implies u in {b}
      proof
      let u be set;
      assume A5: u in Support m;
      assume A6: not(u in {b});
      reconsider u as Element of Bags n by A5;
        u <> b by A6,TARSKI:def 1;
      then m.u = 0.L by A2;
      hence thesis by A5,POLYNOM1:def 9;
      end;
  for u being set holds u in {b} implies u in Support m
     proof
     let u be set;
     assume A7: u in {b};
     then u = b by TARSKI:def 1;
     then reconsider u as Element of Bags n by POLYNOM1:def 14;
       m.u <> 0.L by A3,A7,TARSKI:def 1;
     hence thesis by POLYNOM1:def 9;
     end;
then A8: Support m = {b} by A4,TARSKI:2;
reconsider sm = Support m as finite Subset of Bags n;
set sg = SgmX(BagOrder n, sm);
A9: BagOrder n linearly_orders sm by POLYNOM2:20;
then A10: rng sg = {b} &
    for l,m being Nat st l in dom sg & m in dom sg & l < m
    holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n) by A8,TRIANG_1:def 2;
then b in rng sg by TARSKI:def 1;
then A11: 1 in dom sg by FINSEQ_3:33;
then A12: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
  for u being set holds u in dom sg implies u in {1}
     proof
     let u be set;
     assume A13: u in dom sg;
     assume A14: not(u in {1});
     reconsider u as Nat by A13;
     A15: u <> 1 by A14,TARSKI:def 1;
     A16: 1 < u
        proof
        consider k being Nat such that A17: dom sg = Seg k by FINSEQ_1:def 2;
          Seg k = {l where l is Nat : 1 <= l & l <= k} by FINSEQ_1:def 1;
        then consider m' being Nat such that
        A18: m' = u & 1 <= m' & m' <= k by A13,A17;
        thus thesis by A15,A18,REAL_1:def 5;
        end;
       sg/.1 = sg.1 & sg/.u = sg.u by A11,A13,FINSEQ_4:def 4;
     then A19: sg/.1 in rng sg & sg/.u in rng sg by A11,A13,FUNCT_1:12;
     then sg/.1 = b by A10,TARSKI:def 1
               .= sg/.u by A10,A19,TARSKI:def 1;
     hence thesis by A9,A11,A13,A16,TRIANG_1:def 2;
     end;
then A20: dom sg = Seg 1 by A12,FINSEQ_1:4,TARSKI:2;
then A21: len sg = 1 by FINSEQ_1:def 3;
A22: 1 in dom sg by A20,FINSEQ_1:4,TARSKI:def 1;
  sg/.1 = sg.1 by A11,FINSEQ_4:def 4;
then sg/.1 in rng sg by A22,FUNCT_1:12;
then A23: sg/.1 = b by A10,TARSKI:def 1;
A24: sg.1 in rng sg by A11,FUNCT_1:12;
then A25: sg.1 = b by A10,TARSKI:def 1;
A26: b in Bags n by POLYNOM1:def 14;
  dom m = Bags n by FUNCT_2:def 1;
then 1 in dom (m * sg) by A11,A25,A26,FUNCT_1:21;
then A27: (m * sg)/.1 = (m * sg).1 by FINSEQ_4:def 4
                   .= m.(sg.1) by A11,FUNCT_1:23
                   .= m.b by A10,A24,TARSKI:def 1
                   .= m.(term(m)) by A3,Def6
                   .= coefficient(m) by Def7;
  dom y = Seg(len y) by FINSEQ_1:def 3
     .= dom sg by A1,FINSEQ_1:def 3;
then y.1 = y/.1 by A22,FINSEQ_4:def 4
   .= (m * sg)/.1 * eval((sg/.1)@,x) by A1,A21
   .= (m * sg)/.1 * eval(b,x) by A23,POLYNOM2:def 3;
then y = <* coefficient(m) * eval(b,x) *>
            by A1,A21,A27,FINSEQ_1:57;
hence eval(m,x) = coefficient(m) * eval(b,x) by A1,RLVECT_1:61
              .= coefficient(m) * eval(term(m),x) by A3,Def6;
case A28: m.b = 0.L;
A29: Support m = {}
   proof
   assume Support m <> {};
   then reconsider sm = Support m as non empty Subset of Bags n;
   consider c being Element of sm;
     c in Support m;
   then m.c <> 0.L by POLYNOM1:def 9;
   hence thesis by A2,A28;
   end;
then A30: term(m) = EmptyBag n by Def6;
  m.(EmptyBag n) = 0.L by A29,POLYNOM1:def 9;
then A31: coefficient(m) * eval(term(m),x) = 0.L * eval(term(m),x) by A30,Def7
                                        .= 0.L by VECTSP_1:39;
consider y being FinSequence of the carrier of L such that
A32: len y = len SgmX(BagOrder n, Support m) &
     eval(m,x) = Sum y &
     for i being Nat st 1 <= i & i <= len y holds
        y/.i = (m * SgmX(BagOrder n, Support m))/.i *
               eval(((SgmX(BagOrder n, Support m))/.i)@,x) by POLYNOM2:def 4;
  BagOrder n linearly_orders Support m by POLYNOM2:20;
then rng SgmX(BagOrder n, Support m) = {} by A29,TRIANG_1:def 2;
then SgmX(BagOrder n, Support m) = {} by FINSEQ_1:27;
then len y = 0 by A32,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
hence eval(m,x) = coefficient(m) * eval(term(m),x) by A31,A32,RLVECT_1:60;
end;
hence thesis;
end;

theorem
  for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive (non trivial doubleLoopStr),
    a being Element of L,
    b being bag of n,
    x being Function of n,L
holds eval(Monom(a,b),x) = a * eval(b,x)
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive
         (non trivial doubleLoopStr),
    a be Element of L,
    b be bag of n,
    x be Function of n,L;
set m = Monom(a,b);
  now per cases;
case a <> 0.L;
  then A1: a is non-zero by RLVECT_1:def 13;
  thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12
                .= a * eval(term(m),x) by Th9
                .= a * eval(b,x) by A1,Th10;
case A2: a = 0.L;
    for b' being bag of n holds m.b' = 0.L
     proof
     let b' be bag of n;
       now per cases;
     case A3: b' = b;
       A4: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 24
                        .= Bags n by FUNCOP_1:19;
       A5: b in Bags n by POLYNOM1:def 14;
       A6: m = 0_(n,L)+*(b,a) by Def5
             .= 0_(n,L)+*(b .--> a) by A4,A5,FUNCT_7:def 3;
         dom(b .--> a) = {b} by CQC_LANG:5;
       then b in dom(b .--> a) by TARSKI:def 1;
       hence m.b' = (b .--> a).b by A3,A6,FUNCT_4:14
                .= 0.L by A2,CQC_LANG:6;
     case A7: b' <> b;
       thus m.b' = 0_(n,L)+*(b,a).b' by Def5
                .= 0_(n,L).b' by A7,FUNCT_7:34
                .= 0.L by POLYNOM1:81;
     end;
     hence thesis;
     end;
  then A8: m.(term(m)) = 0.L;
  thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12
                .= m.(term(m)) * eval(term(m),x) by Def7
                .= 0.L by A8,VECTSP_1:39
                .= a * eval(b,x) by A2,VECTSP_1:39;
end;
hence thesis;
end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Constant Polynomials

begin

definition
let X be set,
    L be non empty ZeroStr,
    p be Series of X,L;
attr p is Constant means :Def8:
  for b being bag of X st b <> EmptyBag X holds p.b = 0.L;
end;

definition
let X be set,
    L be non empty ZeroStr;
cluster Constant Series of X,L;
existence
 proof
 set c = 0_(X,L);
 take c;
   for b being bag of X st b <> EmptyBag X holds c.b = 0.L by POLYNOM1:81;
 hence thesis by Def8;
 end;
end;

definition
let X be set,
    L be non empty ZeroStr;
mode ConstPoly of X,L is Constant Series of X,L;
end;

definition
let X be set,
    L be non empty ZeroStr;
cluster Constant -> monomial-like Series of X,L;
coherence
proof
let p be Series of X,L;
assume p is Constant;
then for b being bag of X st b <> EmptyBag X holds p.b = 0.L by Def8;
hence thesis by Def4;
end;
end;

theorem Th14:
for X being set,
    L being non empty ZeroStr,
    p being Series of X,L
holds p is ConstPoly of X,L iff
      (p = 0_(X,L) or Support p = {EmptyBag X})
proof
let n be set,
    L be non empty ZeroStr,
    p be Series of n,L;
A1: now assume A2: p is ConstPoly of n,L;
   A3: for u being set holds u in Support p implies u in {EmptyBag n}
      proof
      let u be set;
      assume A4: u in Support p;
      then reconsider u as Element of Bags n;
      reconsider u' = u as bag of n;
        p.u' <> 0.L by A4,POLYNOM1:def 9;
      then u' = EmptyBag n by A2,Def8;
      hence thesis by TARSKI:def 1;
      end;
   thus Support p = {EmptyBag n} or p = 0_(n,L)
     proof
     assume A5: not(Support p = {EmptyBag n});
     A6: not(EmptyBag n in Support p)
        proof
        assume EmptyBag n in Support p;
        then for u being set holds u in {EmptyBag n} implies u in Support p
          by TARSKI:def 1;
        hence thesis by A3,A5,TARSKI:2;
        end;
     A7: Support p = {}
        proof
        assume A8: Support p <> {};
        consider v being Element of Support p;
        A9: v in Support p by A8;
          v in {EmptyBag n} by A3,A8;
        hence thesis by A6,A9,TARSKI:def 1;
        end;
     A10: for b being bag of n holds p.b = 0.L
        proof
        let b be bag of n;
        assume A11: p.b <> 0.L;
          b is Element of Bags n by POLYNOM1:def 14;
        hence thesis by A7,A11,POLYNOM1:def 9;
        end;
     A12: dom p = Bags n by FUNCT_2:def 1;
     A13: for u being set holds u in rng p implies u in {0.L}
        proof
        let u be set;
        assume u in rng p;
        then consider x being set such that
        A14: x in dom p & p.x = u by FUNCT_1:def 5;
          x is bag of n by A14,POLYNOM1:def 14;
        then u = 0.L by A10,A14;
        hence thesis by TARSKI:def 1;
        end;
       for u being set holds u in {0.L} implies u in rng p
        proof
        let u be set;
        assume u in {0.L};
        then A15: u = 0.L by TARSKI:def 1;
        consider b being bag of n;
        A16: p.b = u by A10,A15;
          b in dom p by A12,POLYNOM1:def 14;
        hence thesis by A16,FUNCT_1:def 5;
        end;
     then rng p = {0.L} by A13,TARSKI:2;
     then p = (Bags n) --> 0.L by A12,FUNCOP_1:15;
     hence p = 0_(n,L) by POLYNOM1:def 24;
     end;
   end;
  now assume A17: p = 0_(n,L) or Support p = {EmptyBag n};
  per cases by A17;
  suppose p = 0_(n,L);
    then for b being bag of n st b <> EmptyBag n holds p.b = 0.L by POLYNOM1:81
;
    hence p is ConstPoly of n,L by Def8;
  suppose A18: Support p = {EmptyBag n};
      for b being bag of n st b <> EmptyBag n holds p.b = 0.L
      proof
      let b be bag of n;
      assume A19: b <> EmptyBag n;
      reconsider b as Element of Bags n by POLYNOM1:def 14;

        not(b in Support p) by A18,A19,TARSKI:def 1;
      hence thesis by POLYNOM1:def 9;
      end;
    hence p is ConstPoly of n,L by Def8;
  end;
hence thesis by A1;
end;

definition
let X be set,
    L be non empty ZeroStr;
cluster 0_(X,L) -> Constant;
coherence
 proof
   for b being bag of X st b <> EmptyBag X holds (0_(X,L)).b = 0.L
   by POLYNOM1:81;
 hence thesis by Def8;
 end;
end;

definition
let X be set,
    L be unital (non empty doubleLoopStr);
cluster 1_(X,L) -> Constant;
coherence
 proof
   for b being bag of X st b <> EmptyBag X holds (1_(X,L)).b = 0.L
   by POLYNOM1:84;
 hence thesis by Def8;
 end;
end;

Lm2:
for X being set,
    L being non empty ZeroStr,
    c being ConstPoly of X,L
holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X)
proof
let n be set,
    L be non empty ZeroStr,
    c be ConstPoly of n,L;
set eb = EmptyBag n;
A1: now per cases;
case c.eb <> 0.L;
  hence term(c) = EmptyBag n by Def6;
case A2: c.eb = 0.L;
    Support c = {}
    proof
    assume A3: Support c <> {};
    consider u being Element of Support c;
      u in Support c by A3;
    then reconsider u as Element of Bags n;
      c.u <> 0.L by A3,POLYNOM1:def 9;
    hence thesis by A2,Def8;
    end;
  hence term(c) = EmptyBag n by Def6;
end;
hence term(c) = EmptyBag n;
thus coefficient(c) = c.(EmptyBag n) by A1,Def7;
end;

theorem Th15:
for X being set,
    L being non empty ZeroStr,
    c being ConstPoly of X,L
holds Support(c) = {} or Support(c) = {EmptyBag X}
proof
let X be set,
    L be non empty ZeroStr,
    c be ConstPoly of X,L;
assume Support(c) <> {};
hence Support(c) = {term(c)} by Th7 .= {EmptyBag X} by Lm2;
end;

theorem
  for X being set,
    L being non empty ZeroStr,
    c being ConstPoly of X,L
holds term(c) = EmptyBag X & coefficient(c) = c.(EmptyBag X) by Lm2;

definition
let X be set,
    L be non empty ZeroStr,
    a be Element of L;
func a _(X,L) -> Series of X,L equals :Def9:
 0_(X,L)+*(EmptyBag X,a);
 coherence;
end;

definition
let X be set,
    L be non empty ZeroStr,
    a be Element of L;
cluster a _(X,L) -> Constant;
coherence
 proof
 set Z = 0_(X,L);
 set O = Z+*(EmptyBag X,a);
 reconsider O as Function of Bags X,the carrier of L;
 reconsider O' = O as Function of Bags X,L;
 reconsider O' as Series of X,L;
 A1: O = a _(X,L) by Def9;
   now let b be bag of X;
   assume A2: b <> EmptyBag X;
     dom(Z) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
              .= Bags X by FUNCOP_1:19;
   then A3: O' = 0_(X,L)+*(EmptyBag X .--> a) by FUNCT_7:def 3;
     dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
   then not(b in dom(EmptyBag X .--> a)) by A2,TARSKI:def 1;
   hence (O').b = (0_(X,L)).b by A3,FUNCT_4:12 .= 0.L by POLYNOM1:81;
   end;
 hence thesis by A1,Def8;
 end;
end;

Lm3: for X being set,
    L being non empty ZeroStr
holds 0.L _(X,L) = 0_(X,L)
proof
let X be set,
    L be non empty ZeroStr;
set o1 = 0.L _(X,L), o2 = 0_(X,L);
A1: Bags X = dom o1 by FUNCT_2:def 1;
A2: Bags X = dom o2 by FUNCT_2:def 1;
  now let x be set;
  assume x in Bags X;
  then reconsider x' = x as bag of X by POLYNOM1:def 14;
  A3: o2.x' = 0.L by POLYNOM1:81;
  set m = 0_(X,L)+*(EmptyBag X,0.L);
  reconsider m as Function of Bags X, the carrier of L;
  reconsider m as Function of Bags X, L ;
  reconsider m as Series of X, L ;
  A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                   .= Bags X by FUNCOP_1:19;
  then A5: m = 0_(X,L)+*(EmptyBag X .--> 0.L) by FUNCT_7:def 3;
  A6: dom(EmptyBag X .--> 0.L) = {EmptyBag X} by CQC_LANG:5;
  then A7: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1;
  A8: m.(EmptyBag X)
        = (0_(X,L)+*(EmptyBag X .--> 0.L)).(EmptyBag X) by A4,FUNCT_7:def 3
       .= (EmptyBag X .--> 0.L).(EmptyBag X) by A7,FUNCT_4:14
       .= 0.L by CQC_LANG:6;
  per cases;
  suppose x' = EmptyBag X;
    hence o1.x = o2.x by A3,A8,Def9;
  suppose x' <> EmptyBag X;
    then not(x' in dom(EmptyBag X .--> 0.L)) by A6,TARSKI:def 1;
    then m.x' = (0_(X,L)).x' by A5,FUNCT_4:12;
    hence o1.x = o2.x by Def9;
  end;
hence thesis by A1,A2,FUNCT_1:9;
end;

theorem
  for X being set,
    L being non empty ZeroStr,
    p being Series of X,L
holds p is ConstPoly of X,L iff ex a being Element of L st p = a _(X,L)
proof
let X be set,
    L be non empty ZeroStr,
    p be Series of X,L;
  now assume A1: p is ConstPoly of X,L;
     now per cases by A1,Th14;
   case p = 0_(X,L);
     then p = 0.L _(X,L) by Lm3;
     hence ex a being Element of L st p = a _(X,L);
   case A2: Support p = {EmptyBag X};
     set q = 0_(X,L)+*(EmptyBag X,p.(EmptyBag X));
     A3: q = p.(EmptyBag X) _(X,L) by Def9;
     A4: Bags X = dom p by FUNCT_2:def 1;
     A5: Bags X = dom q by FUNCT_2:def 1;
       now let x be set;
       assume x in Bags X;
       then reconsider x' = x as bag of X by POLYNOM1:def 14;
       A6: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                        .= Bags X by FUNCOP_1:19;
       then A7: q = 0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X)) by FUNCT_7:def 3;
       A8: dom(EmptyBag X .--> p.(EmptyBag X)) = {EmptyBag X} by CQC_LANG:5;
       then A9: EmptyBag X in dom(EmptyBag X .--> p.(EmptyBag X))
                 by TARSKI:def 1;
       A10: q.(EmptyBag X)
              = (0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X))).(EmptyBag X)
                by A6,FUNCT_7:def 3
             .= (EmptyBag X .--> p.(EmptyBag X)).(EmptyBag X)
                by A9,FUNCT_4:14
             .= p.(EmptyBag X) by CQC_LANG:6;
         now per cases;
       case x' = EmptyBag X;
         hence p.x = q.x by A10;
       case A11: x' <> EmptyBag X;
         then not(x' in dom(EmptyBag X .--> p.(EmptyBag X)))
                by A8,TARSKI:def 1;
         then A12: q.x' = (0_(X,L)).x' by A7,FUNCT_4:12;
         A13: not(x' in Support p) by A2,A11,TARSKI:def 1;
           x' is Element of Bags X by POLYNOM1:def 14;
         then p.x' = 0.L by A13,POLYNOM1:def 9;
         hence p.x = q.x by A12,POLYNOM1:81;
       end;
       hence p.x = q.x;
       end;
     then p = q by A4,A5,FUNCT_1:9;
     hence ex a being Element of L st p = a _(X,L) by A3;
   end;
   hence ex a being Element of L st p = a _(X,L);
   end;
hence thesis;
end;

theorem Th18:
for X being set,
    L being non empty multLoopStr_0,
    a being Element of L
holds (a _(X,L)).EmptyBag X = a &
      for b being bag of X st b <> EmptyBag X holds (a _(X,L)).b = 0.L
proof
let n be set,
    L be non empty multLoopStr_0,
    a be Element of L;
set Z = 0_(n,L);
A1: Z = (Bags n --> 0.L) by POLYNOM1:def 24;
then A2: dom Z = Bags n by FUNCOP_1:19;
A3: Z+*(EmptyBag n,a) = a _(n,L) by Def9;
hence (a _(n,L)).EmptyBag n = a by A2,FUNCT_7:33;
let b be bag of n;
assume A4: b <> EmptyBag n;
A5: b in Bags n by POLYNOM1:def 14;
thus (a _(n,L)).b = Z.b by A3,A4,FUNCT_7:34 .= 0.L by A1,A5,FUNCOP_1:13;
end;

theorem
  for X being set,
    L being non empty ZeroStr
holds 0.L _(X,L) = 0_(X,L) by Lm3;

theorem
  for X being set,
    L being unital (non empty multLoopStr_0)
holds 1.L _(X,L) = 1_(X,L)
proof
let X be set,
    L be unital (non empty multLoopStr_0);
set o1 = 1.L _(X,L), o2 = 1_(X,L);
A1: Bags X = dom o1 by FUNCT_2:def 1;
A2: Bags X = dom o2 by FUNCT_2:def 1;
  now let x be set;
  assume x in Bags X;
  then reconsider x' = x as bag of X by POLYNOM1:def 14;
  set m = 0_(X,L)+*(EmptyBag X,1.L);
  reconsider m as Function of Bags X, the carrier of L;
  reconsider m as Function of Bags X, L ;
  reconsider m as Series of X, L ;
  A3: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                   .= Bags X by FUNCOP_1:19;
  then A4: m = 0_(X,L)+*(EmptyBag X .--> 1.L) by FUNCT_7:def 3;
  A5: dom(EmptyBag X .--> 1.L) = {EmptyBag X} by CQC_LANG:5;
  then A6: EmptyBag X in dom(EmptyBag X .--> 1.L) by TARSKI:def 1;
  A7: m.(EmptyBag X)
        = (0_(X,L)+*(EmptyBag X .--> 1.L)).(EmptyBag X) by A3,FUNCT_7:def 3
       .= (EmptyBag X .--> 1.L).(EmptyBag X) by A6,FUNCT_4:14
       .= 1.L by CQC_LANG:6;
  per cases;
  suppose A8: x' = EmptyBag X;
    hence o1.x = 1.L by A7,Def9 .= o2.x by A8,POLYNOM1:84;
  suppose A9: x' <> EmptyBag X;
    then not(x' in dom(EmptyBag X .--> 1.L)) by A5,TARSKI:def 1;
    then m.x' = (0_(X,L)).x' by A4,FUNCT_4:12
             .= 0.L by POLYNOM1:81
             .= o2.x' by A9,POLYNOM1:84;
    hence o1.x = o2.x by Def9;
  end;
hence thesis by A1,A2,FUNCT_1:9;
end;

theorem
  for X being set,
    L being non empty ZeroStr,
    a,b being Element of L
holds a _(X,L) = b _(X,L) iff a = b
proof
let X be set,
    L be non empty ZeroStr,
    a,b be Element of L;
set m = 0_(X,L)+*(EmptyBag X,a);
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L ;
reconsider m as Series of X, L ;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                 .= Bags X by FUNCOP_1:19;
  dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
then A2: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
A3: m.(EmptyBag X)
         = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by A1,FUNCT_7:def 3
        .= (EmptyBag X .--> a).(EmptyBag X) by A2,FUNCT_4:14
        .= a by CQC_LANG:6;
set k = 0_(X,L)+*(EmptyBag X,b);
reconsider k as Function of Bags X, the carrier of L;
reconsider k as Function of Bags X, L ;
reconsider k as Series of X, L ;
A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                 .= Bags X by FUNCOP_1:19;
  dom(EmptyBag X .--> b) = {EmptyBag X} by CQC_LANG:5;
then A5: EmptyBag X in dom(EmptyBag X .--> b) by TARSKI:def 1;
A6: k.(EmptyBag X)
         = (0_(X,L)+*(EmptyBag X .--> b)).(EmptyBag X) by A4,FUNCT_7:def 3
        .= (EmptyBag X .--> b).(EmptyBag X) by A5,FUNCT_4:14
        .= b by CQC_LANG:6;
  m = a _(X,L) & k = b _(X,L) by Def9;
hence thesis by A3,A6;
end;

theorem
  for X being set,
    L being non empty ZeroStr,
    a being Element of L
holds Support(a _(X,L)) = {} or Support(a _(X,L)) = {EmptyBag X} by Th15;

theorem Th23:
for X being set,
    L being non empty ZeroStr,
    a being Element of L
holds term(a _(X,L)) = EmptyBag X & coefficient(a _(X,L)) = a
proof
let X be set,
    L be non empty ZeroStr,
    a be Element of L;
set m = 0_(X,L)+*(EmptyBag X,a);
reconsider m as Function of Bags X, the carrier of L;
reconsider m as Function of Bags X, L ;
reconsider m as Series of X, L ;
A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 24
                 .= Bags X by FUNCOP_1:19;
  dom(EmptyBag X .--> a) = {EmptyBag X} by CQC_LANG:5;
then A2: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1;
A3: m.(EmptyBag X)
         = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by A1,FUNCT_7:def 3
        .= (EmptyBag X .--> a).(EmptyBag X) by A2,FUNCT_4:14
        .= a by CQC_LANG:6;
  coefficient(a _(X,L)) = (a _(X,L)).(EmptyBag X) by Lm2
                     .= a by A3,Def9;
hence thesis by Lm2;
end;

theorem Th24:
for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive (non trivial doubleLoopStr),
    c being ConstPoly of n,L,
    x being Function of n,L
holds eval(c,x) = coefficient(c)
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive
         (non trivial doubleLoopStr),
    c be ConstPoly of n,L,
    x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support c) &
    eval(c,x) = Sum y &
    for i being Nat st 1 <= i & i <= len y holds
        y/.i = (c * SgmX(BagOrder n, Support c))/.i *
               eval(((SgmX(BagOrder n, Support c))/.i)@,x)
    by POLYNOM2:def 4;
  now per cases;
case A2: coefficient(c) = 0.L;
    Support c = {}
     proof
     assume A3: Support c <> {};
     consider u being Element of Support c;
       u in Support c by A3;
     then reconsider u as Element of Bags n;
       c.u <> 0.L by A3,POLYNOM1:def 9;
     then u <> EmptyBag n by A2,Lm2;
     then c.u = 0.L by Def8;
     hence thesis by A3,POLYNOM1:def 9;
     end;
  then reconsider Sc = Support c as empty Subset of Bags n;
    BagOrder n linearly_orders Sc by POLYNOM2:20;
  then SgmX(BagOrder n, Sc) = {} by POLYNOM2:9;
  then len y = 0 by A1,FINSEQ_1:25;
  then y = <*>(the carrier of L) by FINSEQ_1:32;
  hence eval(c,x) = coefficient(c) by A1,A2,RLVECT_1:60;
case A4: coefficient(c) <> 0.L;
  A5: for u being set holds u in Support c implies u in {EmptyBag n}
      proof
      let u be set;
      assume A6: u in Support c;
      assume A7: not(u in {EmptyBag n});
      reconsider u as Element of Bags n by A6;
        u <> EmptyBag n by A7,TARSKI:def 1;
      then c.u = 0.L by Def8;
      hence thesis by A6,POLYNOM1:def 9;
      end;
    for u being set holds u in {EmptyBag n} implies u in Support c
     proof
     let u be set;
     assume A8: u in {EmptyBag n};
     then A9: u = EmptyBag n by TARSKI:def 1;
     reconsider u as Element of Bags n by A8,TARSKI:def 1;
       c.u <> 0.L by A4,A9,Lm2;
     hence thesis by POLYNOM1:def 9;
     end;
  then A10: Support c = {EmptyBag n} by A5,TARSKI:2;
  reconsider sc = Support c as finite Subset of Bags n;
  set sg = SgmX(BagOrder n, sc);
  A11: BagOrder n linearly_orders sc by POLYNOM2:20;
  then A12: rng sg = {EmptyBag n} &
    for l,m being Nat st l in dom sg & m in dom sg & l < m
    holds sg/.l <> sg/.m & [sg/.l,sg/.m] in (BagOrder n) by A10,TRIANG_1:def 2;
  then EmptyBag n in rng sg by TARSKI:def 1;
  then A13: 1 in dom sg by FINSEQ_3:33;
  then A14: for u being set holds u in {1} implies u in dom sg by TARSKI:def 1;
    for u being set holds u in dom sg implies u in {1}
     proof
     let u be set;
     assume A15: u in dom sg;
     assume A16: not(u in {1});
     reconsider u as Nat by A15;
     A17: u <> 1 by A16,TARSKI:def 1;
     A18: 1 < u
        proof
        consider k being Nat such that A19: dom sg = Seg k by FINSEQ_1:def 2;
          Seg k = {m where m is Nat : 1 <= m & m <= k} by FINSEQ_1:def 1;
        then consider m' being Nat such that
        A20: m' = u & 1 <= m' & m' <= k by A15,A19;
        thus thesis by A17,A20,REAL_1:def 5;
        end;
       sg/.1 = sg.1 & sg/.u = sg.u by A13,A15,FINSEQ_4:def 4;
     then A21: sg/.1 in rng sg & sg/.u in rng sg by A13,A15,FUNCT_1:12;
     then sg/.1 = EmptyBag n by A12,TARSKI:def 1
               .= sg/.u by A12,A21,TARSKI:def 1;
     hence thesis by A11,A13,A15,A18,TRIANG_1:def 2;
     end;
  then A22: dom sg = Seg 1 by A14,FINSEQ_1:4,TARSKI:2;
  then A23: len sg = 1 by FINSEQ_1:def 3;
  A24: 1 in dom sg by A22,FINSEQ_1:4,TARSKI:def 1;
    sg/.1 = sg.1 by A13,FINSEQ_4:def 4;
  then sg/.1 in rng sg by A24,FUNCT_1:12;
  then A25: sg/.1 = EmptyBag n by A12,TARSKI:def 1;
  A26: sg.1 in rng sg by A13,FUNCT_1:12;
  then A27: sg.1 = EmptyBag n by A12,TARSKI:def 1;
    dom c = Bags n by FUNCT_2:def 1;
  then 1 in dom (c * sg) by A13,A27,FUNCT_1:21;
  then A28: (c * sg)/.1 = (c * sg).1 by FINSEQ_4:def 4
                       .= c.(sg.1) by A13,FUNCT_1:23
                       .= c.(EmptyBag n) by A12,A26,TARSKI:def 1
                       .= coefficient(c) by Lm2;
    dom y = Seg(len y) by FINSEQ_1:def 3
       .= dom sg by A1,FINSEQ_1:def 3;
  then y.1 = y/.1 by A24,FINSEQ_4:def 4
     .= (c * sg)/.1 * eval((sg/.1)@,x) by A1,A23
     .= coefficient(c) * eval(EmptyBag n,x) by A25,A28,POLYNOM2:def 3
     .= coefficient(c) * 1. L by POLYNOM2:16
     .= coefficient(c) by GROUP_1:def 4;
  then y = <* coefficient(c) *> by A1,A23,FINSEQ_1:57;
  hence eval(c,x) = coefficient(c) by A1,RLVECT_1:61;
end;
hence thesis;
end;

theorem Th25:
for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive (non trivial doubleLoopStr),
    a being Element of L,
    x being Function of n,L
holds eval(a _(n,L),x) = a
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive
         (non trivial doubleLoopStr),
    a be Element of L,
    x be Function of n,L;
thus eval(a _(n,L),x) = coefficient(a _(n,L)) by Th24 .= a by Th23;
end;


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Multiplication with Coefficients

begin

definition
let X be set,
    L be non empty multLoopStr_0,
    p be Series of X,L,
    a be Element of L;
func a * p -> Series of X,L means :Def10:
  for b being bag of X holds it.b = a * p.b;
existence
 proof
 deffunc F(Element of Bags X) = a * p.$1;
 consider f being Function of Bags X, the carrier of L such that
 A1: for x being Element of Bags X holds f.x = F(x) from LambdaD;
 reconsider f as Function of Bags X,L ;
 reconsider f as Series of X,L ;
 reconsider f as Series of X,L;
 take f;
 let x be bag of X;
   x in Bags X by POLYNOM1:def 14;
 hence thesis by A1;
 end;
uniqueness
 proof
 let p1,p2 be Series of X,L such that
 A2: for b being bag of X holds p1.b = a * p.b and
 A3: for b being bag of X holds p2.b = a * p.b;
   now let b be Element of Bags X;
   reconsider b' = b as bag of X;
   thus p1.b = a * p.b' by A2 .= p2.b by A3;
   end;
 hence p1 = p2 by FUNCT_2:113;
 end;
func p * a -> Series of X,L means :Def11:
  for b being bag of X holds it.b = p.b * a;
existence
 proof
 deffunc F(Element of Bags X) = p.$1 * a;
 consider f being Function of Bags X, the carrier of L such that
 A4: for x being Element of Bags X holds f.x = F(x) from LambdaD;
 reconsider f as Function of Bags X,L ;
 reconsider f as Series of X,L ;
 reconsider f as Series of X,L;
 take f;
 let x be bag of X;
   x in Bags X by POLYNOM1:def 14;
 hence thesis by A4;
 end;
uniqueness
 proof
 let p1,p2 be Series of X,L such that
 A5: for b being bag of X holds p1.b = p.b * a and
 A6: for b being bag of X holds p2.b = p.b * a;
   now let b be Element of Bags X;
   reconsider b' = b as bag of X;
   thus p1.b = p.b' * a by A5 .= p2.b by A6;
   end;
 hence p1 = p2 by FUNCT_2:113;
 end;
end;

definition
let X be set,
    L be left_zeroed right_zeroed add-cancelable
         distributive (non empty doubleLoopStr),
    p be finite-Support Series of X,L,
    a be Element of L;
cluster a * p -> finite-Support;
coherence
 proof
 set ap = a * p;
 A1: Support p is finite by POLYNOM1:def 10;
   now
     now let u be set;
     assume A2: u in Support ap;
     then A3: ap.u <> 0.L by POLYNOM1:def 9;
     reconsider u' = u as Element of Bags X by A2;
       a * p.u' <> 0.L by A3,Def10;
     then p.u' <> 0.L by BINOM:2;
     hence u in Support p by POLYNOM1:def 9;
     end;
   then Support ap c= Support p by TARSKI:def 3;
   then Support ap is finite by A1,FINSET_1:13;
   hence thesis by POLYNOM1:def 10;
 end;
 hence thesis;
 end;
cluster p * a -> finite-Support;
coherence
 proof
 set ap = p * a;
 A4: Support p is finite by POLYNOM1:def 10;
   now
  let u be set;
     assume A5: u in Support ap;
     then A6: ap.u <> 0.L by POLYNOM1:def 9;
     reconsider u' = u as Element of Bags X by A5;
       p.u' * a <> 0.L by A6,Def11;
     then p.u' <> 0.L by BINOM:1;
     hence u in Support p by POLYNOM1:def 9;
     end;
   then Support ap c= Support p by TARSKI:def 3;
   then Support ap is finite by A4,FINSET_1:13;
   hence thesis by POLYNOM1:def 10;
end;
end;

theorem
  for X being set,
    L being commutative (non empty multLoopStr_0),
    p being Series of X,L,
    a being Element of L
holds a * p = p * a
proof
let n be set,
    L be commutative (non empty multLoopStr_0),
    p be Series of n,L,
    a be Element of L;
  now let b be Element of Bags n;
   reconsider b' = b as bag of n;
   thus (a * p).b = a * p.b' by Def10
                 .= (p * a).b by Def11;
   end;
hence a * p = p * a by FUNCT_2:113;
end;

theorem Th27:
for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            left-distributive (non empty doubleLoopStr),
    p being Series of n,L,
    a being Element of L
holds a * p = a _(n,L) *' p
proof
let n be Ordinal,
    L be add-associative right_complementable left-distributive
         right_zeroed (non empty doubleLoopStr),
    p be Series of n,L,
    a be Element of L;
A1: Bags n = dom(a * p) by FUNCT_2:def 1;
A2: Bags n = dom(a _(n,L) *' p) by FUNCT_2:def 1;
  for x being set st x in Bags n holds (a * p).x = (a _(n,L) *' p).x
  proof
  let x be set;
  assume x in Bags n;
  then reconsider b = x as bag of n by POLYNOM1:def 14;
  A3: b is Element of Bags n by POLYNOM1:def 14;
  set O = a _(n,L), cL = the carrier of L;
    for b being Element of Bags n holds (a _(n,L) *' p).b = a * p.b
    proof
    let b be Element of Bags n;
    consider s being FinSequence of cL such that
    A4: (O*'p).b = Sum s and
    A5: len s = len decomp b and
    A6: for k being Nat st k in dom s
        ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*>
             & s/.k = (O.b1)*(p.b2) by POLYNOM1:def 26;
    A7: len s <> 0 by A5,FINSEQ_1:25;
    then s is non empty by FINSEQ_1:25;
    then consider s1 being Element of cL, t being FinSequence of cL such that
    A8: s1 = s.1 and
    A9: s = <*s1*>^t by FSM_1:5;
    A10: Sum s = (Sum <*s1*>) + (Sum t) by A9,RLVECT_1:58;
      s is non empty by A7,FINSEQ_1:25;
    then A11: 1 in dom s by FINSEQ_5:6;
    then consider b1, b2 being bag of n such that
    A12: (decomp b)/.1 = <*b1, b2*> and
    A13: s/.1 = O.b1*p.b2 by A6;
      (decomp b)/.1 = <*EmptyBag n, b*> by POLYNOM1:75;
    then A14: b2 = b & b1 = EmptyBag n by A12,GROUP_7:2;
    A15: s/.1 = s.1 by A11,FINSEQ_4:def 4;
    A16: Sum <*s1*> = s1 by RLVECT_1:61
       .= a * p.b by A8,A13,A14,A15,Th18;
      now per cases;
    suppose t = <*>(cL);
      hence (Sum t) = 0.L by RLVECT_1:60;
    suppose A17: t <> <*>(cL);
        now let k be Nat;
      assume A18: k in dom t;
      then A19: t/.k = t.k by FINSEQ_4:def 4
                    .= s.(k+1) by A9,A18,FSM_1:6;
        1 <= k by A18,FINSEQ_3:27;
      then A20: 1 < k+1 by NAT_1:38;
      A21: dom s = dom decomp b by A5,FINSEQ_3:31;
      A22: len s = len t + len <*s1*> by A9,FINSEQ_1:35
                .= len t +1 by FINSEQ_1:56;
        k <= len t by A18,FINSEQ_3:27;
      then A23: k+1 <= len s by A22,AXIOMS:24;
      then A24: k+1 in dom decomp b by A5,A20,FINSEQ_3:27;
      then A25: s/.(k+1) = s.(k+1) by A21,FINSEQ_4:def 4;
      per cases by A23,AXIOMS:21;
      suppose A26: k+1 < len s;
        consider b1, b2 being bag of n such that
        A27: (decomp b)/.(k+1) = <*b1, b2*> and
        A28: s/.(k+1) = O.b1*p.b2 by A6,A21,A24;
          b1 <> EmptyBag n by A5,A20,A26,A27,POLYNOM1:76;
        hence t/.k = 0.L*p.b2 by A19,A25,A28,Th18
                    .= 0.L by VECTSP_1:39;
      suppose A29: k+1 = len s;
        consider b1, b2 being bag of n such that
        A30: (decomp b)/.(k+1) = <*b1, b2*> and
        A31: s/.(k+1) = O.b1*p.b2 by A6,A21,A24;
          (decomp b)/.(len s) = <*b,EmptyBag n*> by A5,POLYNOM1:75;
        then A32: b2 = EmptyBag n & b1 = b by A29,A30,GROUP_7:2;
          now assume b = EmptyBag n;
             then decomp b = <* <*EmptyBag n, EmptyBag n*> *>
               by POLYNOM1:77;
             then len t +1 = 0+1 by A5,A22,FINSEQ_1:56;
             then len t = 0 by XCMPLX_1:2;
             hence contradiction by A17,FINSEQ_1:25;
             end;
        then s.(k+1) = 0.L*(p.EmptyBag n) by A25,A31,A32,Th18
              .= 0.L by VECTSP_1:39;
        hence t/.k = 0.L by A19;
      end;
      hence Sum t = 0.L by MATRLIN:15;
      end;
    hence (O*'p).b = a * p.b by A4,A10,A16,RLVECT_1:10;
    end;
  then (O*'p).b = a * p.b by A3 .= (a * p).b by Def10;
  hence (O*'p).x = (a * p).x;
  end;
hence thesis by A1,A2,FUNCT_1:9;
end;

theorem Th28:
for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            right-distributive (non empty doubleLoopStr),
    p being Series of n,L,
    a being Element of L
holds p * a = p *' (a _(n,L))
proof
let n be Ordinal,
    L be add-associative right_complementable right-distributive
         right_zeroed (non empty doubleLoopStr),
    p be Series of n,L,
    a be Element of L;
A1: Bags n = dom(p * a) by FUNCT_2:def 1;
A2: Bags n = dom(p *' (a _(n,L))) by FUNCT_2:def 1;
  for x being set st x in Bags n holds (p * a).x = (p *' (a _(n,L))).x
  proof
  let x be set;
  assume x in Bags n;
  then reconsider b = x as bag of n by POLYNOM1:def 14;
  A3: b is Element of Bags n by POLYNOM1:def 14;
  set O = a _(n,L), cL = the carrier of L;
    for b being Element of Bags n holds (p *' (a _(n,L))).b = p.b * a
    proof
    let b be Element of Bags n;
    consider s being FinSequence of cL such that
    A4: (p*'O).b = Sum s and
    A5: len s = len decomp b and
    A6: for k being Nat st k in dom s
        ex b1,b2 being bag of n st (decomp b)/.k = <*b1, b2*>
             & s/.k = (p.b1)*(O.b2) by POLYNOM1:def 26;
    A7: len s <> 0 by A5,FINSEQ_1:25;
    then consider t being FinSequence of cL,s1 being Element of cL such that
    A8: s = t^<*s1*> by FINSEQ_2:22;
    A9: Sum s = (Sum t) + (Sum <*s1*>) by A8,RLVECT_1:58;
      s is non empty by A7,FINSEQ_1:25;
    then A10: len s in dom s by FINSEQ_5:6;
    then consider b1, b2 being bag of n such that
    A11: (decomp b)/.len s = <*b1, b2*> and
    A12: s/.len s = p.b1*O.b2 by A6;
      (decomp b)/.len s = <*b,EmptyBag n*> by A5,POLYNOM1:75;
    then A13: b1 = b & b2 = EmptyBag n by A11,GROUP_7:2;
    A14: s/.len s = s.len s by A10,FINSEQ_4:def 4;
    A15: s.len s = (t^<*s1*>).(len t +1) by A8,FINSEQ_2:19
            .= s1 by FINSEQ_1:59;
    A16: Sum <*s1*> = s1 by RLVECT_1:61
       .= p.b * a by A12,A13,A14,A15,Th18;
      now per cases;
    suppose t = <*>(cL);
      hence (Sum t) = 0.L by RLVECT_1:60;
    suppose A17: t <> <*>(cL);
        now let k be Nat;
      assume A18: k in dom t;
      then A19: t/.k = t.k by FINSEQ_4:def 4
                      .= s.k by A8,A18,FINSEQ_1:def 7;
      A20: 1 <= k by A18,FINSEQ_3:27;
      A21: dom s = dom decomp b by A5,FINSEQ_3:31;
      A22: len s = len t + len <*s1*> by A8,FINSEQ_1:35
                .= len t +1 by FINSEQ_1:56;
        k <= len t by A18,FINSEQ_3:27;
      then A23: k < len s by A22,NAT_1:38;
      then A24: k in dom decomp b by A5,A20,FINSEQ_3:27;
      then A25: s/.k = s.k by A21,FINSEQ_4:def 4;
      per cases by A20,AXIOMS:21;
      suppose A26: 1 < k;
        consider b1, b2 being bag of n such that
        A27: (decomp b)/.k = <*b1, b2*> and
        A28: s/.k = p.b1*O.b2 by A6,A21,A24;
          b2 <> EmptyBag n by A5,A23,A26,A27,POLYNOM1:76;
        hence t/.k = p.b1*0.L by A19,A25,A28,Th18
                    .= 0.L by VECTSP_1:36;
      suppose A29: k = 1;
        consider b1, b2 being bag of n such that
        A30: (decomp b)/.k = <*b1, b2*> and
        A31: s/.k = p.b1*O.b2 by A6,A21,A24;
          (decomp b)/.1 = <*EmptyBag n, b*> by POLYNOM1:75;
        then A32: b1 = EmptyBag n & b2 = b by A29,A30,GROUP_7:2;
          now assume b = EmptyBag n;
             then decomp b = <* <*EmptyBag n, EmptyBag n*> *>
               by POLYNOM1:77;
             then len t +1 = 0+1 by A5,A22,FINSEQ_1:56;
             then len t = 0 by XCMPLX_1:2;
             hence contradiction by A17,FINSEQ_1:25;
             end;
        then s.k = (p.EmptyBag n)*0.L by A25,A31,A32,Th18
           .= 0.L by VECTSP_1:36;
        hence t/.k = 0.L by A19;
      end;
      hence Sum t = 0.L by MATRLIN:15;
      end;
    hence (p*'O).b = p.b * a by A4,A9,A16,RLVECT_1:10;
    end;
  then (p*'O).b = p.b * a by A3 .= (p * a).b by Def11;
  hence (p*'O).x = (p * a).x;
  end;
hence thesis by A1,A2,FUNCT_1:9;
end;

Lm4:
for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval((a _(n,L))*'p,x) = a * eval(p,x)
proof
let n be Ordinal,
    L be left_zeroed right_zeroed add-associative
         right_complementable unital associative commutative Abelian
         distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x being Function of n,L;
thus eval((a _(n,L))*'p,x) = eval(a _(n,L),x) * eval(p,x) by POLYNOM2:27
                          .= a * eval(p,x) by Th25;
end;

Lm5:
for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(p*'(a _(n,L)),x) = eval(p,x) * a
proof
let n be Ordinal,
    L be left_zeroed right_zeroed add-associative
         right_complementable unital associative commutative Abelian
         distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x being Function of n,L;
thus eval(p*'(a _(n,L)),x) = eval(p,x) * eval(a _(n,L),x) by POLYNOM2:27
                          .= eval(p,x) * a by Th25;
end;

theorem
  for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(a*p,x) = a * eval(p,x)
proof
let n be Ordinal,
    L be Abelian left_zeroed right_zeroed add-associative
         right_complementable unital associative commutative
         distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x be Function of n,L;
thus eval(a*p,x) = eval((a _(n,L)) *' p,x) by Th27
                .= a * eval(p,x) by Lm4;
end;

theorem
  for n being Ordinal,
    L being left_zeroed right_zeroed add-left-cancelable add-associative
            right_complementable unital associative domRing-like
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(a*p,x) = a * eval(p,x)
proof
let n be Ordinal,
    L be left_zeroed right_zeroed add-left-cancelable add-associative
         right_complementable unital associative domRing-like
         distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support(a*p)) &
   eval(a*p,x) = Sum y &
   for i being Nat st 1 <= i & i <= len y holds
        y/.i = ((a*p) * SgmX(BagOrder n, Support(a*p)))/.i *
             eval(((SgmX(BagOrder n, Support(a*p)))/.i)@,x) by POLYNOM2:def 4;
consider z being FinSequence of the carrier of L such that
A2: len z = len SgmX(BagOrder n, Support p) &
   eval(p,x) = Sum z &
   for i being Nat st 1 <= i & i <= len z holds
        z/.i = (p * SgmX(BagOrder n, Support p))/.i *
               eval(((SgmX(BagOrder n, Support p))/.i)@,x) by POLYNOM2:def 4;
A3: BagOrder n linearly_orders Support(a*p) by POLYNOM2:20;
per cases;
suppose A4: a = 0.L;
A5: now let b be bag of n;
    thus (a*p).b = a * p.b by Def10 .= 0.L by A4,BINOM:1;
    end;
  now assume Support(a*p) <> {};
    then reconsider sp = Support(a*p) as non empty Subset of Bags n;
    consider c being Element of sp;
      c in sp;
    then (a*p).c <> 0.L by POLYNOM1:def 9;
    hence contradiction by A5;
    end;
then rng(SgmX(BagOrder n, Support(a*p))) = {} by A3,TRIANG_1:def 2;
then SgmX(BagOrder n, Support(a*p)) = {} by FINSEQ_1:27;
then len y = 0 by A1,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
then Sum y = 0.L by RLVECT_1:60 .= a * Sum z by A4,BINOM:1;
hence thesis by A1,A2;
suppose A6: a <> 0.L;
A7: for u being set holds u in Support p implies u in Support(a*p)
   proof
   let u be set;
   assume A8: u in Support p;
   then A9: p.u <> 0.L by POLYNOM1:def 9;
   reconsider u' = u as Element of Bags n by A8;
     a * p.u' <> 0.L by A6,A9,VECTSP_2:def 5;
   then (a * p).u' <> 0.L by Def10;
   hence thesis by POLYNOM1:def 9;
   end;
A10: for u being set holds u in Support(a*p) implies u in Support p
   proof
   let u be set;
   assume A11: u in Support(a*p);
   then reconsider u' = u as Element of Bags n;
     (a*p).u <> 0.L by A11,POLYNOM1:def 9;
   then a * p.u' <> 0.L by Def10;
   then p.u' <> 0.L by BINOM:2;
   hence thesis by POLYNOM1:def 9;
   end;
then A12: Support(a*p) = Support(p) by A7,TARSKI:2;
A13: len z = len y by A1,A2,A7,A10,TARSKI:2;
then A14: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3;
  now let i be set;
  assume A15: i in dom z;
  then i in Seg(len z) by FINSEQ_1:def 3;
  then i in { k where k is Nat : 1 <= k & k <= len z } by FINSEQ_1:def 1;
  then consider k being Nat such that
  A16: i = k & 1 <= k & k <= len z;
  A17: a * z/.k = a * ((p * SgmX(BagOrder n, Support p))/.k *
                  eval(((SgmX(BagOrder n, Support p))/.k)@,x)) by A2,A16
    .= (a * (p * SgmX(BagOrder n, Support(a*p)))/.k) *
        eval(((SgmX(BagOrder n, Support(a*p)))/.k)@,x) by A12,VECTSP_1:def 16;
  A18: dom z = Seg(len SgmX(BagOrder n, Support(a*p))) by A1,A14,FINSEQ_1:def 3
           .= dom(SgmX(BagOrder n, Support(a*p))) by FINSEQ_1:def 3;
  A19: dom p = Bags n by FUNCT_2:def 1;
    now let u be set;
    assume u in rng(SgmX(BagOrder n, Support(a*p)));
    then u in Support(a*p) by A3,TRIANG_1:def 2;
    hence u in dom p by A19;
    end;
  then rng SgmX(BagOrder n, Support(a*p)) c= dom p by TARSKI:def 3;
  then reconsider q = p * SgmX(BagOrder n, Support(a*p))
       as FinSequence by FINSEQ_1:20;
    for u being set holds u in rng q implies u in the carrier of L
    proof
    let u be set;
    assume u in rng q;
    then A20: u in rng p by FUNCT_1:25;
      rng p c= the carrier of L by RELSET_1:12;
    hence thesis by A20;
    end;
  then rng q c= the carrier of L by TARSKI:def 3;
  then reconsider q as FinSequence of the carrier of L by FINSEQ_1:def 4;
    (SgmX(BagOrder n, Support(a*p))).k
   = (SgmX(BagOrder n, Support(a*p)))/.k by A15,A16,A18,FINSEQ_4:def 4;
  then k in dom q by A15,A16,A18,A19,FUNCT_1:21;
  then A21: (p * SgmX(BagOrder n, Support(a*p)))/.k
          = q.k by FINSEQ_4:def 4
         .= p.(SgmX(BagOrder n, Support(a*p)).k) by A15,A16,A18,FUNCT_1:23
         .= p.(SgmX(BagOrder n, Support(a*p))/.k) by A15,A16,A18,FINSEQ_4:def 4
;
  reconsider c = SgmX(BagOrder n, Support(a*p))/.k as Element of Bags n;
  reconsider c as bag of n;
  A22: (a*p).(SgmX(BagOrder n, Support(a*p))/.k)
     = (a*p).c
    .= a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A21,Def10;
  A23: dom(a*p) = Bags n by FUNCT_2:def 1;
    now let u be set;
    assume u in rng(SgmX(BagOrder n, Support(a*p)));
    then u in Support(a*p) by A3,TRIANG_1:def 2;
    hence u in dom(a*p) by A23;
    end;
  then rng SgmX(BagOrder n, Support(a*p)) c= dom(a*p) by TARSKI:def 3;
  then reconsider r = (a*p) * SgmX(BagOrder n, Support(a*p))
       as FinSequence by FINSEQ_1:20;
    for u being set holds u in rng r implies u in the carrier of L
    proof
    let u be set;
    assume u in rng r;
    then A24: u in rng(a*p) by FUNCT_1:25;
      rng(a*p) c= the carrier of L by RELSET_1:12;
    hence thesis by A24;
    end;
  then rng r c= the carrier of L by TARSKI:def 3;
  then reconsider r as FinSequence of the carrier of L by FINSEQ_1:def 4;
    (SgmX(BagOrder n, Support(a*p))).k
   = (SgmX(BagOrder n, Support(a*p)))/.k by A15,A16,A18,FINSEQ_4:def 4;
  then k in dom r by A15,A16,A18,A23,FUNCT_1:21;
  then ((a*p) * SgmX(BagOrder n, Support(a*p)))/.k
     = r.k by FINSEQ_4:def 4
    .= (a*p).(SgmX(BagOrder n, Support(a*p)).k) by A15,A16,A18,FUNCT_1:23
    .= a * (p * SgmX(BagOrder n, Support(a*p)))/.k
       by A15,A16,A18,A22,FINSEQ_4:def 4;
  hence y/.i = a * z/.i by A1,A13,A16,A17;
  end;
then y = a * z by A14,POLYNOM1:def 2;
hence thesis by A1,A2,BINOM:4;
end;

theorem
  for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(p*a,x) = eval(p,x) * a
proof
let n be Ordinal,
    L be Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x be Function of n,L;
thus eval(p*a,x) = eval(p*'(a _(n,L)),x) by Th28
                .= eval(p,x) * a by Lm5;
end;

theorem
  for n being Ordinal,
    L being left_zeroed right_zeroed add-left-cancelable add-associative
            right_complementable unital associative commutative
            distributive domRing-like (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(p*a,x) = eval(p,x) * a
proof
let n be Ordinal,
    L be left_zeroed right_zeroed add-left-cancelable add-associative
         right_complementable unital associative commutative
         distributive domRing-like (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x be Function of n,L;
consider y being FinSequence of the carrier of L such that
A1: len y = len SgmX(BagOrder n, Support(p*a)) &
   eval(p*a,x) = Sum y &
   for i being Nat st 1 <= i & i <= len y holds
        y/.i = ((p*a) * SgmX(BagOrder n, Support(p*a)))/.i *
             eval(((SgmX(BagOrder n, Support(p*a)))/.i)@,x) by POLYNOM2:def 4;
consider z being FinSequence of the carrier of L such that
A2: len z = len SgmX(BagOrder n, Support p) &
   eval(p,x) = Sum z &
   for i being Nat st 1 <= i & i <= len z holds
        z/.i = (p * SgmX(BagOrder n, Support p))/.i *
               eval(((SgmX(BagOrder n, Support p))/.i)@,x) by POLYNOM2:def 4;
  now per cases;
case A3: a = 0.L;
A4: now let b be bag of n;
    thus (p*a).b = p.b * a by Def11 .= 0.L by A3,BINOM:2;
    end;
A5: now assume Support(p*a) <> {};
    then reconsider sp = Support(p*a) as non empty Subset of Bags n;
    consider c being Element of sp;
      c in sp;
    then (p*a).c <> 0.L by POLYNOM1:def 9;
    hence contradiction by A4;
    end;
  BagOrder n linearly_orders Support(p*a) by POLYNOM2:20;
then rng(SgmX(BagOrder n, Support(p*a))) = {} by A5,TRIANG_1:def 2;
then SgmX(BagOrder n, Support(p*a)) = {} by FINSEQ_1:27;
then len y = 0 by A1,FINSEQ_1:25;
then y = <*>(the carrier of L) by FINSEQ_1:32;
then Sum y = 0.L by RLVECT_1:60 .= Sum z * a by A3,BINOM:2;
hence thesis by A1,A2;
case A6: a <> 0.L;
A7: BagOrder n linearly_orders Support(p*a) by POLYNOM2:20;
A8: for u being set holds u in Support p implies u in Support(p*a)
   proof
   let u be set;
   assume A9: u in Support p;
   then A10: p.u <> 0.L by POLYNOM1:def 9;
   reconsider u' = u as Element of Bags n by A9;
     p.u' * a <> 0.L by A6,A10,VECTSP_2:def 5;
   then (p *a).u' <> 0.L by Def11;
   hence thesis by POLYNOM1:def 9;
   end;
A11: for u being set holds u in Support(p*a) implies u in Support p
   proof
   let u be set;
   assume A12: u in Support(p*a);
   then reconsider u' = u as Element of Bags n;
     (p*a).u <> 0.L by A12,POLYNOM1:def 9;
   then p.u' * a <> 0.L by Def11;
   then p.u' <> 0.L by BINOM:1;
   hence thesis by POLYNOM1:def 9;
   end;
then A13: Support(p*a) = Support(p) by A8,TARSKI:2;
A14: len z = len y by A1,A2,A8,A11,TARSKI:2;
then A15: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3;
  now let i be set;
  assume A16: i in dom z;
  then i in Seg(len z) by FINSEQ_1:def 3;
  then i in { k where k is Nat : 1 <= k & k <= len z } by FINSEQ_1:def 1;
  then consider k being Nat such that
  A17: i = k & 1 <= k & k <= len z;
  A18: z/.k * a = (p * SgmX(BagOrder n, Support(p*a)))/.k *
           (eval(((SgmX(BagOrder n, Support(p*a)))/.k)@,x)) * a by A2,A13,A17
    .= ((p * SgmX(BagOrder n, Support(p*a)))/.k * a) *
       eval(((SgmX(BagOrder n, Support(p*a)))/.k)@,x) by VECTSP_1:def 16;
  A19: dom z = Seg(len SgmX(BagOrder n, Support(p*a))) by A1,A15,FINSEQ_1:def 3
           .= dom(SgmX(BagOrder n, Support(p*a))) by FINSEQ_1:def 3;
  A20: dom p = Bags n by FUNCT_2:def 1;
    now let u be set;
    assume u in rng(SgmX(BagOrder n, Support(p*a)));
    then u in Support(p*a) by A7,TRIANG_1:def 2;
    hence u in dom p by A20;
    end;
  then rng SgmX(BagOrder n, Support(p*a)) c= dom p by TARSKI:def 3;
  then reconsider q = p * SgmX(BagOrder n, Support(p*a))
       as FinSequence by FINSEQ_1:20;
    for u being set holds u in rng q implies u in the carrier of L
    proof
    let u be set;
    assume u in rng q;
    then A21: u in rng p by FUNCT_1:25;
      rng p c= the carrier of L by RELSET_1:12;
    hence thesis by A21;
    end;
  then rng q c= the carrier of L by TARSKI:def 3;
  then reconsider q as FinSequence of the carrier of L by FINSEQ_1:def 4;
    (SgmX(BagOrder n, Support(p*a))).k
   = (SgmX(BagOrder n, Support(p*a)))/.k by A16,A17,A19,FINSEQ_4:def 4;
  then k in dom q by A16,A17,A19,A20,FUNCT_1:21;
  then A22: (p * SgmX(BagOrder n, Support(p*a)))/.k
          = q.k by FINSEQ_4:def 4
         .= p.(SgmX(BagOrder n, Support(p*a)).k) by A16,A17,A19,FUNCT_1:23
         .= p.(SgmX(BagOrder n, Support(p*a))/.k) by A16,A17,A19,FINSEQ_4:def 4
;
  reconsider c = SgmX(BagOrder n, Support(p*a))/.k as Element of Bags n;
  reconsider c as bag of n;
  A23: (p*a).(SgmX(BagOrder n, Support(p*a))/.k)
     = (p*a).c
    .= (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A22,Def11;
  A24: dom(p*a) = Bags n by FUNCT_2:def 1;
    now let u be set;
    assume u in rng(SgmX(BagOrder n, Support(p*a)));
    then u in Support(p*a) by A7,TRIANG_1:def 2;
    hence u in dom(p*a) by A24;
    end;
  then rng SgmX(BagOrder n, Support(p*a)) c= dom(p*a) by TARSKI:def 3;
  then reconsider r = (p*a) * SgmX(BagOrder n, Support(p*a))
       as FinSequence by FINSEQ_1:20;
    for u being set holds u in rng r implies u in the carrier of L
    proof
    let u be set;
    assume u in rng r;
    then A25: u in rng(p*a) by FUNCT_1:25;
      rng(p*a) c= the carrier of L by RELSET_1:12;
    hence thesis by A25;
    end;
  then rng r c= the carrier of L by TARSKI:def 3;
  then reconsider r as FinSequence of the carrier of L by FINSEQ_1:def 4;
    (SgmX(BagOrder n, Support(p*a))).k
   = (SgmX(BagOrder n, Support(p*a)))/.k by A16,A17,A19,FINSEQ_4:def 4;
  then k in dom r by A16,A17,A19,A24,FUNCT_1:21;
  then ((p*a) * SgmX(BagOrder n, Support(p*a)))/.k
     = r.k by FINSEQ_4:def 4
    .= (p*a).(SgmX(BagOrder n, Support(p*a)).k) by A16,A17,A19,FUNCT_1:23
    .= (p * SgmX(BagOrder n, Support(p*a)))/.k * a
       by A16,A17,A19,A23,FINSEQ_4:def 4;
  hence y/.i = z/.i * a by A1,A14,A17,A18;
  end;
then y = z * a by A15,POLYNOM1:def 3;
hence thesis by A1,A2,BINOM:5;
end;
hence thesis;
end;

theorem
  for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval((a _(n,L))*'p,x) = a * eval(p,x) by Lm4;

theorem
  for n being Ordinal,
    L being Abelian left_zeroed right_zeroed add-associative
            right_complementable unital associative commutative
            distributive (non trivial doubleLoopStr),
    p being Polynomial of n,L,
    a being Element of L,
    x being Function of n,L
holds eval(p*'(a _(n,L)),x) = eval(p,x) * a
proof
let n be Ordinal,
    L be left_zeroed right_zeroed add-associative
         right_complementable unital associative commutative Abelian
         distributive (non trivial doubleLoopStr),
    p be Polynomial of n,L,
    a be Element of L,
    x being Function of n,L;
thus eval(p*'(a _(n,L)),x) = eval(p,x) * eval(a _(n,L),x) by POLYNOM2:27
                         .= eval(p,x) * a by Th25;
end;



Back to top