### 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