:: More About Polynomials: Monomials and Constant Polynomials :: by Christoph Schwarzweller :: :: Received November 28, 2001 :: Copyright (c) 2001-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RLVECT_1, ALGSTR_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES, VECTSP_2, ZFMISC_1, XBOOLE_0, STRUCT_0, POLYNOM1, VALUED_0, SUBSET_1, SUPINF_2, FUNCT_4, PRE_POLY, FUNCT_1, FUNCOP_1, RELAT_1, ORDINAL1, CARD_1, PARTFUN1, POLYNOM2, FINSEQ_1, CARD_3, NUMBERS, XXREAL_0, FINSET_1, ORDERS_1, ARYTM_3, NAT_1, MESFUNC1, QUOFIELD, GROUP_1, TARSKI, MSSUBFAM, ALGSEQ_1, CAT_3, XCMPLX_0, ORDINAL4, POLYNOM7, FUNCT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_7, POLYNOM1, NUMBERS, XXREAL_0, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_4, NAT_1, ALGSTR_1, RLVECT_1, ORDERS_1, FINSEQ_1, FUNCOP_1, GROUP_1, QUOFIELD, GRCAT_1, VECTSP_2, POLYNOM2, VECTSP_1, GROUP_6, PRE_POLY; constructors REALSET2, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM2, ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, FUNCT_4, RINGCAT1, MOD_4; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1, POLYNOM2, ALGSTR_0, CARD_1, SUBSET_1, PRE_POLY, FUNCT_1, RINGCAT1, MOD_4; requirements NUMERALS, BOOLE, SUBSET, ARITHM; equalities FUNCOP_1, STRUCT_0, ORDINAL1; expansions FUNCT_2, STRUCT_0, RINGCAT1, MOD_4; theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1, VECTSP_1, POLYNOM1, QUOFIELD, FUNCT_7, FUNCT_4, FUNCOP_1, BINOM, FINSEQ_3, RLVECT_1, VECTSP_2, GROUP_1, NAT_1, FINSEQ_2, FINSEQ_5, MATRLIN, POLYNOM2, XBOOLE_0, XREAL_1, GROUP_6, XXREAL_0, ORDINAL1, PARTFUN1, PRE_POLY, XTUPLE_0, PBOOLE; schemes FUNCT_2; begin registration cluster Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive domRing-like for non trivial doubleLoopStr; existence proof set R = the domRing; take R; thus thesis; end; end; definition let X be set, R be non empty ZeroStr, p be Series of X,R; attr p is non-zero means p <> 0_(X,R); end; registration let X be set, R be non trivial ZeroStr; cluster non-zero for Series of X,R; existence proof set a = the Element of NonZero R; A1: not a in {0.R} by XBOOLE_0:def 5; 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 8; then dom 0_(X,R) = Bags X; then A2: p.(EmptyBag X) = a by FUNCT_7:31; a <> 0.R by A1,TARSKI:def 1; then p <> 0_(X,R) by A2,POLYNOM1:22; hence thesis; end; end; registration let n be Ordinal, R be non trivial ZeroStr; cluster non-zero for Polynomial of n,R; existence proof set a = the Element of NonZero R; A1: not a in {0.R} by XBOOLE_0:def 5; 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; A2: now let u be object; assume A3: u in Support p; then u is Element of Bags n; then A4: u is bag of n; now assume u <> EmptyBag n; then p.u = (0_(n,R)).u by FUNCT_7:32 .= 0.R by A4,POLYNOM1:22; hence contradiction by A3,POLYNOM1:def 4; end; hence u in {EmptyBag n} by TARSKI:def 1; end; 0_(n,R) = (Bags n --> 0.R) by POLYNOM1:def 8; then dom 0_(n,R) = Bags n; then A5: p.(EmptyBag n) = a by FUNCT_7:31; now let u be object; assume u in {EmptyBag n}; then A6: u = EmptyBag n by TARSKI:def 1; a <> 0.R by A1,TARSKI:def 1; hence u in Support p by A5,A6,POLYNOM1:def 4; end; then Support p = {EmptyBag n} by A2,TARSKI:2; then reconsider p as Polynomial of n,R by POLYNOM1:def 5; take p; a <> 0.R by A1,TARSKI:def 1; then p <> 0_(n,R) by A5,POLYNOM1:22; hence thesis; 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: Support s = {}; now let x be object; assume x in Bags X; then reconsider x9 = x as Element of Bags X; s.x9 = 0.R by A2,POLYNOM1:def 4; hence s.x = (0_(X,R)).x by POLYNOM1:22; end; hence s = 0_(X,R); end; now assume A3: s = 0_(X,R); now set x = the Element of Support s; assume Support s <> {}; then A4: x in Support s; then reconsider x as bag of X; s.x <> 0.R by A4,POLYNOM1:def 4; hence contradiction by A3,POLYNOM1:22; end; hence Support s = {}; 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 set x = EmptyBag X; assume R is non trivial; then consider a being Element of R such that A2: a <> 0.R; take s = (Bags X) --> a; s.x = a; then EmptyBag X in Support s by A2,POLYNOM1:def 4; hence ex s being Series of X,R st Support(s) <> {}; end; now assume ex s being Series of X,R st Support(s) <> {}; then consider s being Series of X,R such that A3: Support(s) <> {}; set b = the Element of Support s; b in Support s by A3; then reconsider b as Element of Bags X; now given x being object such that A4: the carrier of R = {x}; 0.R = x by A4,TARSKI:def 1 .= s.b by A4,TARSKI:def 1; hence contradiction by A3,POLYNOM1:def 4; end; hence R is non trivial by ZFMISC_1:131; end; hence thesis by A1; end; definition let X be set, b be bag of X; attr b is univariate means ex u being Element of X st support b = {u}; end; registration let X be non empty set; cluster univariate for bag of X; existence proof set x = the Element of X; set b = EmptyBag X +* (x,1); take b; A1: dom (EmptyBag X) = X by PARTFUN1:def 2; then A2: b.x = ((EmptyBag X)+*(x.-->1)).x by FUNCT_7:def 3; A4: for u being object holds u in support b implies u in {x} proof let u be object; assume A5: u in support b; now assume u <> x; then A6: not u in dom (x.-->1) by TARSKI:def 1; b.u = ((EmptyBag X)+*(x.-->1)).u by A1,FUNCT_7:def 3; then b.u = (EmptyBag X).u by A6,FUNCT_4:11 .= 0 by PBOOLE:5; hence contradiction by A5,PRE_POLY:def 7; end; hence thesis by TARSKI:def 1; end; x in dom (x.-->1) by TARSKI:def 1; then A7: b.x = (x.-->1).x by A2,FUNCT_4:13 .= 1 by FUNCOP_1:72; for u being object holds u in {x} implies u in support b proof let u be object; assume u in {x}; then u = x by TARSKI:def 1; hence thesis by A7,PRE_POLY:def 7; end; then support b = {x} by A4,TARSKI:2; hence thesis; end; end; registration let X be non empty set; cluster univariate -> non empty-yielding for 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}; x in support b by A1,TARSKI:def 1; then b.x <> 0 by PRE_POLY:def 7; then b.x <> (EmptyBag X).x by PBOOLE:5; hence thesis by PRE_POLY:def 18; end; end; begin :: Polynomials without Variables theorem for b being bag of {} holds b = EmptyBag {} proof set n = {}; let b be bag of {}; A1: for b being bag of n holds b = {} proof let b be bag of n; b in Bags n by PRE_POLY:def 12; hence thesis by PRE_POLY:51,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 set n = {}; let L be non empty doubleLoopStr, p be Polynomial of {},L; A1: for b being bag of {} holds b = {} proof let b be bag of {}; b in Bags {} by PRE_POLY:def 12; hence thesis by PRE_POLY:51,TARSKI:def 1; end; reconsider p as Function of Bags {},L; reconsider p as Function of {{}},the carrier of L by PRE_POLY:51; set a = p/.{}; A2: dom p = {{}} by FUNCT_2:def 1 .= {EmptyBag n} by A1; A3: for u being object holds u in p implies u in [:{EmptyBag n},{a}:] proof let u be object; assume A4: u in p; then consider p1,p2 being object such that A5: u = [p1,p2] by RELAT_1:def 1; A6: p1 in dom p by A4,A5,XTUPLE_0:def 12; then reconsider p1 as bag of n by A2; A7: p2 is set by TARSKI:1; A8: p1 = {} by A1; then p2 = p.{} by A4,A5,A6,FUNCT_1:def 2,A7 .= p/.{} by A6,A8,PARTFUN1:def 6; then p2 in {a} by TARSKI:def 1; hence thesis by A2,A5,A6,ZFMISC_1:def 2; end; take a; A9: EmptyBag n = {} by A1; for u being object holds u in [:{EmptyBag n},{a}:] implies u in p proof let u be object; assume u in [:{EmptyBag n},{a}:]; then consider u1,u2 being object such that A10: u1 in {EmptyBag n} and A11: u2 in {a} and A12: u = [u1,u2] by ZFMISC_1:def 2; A13: u1 = {} by A9,A10,TARSKI:def 1; u2 = a by A11,TARSKI:def 1 .= p.{} by A2,A10,A13,PARTFUN1:def 6; hence thesis by A2,A10,A12,A13,FUNCT_1:1; end; hence thesis by A3,TARSKI: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 set n = {}; 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; A1: for b being bag of n holds b = {} proof let b be bag of n; b in Bags n by PRE_POLY:def 12; hence thesis by PRE_POLY:51,TARSKI:def 1; end; then A2: EmptyBag n = {}; consider a being Element of L such that A3: p = {EmptyBag n} --> a by Lm1; A4: p.(EmptyBag n) = a by A3; A5: dom p = {EmptyBag n} by A3; now per cases; case A6: a = 0.L; Support p = {} proof set u = the Element of Support p; assume A7: Support p <> {}; then u in Support p; then reconsider u as Element of Bags n; p.u <> 0.L by A7,POLYNOM1:def 4; hence thesis by A1,A2,A4,A6; end; then reconsider Sp = Support p as empty Subset of Bags n; consider y being FinSequence of the carrier of L such that A8: len y = len SgmX(BagOrder n, Support p) and A9: eval(p,x) = Sum y and for i being Element of 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; SgmX(BagOrder n, Sp) = {} by POLYNOM2:18,PRE_POLY:76; then y = <*>(the carrier of L) by A8; hence eval(p,x) = a by A6,A9,RLVECT_1:43; end; case A10: a <> 0.L; reconsider sp = Support p as finite Subset of Bags n; set sg = SgmX(BagOrder n, sp); A11: BagOrder n linearly_orders sp by POLYNOM2:18; A12: for u being object holds u in Support p implies u in {{}} proof let u be object; 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 object holds u in {{}} implies u in Support p proof let u be object; assume u in {{}}; then u = EmptyBag n by A2,TARSKI:def 1; hence thesis by A4,A10,POLYNOM1:def 4; end; then Support p = {{}} by A12,TARSKI:2; then A13: rng sg = {{}} by A11,PRE_POLY:def 2; then A14: {} in rng sg by TARSKI:def 1; then A15: 1 in dom sg by FINSEQ_3:31; then sg.1 in dom p by A2,A5,A13,FUNCT_1:3; then 1 in dom (p * sg) by A15,FUNCT_1:11; then A16: (p * sg)/.1 = (p * sg).1 by PARTFUN1:def 6 .= p.(sg.1) by A15,FUNCT_1:13 .= a by A2,A3,A13,A15,FUNCOP_1:7,FUNCT_1:3; A17: for u being object holds u in dom sg implies u in {1} proof let u be object; assume A18: u in dom sg; assume A19: not u in {1}; reconsider u as Element of NAT by A18; sg/.u = sg.u by A18,PARTFUN1:def 6; then A20: sg/.u in rng sg by A18,FUNCT_1:3; A21: u <> 1 by A19,TARSKI:def 1; A22: 1 < u proof consider k being Nat such that A23: 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 ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23; hence thesis by A21,XXREAL_0:1; end; sg/.1 = sg.1 by A14,A18,FINSEQ_3:31,PARTFUN1:def 6; then sg/.1 in rng sg by A15,FUNCT_1:3; then sg/.1 = {} by A13,TARSKI:def 1 .= sg/.u by A13,A20,TARSKI:def 1; hence thesis by A11,A15,A18,A22,PRE_POLY:def 2; end; for u being object holds u in {1} implies u in dom sg by A15,TARSKI:def 1; then dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2; then A24: len sg = 1 by FINSEQ_1:def 3; consider y being FinSequence of the carrier of L such that A25: len y = len sg and A26: Sum y = eval(p,x) and A27: for i being Element of NAT st 1 <= i & i <= len y holds y/.i = (p * sg)/.i * eval((sg/.i),x) by POLYNOM2:def 4; dom y = Seg(len y) by FINSEQ_1:def 3 .= dom sg by A25,FINSEQ_1:def 3; then y.1 = y/.1 by A14,FINSEQ_3:31,PARTFUN1:def 6 .= (p * sg)/.1 * eval((sg/.1),x) by A24,A25,A27 .= (p * sg)/.1 * eval(EmptyBag n,x) by A1,A2 .= (p * sg)/.1 * 1.L by POLYNOM2:14 .= a by A16; then y = <* a *> by A24,A25,FINSEQ_1:40; hence eval(p,x) = a by A26,RLVECT_1:44; end; end; hence thesis by A3; end; theorem for L being right_zeroed add-associative right_complementable Abelian well-unital distributive associative non trivial non trivial doubleLoopStr holds Polynom-Ring({},L) is_ringisomorph_to L proof set n = {}; let L be right_zeroed add-associative right_complementable Abelian well-unital distributive associative non trivial non trivial doubleLoopStr; set PL = Polynom-Ring(n,L); defpred P[set,set] means ex p being Polynomial of n,L st p = $1 & p.{} = $2; A1: dom 0_(n,L) = Bags n by FUNCT_2:def 1; A2: EmptyBag n in dom(EmptyBag n .--> 1_L) by TARSKI:def 1; A3: for b being bag of {} holds b = {} proof let b be bag of {}; b in Bags {} by PRE_POLY:def 12; hence thesis by PRE_POLY:51,TARSKI:def 1; end; then A4: EmptyBag n = {}; then reconsider i = {} as bag of n; A5: 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 11; take p.{}; dom p = Bags n by FUNCT_2:def 1; then A6: p.{} in rng p by A4,FUNCT_1:3; rng p c= the carrier of L by RELAT_1:def 19; hence thesis by A6; end; consider f being Function of the carrier of PL,the carrier of L such that A7: for x being Element of PL holds P[x,f.x] from FUNCT_2:sch 3(A5); A8: dom f = the carrier of PL by FUNCT_2:def 1; reconsider f as Function of PL,L; consider p being Polynomial of n,L such that A9: p = 1_PL and A10: p.{} = f.(1.PL) by A7; A11: p = 1_(n,L) by A9,POLYNOM1:31 .= 0_(n,L)+*(EmptyBag n,1_L) by POLYNOM1:def 9; 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 A12: p = x & p.{} = f.x by A7; consider q being Polynomial of n,L such that A13: q = y & q.{} = f.y by A7; A14: (p*'q).{} = p.i * q.i proof A15: decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73; then A16: len decomp EmptyBag n = 1 by FINSEQ_1:39; set z = p.i * q.i; consider s being FinSequence of the carrier of L such that A17: (p*'q).(EmptyBag n) = Sum s and A18: len s = len decomp EmptyBag n and A19: for k being Element of 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 10; len s = 1 by A15,A18,FINSEQ_1:39; then Seg 1 = dom s by FINSEQ_1:def 3; then A20: 1 in dom s by FINSEQ_1:2,TARSKI:def 1; then consider b1,b2 being bag of n such that (decomp EmptyBag n)/.1 = <*b1, b2*> and A21: s/.1 = p.b1*q.b2 by A19; s.1 = p.b1 * q.b2 by A20,A21,PARTFUN1:def 6 .= p.i * q.b2 by A3 .= p.i * q.i by A3; then s = <* z *> by A16,A18,FINSEQ_1:40; then Sum s = z by RLVECT_1:44; hence thesis by A3,A17; end; ex pq being Polynomial of n,L st pq = x * y & pq.{} = f.( x*y) by A7; hence thesis by A12,A13,A14,POLYNOM1:def 11; end; then A22: f is multiplicative by GROUP_6:def 6; 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 A23: p = x and A24: p.{} = f.x by A7; consider q being Polynomial of n,L such that A25: q = y and A26: q.{} = f.y by A7; consider a being Element of L such that A27: p = {EmptyBag n} --> a by Lm1; A28: ex pq being Polynomial of n,L st pq = x + y & pq.{} = f.( x+y) by A7; consider b being Element of L such that A29: q = {EmptyBag n} --> b by Lm1; A30: p.{} = a by A4,A27; A31: (p+q).{} = p.i + q.i by POLYNOM1:15 .= a + b by A4,A30,A29; q.{} = b by A4,A29; then f.x + f.y = a + b by A4,A24,A26,A27; hence thesis by A23,A25,A28,A31,POLYNOM1:def 11; end; then A32: f is additive by VECTSP_1:def 20; p.i = p.(EmptyBag n) by A3 .= (0_(n,L)+*(EmptyBag n .--> 1_L)).(EmptyBag n) by A11,A1,FUNCT_7:def 3 .= (EmptyBag n .--> 1_L).(EmptyBag n) by A2,FUNCT_4:13 .= 1_L by FUNCOP_1:72; then f is unity-preserving by A9,A10,GROUP_1:def 13; then A33: f is RingHomomorphism by A32,A22; A34: for u being object holds u in the carrier of L implies u in rng f proof let u be object; assume u in the carrier of L; then reconsider u as Element of L; set p = EmptyBag n .--> u; reconsider p as Function; rng p = {u} & dom p = Bags n by FUNCOP_1:8,PRE_POLY:51,TARSKI:def 1; then reconsider p as Function of Bags n, the carrier of L by FUNCT_2:2; reconsider p as Function of Bags n, L; reconsider p as Series of n, L; now per cases; case A35: u = 0.L; Support p = {} proof set v = the Element of Support p; assume Support p <> {}; then A36: v in Support p; then v is bag of n; then p.v = p.(EmptyBag n) by A3,A4 .= u by FUNCOP_1:72; hence thesis by A35,A36,POLYNOM1:def 4; end; hence Support p is finite; end; case A37: u <> 0.L; A38: for v being object holds v in {EmptyBag n} implies v in Support p proof let v be object; assume A39: v in {EmptyBag n}; then reconsider v as Element of Bags n; p.v = p.(EmptyBag n) by A39,TARSKI:def 1 .= u by FUNCOP_1:72; hence thesis by A37,POLYNOM1:def 4; end; for v being object holds v in Support p implies v in {EmptyBag n} proof let v be object; assume v in Support p; then reconsider v as bag of n; v = EmptyBag n by A3,A4; hence thesis by TARSKI:def 1; end; hence Support p is finite by A38,TARSKI:2; end; end; then reconsider p as Polynomial of n,L by POLYNOM1:def 5; reconsider p9 = p as Element of PL by POLYNOM1:def 11; consider q being Polynomial of n,L such that A40: q = p9 and A41: q.{} = f.p9 by A7; q.{} = p.(EmptyBag n) by A3,A40 .= u by FUNCOP_1:72; hence thesis by A8,A41,FUNCT_1:3; end; rng f c= the carrier of L by RELAT_1:def 19; then for u being object holds u in rng f implies u in the carrier of L; then rng f = the carrier of L by A34,TARSKI:2; then f is onto; then A42: f is RingEpimorphism by A33; for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2 proof let x1,x2 be object; assume that A43: x1 in dom f & x2 in dom f and A44: f.x1 = f.x2; reconsider x1,x2 as Element of PL by A43; consider p being Polynomial of n,L such that A45: p = x1 & p.{} = f.x1 by A7; consider q being Polynomial of n,L such that A46: q = x2 & q.{} = f.x2 by A7; consider a2 being Element of L such that A47: q = {EmptyBag n} --> a2 by Lm1; A48: q.(EmptyBag n) = a2 by A47; A49: p.{} = p.(EmptyBag n) by A3; consider a1 being Element of L such that A50: p = {EmptyBag n} --> a1 by Lm1; thus thesis by A3,A44,A45,A46,A50,A47,A48,A49; end; then f is one-to-one by FUNCT_1:def 4; then f is RingMonomorphism by A33; then f is RingIsomorphism by A42; hence thesis by QUOFIELD:def 23; 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 :Def3: ex b being bag of X st for b9 being bag of X st b9 <> b holds p.b9 = 0.L; end; registration let X be set, L be non empty ZeroStr; cluster monomial-like for Series of X,L; existence proof set p = 0_(X,L); take p; for b9 being bag of X st b9 <> EmptyBag X holds p.b9 = 0.L by POLYNOM1:22; hence thesis; 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; registration let X be set, L be non empty ZeroStr; cluster monomial-like -> finite-Support for 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 b9 being bag of X st b9 <> b holds s.b9 = 0.L; per cases; suppose A2: s.b = 0.L; now assume Support s <> {}; then reconsider sp = Support s as non empty Subset of Bags X; set c = the Element of sp; s.c <> 0.L by POLYNOM1:def 4; hence contradiction by A1,A2; end; hence thesis by POLYNOM1:def 5; end; suppose A3: s.b <> 0.L; A4: now let u be object; assume A5: u in Support s; then reconsider u9 = u as Element of Bags X; s.u9 <> 0.L by A5,POLYNOM1:def 4; then u9 = b by A1; hence u in {b} by TARSKI:def 1; end; now let u be object; assume u in {b}; then A6: u = b by TARSKI:def 1; then reconsider u9 = u as Element of Bags X by PRE_POLY:def 12; u9 in Support s by A3,A6,POLYNOM1:def 4; hence u in Support s; end; then Support s = {b} by A4,TARSKI:2; hence thesis by POLYNOM1:def 5; end; 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 ex b being bag of n st Support p = {b}; then consider b being bag of n such that A2: Support p = {b}; for b9 being bag of n st b9 <> b holds p.b9 = 0.L proof let b9 be bag of n; assume A3: b9 <> b; assume A4: p.b9 <> 0.L; reconsider b9 as Element of Bags n by PRE_POLY:def 12; b9 in Support p by A4,POLYNOM1:def 4; hence thesis by A2,A3,TARSKI:def 1; end; hence p is Monomial of n,L by Def3; end; A5: now assume p is Monomial of n,L; then consider b being bag of n such that A6: for b9 being bag of n st b9 <> b holds p.b9 = 0.L by Def3; now per cases; case A7: p.b <> 0.L; A8: for u being object holds u in {b} implies u in Support p proof let u be object; assume A9: u in {b}; then u = b by TARSKI:def 1; then reconsider u9 = u as Element of Bags n by PRE_POLY:def 12; p.u9 <> 0.L by A7,A9,TARSKI:def 1; hence thesis by POLYNOM1:def 4; end; for u being object holds u in Support p implies u in {b} proof let u be object; assume A10: u in Support p; then reconsider u9 = u as bag of n; p.u <> 0.L by A10,POLYNOM1:def 4; then u9 = b by A6; hence thesis by TARSKI:def 1; end; then Support p = {b} by A8,TARSKI:2; hence ex b being bag of n st Support p = {b}; end; case A11: p.b = 0.L; thus Support p = {} proof assume Support p <> {}; then reconsider sp = Support p as non empty Subset of Bags n; set c = the Element of sp; p.c <> 0.L by POLYNOM1:def 4; hence thesis by A6,A11; end; end; end; hence Support p = {} or ex b being bag of n st Support p = {b}; end; now set b = the bag of n; assume A12: Support p = {}; for b9 being bag of n st b9 <> b holds p.b9 = 0.L proof let b9 be bag of n; assume b9 <> b; reconsider c = b9 as Element of Bags n by PRE_POLY:def 12; assume p.b9 <> 0.L; then c in Support p by POLYNOM1:def 4; hence thesis by A12; end; hence p is Monomial of n,L by Def3; end; hence thesis by A1,A5; 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 0_(X,L)+*(b,a); coherence proof A1: b in dom(b .--> a) by TARSKI:def 1; 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; A2: b in Bags X by PRE_POLY:def 12; A3: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A4: m = 0_(X,L)+*(b .--> a) by A2,FUNCT_7:def 3; A5: m.b = (0_(X,L)+*(b .--> a)).b by A3,A2,FUNCT_7:def 3 .= (b .--> a).b by A1,FUNCT_4:13 .= a by FUNCOP_1:72; now per cases; case A6: a <> 0.L; A7: for u being object holds u in Support m implies u in {b} proof let u be object; assume A8: u in Support m; assume not u in {b}; then A9: not u in dom(b .--> a); reconsider u as bag of X by A8; m.u = (0_(X,L)).u by A4,A9,FUNCT_4:11 .= 0.L by POLYNOM1:22; hence thesis by A8,POLYNOM1:def 4; end; b in Support m by A2,A5,A6,POLYNOM1:def 4; then for u being object holds u in {b} implies u in Support m by TARSKI:def 1; then Support m = {b} by A7,TARSKI:2; hence thesis by Th6; end; case A10: a = 0.L; now assume Support m <> {}; then reconsider sm = Support m as non empty Subset of Bags X; set c = the Element of sm; m.c <> 0.L by POLYNOM1:def 4; then not c in {b} by A5,A10,TARSKI:def 1; then A11: not c in dom(b .--> a); reconsider c as bag of X; m.c = (0_(X,L)).c by A4,A11,FUNCT_4:11 .= 0.L by POLYNOM1:22; hence contradiction by POLYNOM1:def 4; end; hence thesis by Th6; end; 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 :Def5: m.it <> 0.L or Support m = {} & it = EmptyBag X; existence proof consider b being bag of X such that A1: for b9 being bag of X st b9 <> b holds m.b9 = 0.L by Def3; now per cases; case m.b <> 0.L; hence thesis; end; case A2: m.b = 0.L; Support m = {} proof assume Support m <> {}; then reconsider sm = Support m as non empty Subset of Bags X; set c = the Element of sm; m.c <> 0.L by POLYNOM1:def 4; hence thesis by A1,A2; end; hence thesis; end; 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; consider b being bag of X such that A4: for b9 being bag of X st b9 <> b holds m.b9 = 0.L by Def3; assume A5: m.b2 <> 0.L or Support m = {} & b2 = EmptyBag X; now per cases; case A6: m.b1 <> 0.L; reconsider b19 = b1 as Element of Bags X by PRE_POLY:def 12; A7: b19 in Support m by A6,POLYNOM1:def 4; thus b1 = b by A4,A6 .= b2 by A5,A4,A7; end; case A8: m.b1 = 0.L; now per cases by A5; case A9: m.b2 <> 0.L; reconsider b29 = b2 as Element of Bags X by PRE_POLY:def 12; b29 in Support m by A9,POLYNOM1:def 4; hence thesis by A3,A8; end; case Support m = {} & b2 = EmptyBag X; hence thesis by A3,A8; end; end; hence thesis; end; 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 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; A1: term(m) is Element of Bags X by PRE_POLY:def 12; assume A2: Support(m) <> {}; then m.term(m) <> 0.L by Def5; then A3: term(m) in Support(m) by A1,POLYNOM1:def 4; ex b being bag of X st Support(m) = {b} by A2,Th6; hence thesis by A3,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; 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; A1: b in Bags n by PRE_POLY:def 12; A2: dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8 .= Bags n; then A3: m = 0_(n,L)+*(b .--> 0.L) by A1,FUNCT_7:def 3; A4: b in dom(b .--> 0.L) by TARSKI:def 1; A5: m.b = (0_(n,L)+*(b .--> 0.L)).b by A2,A1,FUNCT_7:def 3 .= (b .--> 0.L).b by A4,FUNCT_4:13 .= 0.L by FUNCOP_1:72; A6: now let b9 be bag of n; now per cases; case b9 = b; hence m.b9 = 0.L by A5; end; case b9 <> b; then not b9 in dom(b .--> 0.L) by TARSKI:def 1; hence m.b9 = (0_(n,L)).b9 by A3,FUNCT_4:11 .= 0.L by POLYNOM1:22; end; end; hence m.b9 = 0.L; end; hence coefficient(Monom(0.L,b)) = 0.L; (Monom(0.L,b)).(term(Monom(0.L,b))) = 0.L by A6; hence thesis by Def5; 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; 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; A1: b in Bags n by PRE_POLY:def 12; A2: b in dom(b .--> a) by TARSKI:def 1; dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8 .= Bags n; then A3: m.b = (0_(n,L)+*(b .--> a)).b by A1,FUNCT_7:def 3 .= (b .--> a).b by A2,FUNCT_4:13 .= a by FUNCOP_1:72; per cases; suppose m.b <> 0.L; hence thesis by A3,Def5; end; suppose m.b = 0.L; hence thesis by A3,Th8; end; 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; 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; A1: b in Bags n by PRE_POLY:def 12; A2: b in dom(b .--> a) by TARSKI:def 1; dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8 .= Bags n; then m.b = (0_(n,L)+*(b .--> a)).b by A1,FUNCT_7:def 3 .= (b .--> a).b by A2,FUNCT_4:13 .= a by FUNCOP_1:72; then m.b <> 0.L; hence thesis by Def5; 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; per cases by Th6; suppose A1: Support m = {}; A2: now A3: term(m) is Element of Bags X by PRE_POLY:def 12; assume coefficient(m) <> 0.L; hence contradiction by A1,A3,POLYNOM1:def 4; end; A4: m = 0_(X,L) by A1,Th1; set m9 = Monom(coefficient(m),term(m)); A5: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; A6: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1; A7: term(m) = EmptyBag X by A1,Def5; then A8: m9.EmptyBag X = (0_(X,L)+*(EmptyBag X .--> 0.L)).EmptyBag X by A2,A5, FUNCT_7:def 3 .= (EmptyBag X .--> 0.L).EmptyBag X by A6,FUNCT_4:13 .= 0.L by FUNCOP_1:72; now let x be object; assume x in Bags X; then reconsider x9= x as Element of Bags X; now per cases; case x9 = EmptyBag X; hence m9.x9 = 0.L by A8; end; case x <> EmptyBag X; then A9: not x9 in dom(EmptyBag X .--> 0.L) by TARSKI:def 1; m9.x9 = (0_(X,L)+*(EmptyBag X .--> 0.L)).x9 by A7,A2,A5,FUNCT_7:def 3 .= 0_(X,L).x9 by A9,FUNCT_4:11; hence m9.x9 = 0.L by POLYNOM1:22; end; end; hence m.x = m9.x by A4,POLYNOM1:22; end; hence thesis; end; suppose ex b being bag of X st Support m = {b}; then consider b being bag of X such that A10: Support m = {b}; set a = m.b; A11: b in dom(b .--> a) by TARSKI:def 1; set m9 = Monom(coefficient(m),term(m)); A12: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; A13: b in Support m by A10,TARSKI:def 1; then a <> 0.L by POLYNOM1:def 4; then A14: term(m) = b by Def5; A15: now let u be object; assume A16: u in Support(Monom(coefficient(m),term(m))); then reconsider u9 = u as Element of Bags X; now assume u <> b; then A17: not u9 in dom(b .--> a) by TARSKI:def 1; b in dom 0_(X,L) by A12,PRE_POLY:def 12; then m9.u9 = (0_(X,L)+*(b .--> a)).u9 by A14,FUNCT_7:def 3 .= 0_(X,L).u9 by A17,FUNCT_4:11; hence m9.u9 = 0.L by POLYNOM1:22; end; hence u in {b} by A16,POLYNOM1:def 4,TARSKI:def 1; end; b in Bags X by PRE_POLY:def 12; then A18: m9.b = (0_(X,L)+*(b .--> a)).b by A14,A12,FUNCT_7:def 3 .= (b .--> a).b by A11,FUNCT_4:13 .= a by FUNCOP_1:72; now let u be object; assume u in {b}; then A19: u = b by TARSKI:def 1; m9.b <> 0.L by A13,A18,POLYNOM1:def 4; hence u in Support(Monom(coefficient(m),term(m))) by A13,A19, POLYNOM1:def 4; end; then A20: Support(Monom(coefficient(m),term(m))) = {b} by A15,TARSKI:2; now let x be object; assume x in Bags X; then reconsider x9 = x as Element of Bags X; now per cases; case x = b; hence Monom(coefficient(m),term(m)).x9 = m.x9 by A18; end; case A21: x <> b; then A22: not x in Support(Monom(coefficient(m),term(m))) by A20,TARSKI:def 1; not x in Support m by A10,A21,TARSKI:def 1; hence m.x9 = 0.L by POLYNOM1:def 4 .= Monom(coefficient(m),term(m)).x9 by A22,POLYNOM1:def 4; end; end; hence m.x = Monom(coefficient(m),term(m)).x; end; hence thesis; end; end; theorem Th12: for n being Ordinal, L being right_zeroed add-associative right_complementable well-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 well-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) and A2: eval(m,x) = Sum y and A3: for i being Element of 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 A4: for b9 being bag of n st b9 <> b holds m.b9 = 0.L by Def3; now per cases; case A5: m.b <> 0.L; A6: for u being object holds u in Support m implies u in {b} proof let u be object; assume A7: u in Support m; assume A8: not u in {b}; reconsider u as Element of Bags n by A7; u <> b by A8,TARSKI:def 1; then m.u = 0.L by A4; hence thesis by A7,POLYNOM1:def 4; end; A9: b in Bags n & dom m = Bags n by FUNCT_2:def 1,PRE_POLY:def 12; reconsider sm = Support m as finite Subset of Bags n; set sg = SgmX(BagOrder n, sm); A10: BagOrder n linearly_orders sm by POLYNOM2:18; for u being object holds u in {b} implies u in Support m proof let u be object; assume A11: u in {b}; then u = b by TARSKI:def 1; then reconsider u as Element of Bags n by PRE_POLY:def 12; m.u <> 0.L by A5,A11,TARSKI:def 1; hence thesis by POLYNOM1:def 4; end; then Support m = {b} by A6,TARSKI:2; then A12: rng sg = {b} by A10,PRE_POLY:def 2; then A13: b in rng sg by TARSKI:def 1; then A14: 1 in dom sg by FINSEQ_3:31; then A15: sg.1 in rng sg by FUNCT_1:3; then sg.1 = b by A12,TARSKI:def 1; then 1 in dom (m * sg) by A14,A9,FUNCT_1:11; then A16: (m * sg)/.1 = (m * sg).1 by PARTFUN1:def 6 .= m.(sg.1) by A14,FUNCT_1:13 .= m.b by A12,A15,TARSKI:def 1 .= coefficient(m) by A5,Def5; A17: for u being object holds u in dom sg implies u in {1} proof let u be object; assume A18: u in dom sg; assume A19: not u in {1}; reconsider u as Element of NAT by A18; sg/.u = sg.u by A18,PARTFUN1:def 6; then A20: sg/.u in rng sg by A18,FUNCT_1:3; A21: u <> 1 by A19,TARSKI:def 1; A22: 1 < u proof consider k being Nat such that A23: 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 ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23; hence thesis by A21,XXREAL_0:1; end; sg/.1 = sg.1 by A13,A18,FINSEQ_3:31,PARTFUN1:def 6; then sg/.1 in rng sg by A14,FUNCT_1:3; then sg/.1 = b by A12,TARSKI:def 1 .= sg/.u by A12,A20,TARSKI:def 1; hence thesis by A10,A14,A18,A22,PRE_POLY:def 2; end; for u being object holds u in {1} implies u in dom sg by A14,TARSKI:def 1; then A24: dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2; then A25: 1 in dom sg by FINSEQ_1:2,TARSKI:def 1; sg/.1 = sg.1 by A14,PARTFUN1:def 6; then sg/.1 in rng sg by A25,FUNCT_1:3; then A26: sg/.1 = b by A12,TARSKI:def 1; A27: len sg = 1 by A24,FINSEQ_1:def 3; dom y = Seg(len y) by FINSEQ_1:def 3 .= dom sg by A1,FINSEQ_1:def 3; then y.1 = y/.1 by A25,PARTFUN1:def 6 .= (m * sg)/.1 * eval(b,x) by A26,A1,A3,A27; then y = <* coefficient(m) * eval(b,x) *> by A1,A27,A16,FINSEQ_1:40; hence eval(m,x) = coefficient(m) * eval(b,x) by A2,RLVECT_1:44 .= coefficient(m) * eval(term(m),x) by A5,Def5; end; 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; set c = the Element of sm; m.c <> 0.L by POLYNOM1:def 4; hence thesis by A4,A28; end; then term(m) = EmptyBag n & m.(EmptyBag n) = 0.L by Def5,POLYNOM1:def 4; then A30: coefficient(m) * eval(term(m),x) = 0.L; consider y being FinSequence of the carrier of L such that A31: len y = len SgmX(BagOrder n, Support m) and A32: eval(m,x) = Sum y and for i being Element of 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:18; then rng SgmX(BagOrder n, Support m) = {} by A29,PRE_POLY:def 2; then SgmX(BagOrder n, Support m) = {} by RELAT_1:41; then y = <*>(the carrier of L) by A31; hence thesis by A30,A32,RLVECT_1:43; end; end; hence thesis; end; theorem for n being Ordinal, L being right_zeroed add-associative right_complementable well-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 well-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; 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; end; case A2: a = 0.L; for b9 being bag of n holds m.b9 = 0.L proof let b9 be bag of n; now per cases; case A3: b9 = b; A4: b in Bags n by PRE_POLY:def 12; A5: b in dom(b .--> a) by TARSKI:def 1; dom(0_(n,L)) = dom((Bags n) --> 0.L) by POLYNOM1:def 8 .= Bags n; then m = 0_(n,L)+*(b .--> a) by A4,FUNCT_7:def 3; hence m.b9 = (b .--> a).b by A3,A5,FUNCT_4:13 .= 0.L by A2,FUNCOP_1:72; end; case b9 <> b; hence m.b9 = 0_(n,L).b9 by FUNCT_7:32 .= 0.L by POLYNOM1:22; end; end; hence thesis; end; then A6: m.(term(m)) = 0.L; thus eval(m,x) = coefficient(m) * eval(term(m),x) by Th12 .= 0.L by A6 .= a * eval(b,x) by A2; end; end; hence thesis; end; begin :: Constant Polynomials definition let X be set, L be non empty ZeroStr, p be Series of X,L; attr p is Constant means :Def7: for b being bag of X st b <> EmptyBag X holds p.b = 0.L; end; registration let X be set, L be non empty ZeroStr; cluster Constant for 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:22; hence thesis; end; end; definition let X be set, L be non empty ZeroStr; mode ConstPoly of X,L is Constant Series of X,L; end; registration let X be set, L be non empty ZeroStr; cluster Constant -> monomial-like for Series of X,L; coherence; 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 object holds u in Support p implies u in {EmptyBag n} proof let u be object; assume A4: u in Support p; then reconsider u as Element of Bags n; reconsider u9 = u as bag of n; p.u9 <> 0.L by A4,POLYNOM1:def 4; then u9 = EmptyBag n by A2,Def7; 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 object 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 set v = the Element of Support p; assume Support p <> {}; then v in Support p & v in {EmptyBag n} by A3; hence thesis by A6,TARSKI:def 1; end; A8: for b being bag of n holds p.b = 0.L proof let b be bag of n; A9: b is Element of Bags n by PRE_POLY:def 12; assume p.b <> 0.L; hence thesis by A7,A9,POLYNOM1:def 4; end; A10: for u being object holds u in rng p implies u in {0.L} proof let u be object; assume u in rng p; then consider x being object such that A11: x in dom p and A12: p.x = u by FUNCT_1:def 3; x is bag of n by A11; then u = 0.L by A8,A12; hence thesis by TARSKI:def 1; end; A13: dom p = Bags n by FUNCT_2:def 1; for u being object holds u in {0.L} implies u in rng p proof set b = the bag of n; let u be object; assume u in {0.L}; then u = 0.L by TARSKI:def 1; then A14: p.b = u by A8; b in dom p by A13,PRE_POLY:def 12; hence thesis by A14,FUNCT_1:def 3; end; then rng p = {0.L} by A10,TARSKI:2; then p = (Bags n) --> 0.L by A13,FUNCOP_1:9; hence thesis by POLYNOM1:def 8; end; end; now assume A15: p = 0_(n,L) or Support p = {EmptyBag n}; per cases by A15; suppose p = 0_(n,L); then for b being bag of n st b <> EmptyBag n holds p.b = 0.L by POLYNOM1:22; hence p is ConstPoly of n,L by Def7; end; suppose A16: 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 A17: b <> EmptyBag n; reconsider b as Element of Bags n by PRE_POLY:def 12; not b in Support p by A16,A17,TARSKI:def 1; hence thesis by POLYNOM1:def 4; end; hence p is ConstPoly of n,L by Def7; end; end; hence thesis by A1; end; registration let X be set, L be non empty ZeroStr; cluster 0_(X,L) -> Constant; coherence by POLYNOM1:22; end; registration let X be set, L be well-unital non empty doubleLoopStr; cluster 1_(X,L) -> Constant; coherence by POLYNOM1:25; 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 Def5; end; case A2: c.eb = 0.L; Support c = {} proof set u = the Element of Support c; assume A3: Support c <> {}; then u in Support c; then reconsider u as Element of Bags n; c.u <> 0.L by A3,POLYNOM1:def 4; hence thesis by A2,Def7; end; hence term(c) = EmptyBag n by Def5; end; end; hence term(c) = EmptyBag n; thus thesis by A1; 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 0_(X,L)+*(EmptyBag X,a); coherence; end; registration 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 O9 = O as Function of Bags X,L; reconsider O9 as Series of X,L; now let b be bag of X; dom(Z) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A1: O9 = 0_(X,L)+*(EmptyBag X .--> a) by FUNCT_7:def 3; assume b <> EmptyBag X; then not b in dom(EmptyBag X .--> a) by TARSKI:def 1; hence (O9).b = (0_(X,L)).b by A1,FUNCT_4:11 .= 0.L by POLYNOM1:22; end; hence thesis; 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); now set m = 0_(X,L)+*(EmptyBag X,0.L); let x be object; 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; assume x in Bags X; then reconsider x9 = x as bag of X; A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A2: m = 0_(X,L)+*(EmptyBag X .--> 0.L) by FUNCT_7:def 3; A3: EmptyBag X in dom(EmptyBag X .--> 0.L) by TARSKI:def 1; A4: m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> 0.L)).(EmptyBag X) by A1, FUNCT_7:def 3 .= (EmptyBag X .--> 0.L).(EmptyBag X) by A3,FUNCT_4:13 .= 0.L by FUNCOP_1:72; per cases; suppose x9 = EmptyBag X; hence o1.x = o2.x by A4,POLYNOM1:22; end; suppose x9 <> EmptyBag X; then not x9 in dom(EmptyBag X .--> 0.L) by TARSKI:def 1; hence o1.x = o2.x by A2,FUNCT_4:11; end; end; hence thesis; 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); end; case A2: Support p = {EmptyBag X}; set q = 0_(X,L)+*(EmptyBag X,p.(EmptyBag X)); A3: now let x be object; assume x in Bags X; then reconsider x9 = x as bag of X; A4: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A5: q = 0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X)) by FUNCT_7:def 3; A6: EmptyBag X in dom(EmptyBag X .--> p.(EmptyBag X)) by TARSKI:def 1; A7: q.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> p.(EmptyBag X))).( EmptyBag X) by A4,FUNCT_7:def 3 .= (EmptyBag X .--> p.(EmptyBag X)).(EmptyBag X) by A6,FUNCT_4:13 .= p.(EmptyBag X) by FUNCOP_1:72; now per cases; case x9 = EmptyBag X; hence p.x = q.x by A7; end; case A8: x9 <> EmptyBag X; A9: x9 is Element of Bags X by PRE_POLY:def 12; not x9 in Support p by A2,A8,TARSKI:def 1; then A10: p.x9 = 0.L by A9,POLYNOM1:def 4; not x9 in dom(EmptyBag X .--> p.(EmptyBag X)) by A8,TARSKI:def 1; then q.x9 = (0_(X,L)).x9 by A5,FUNCT_4:11; hence p.x = q.x by A10,POLYNOM1:22; end; end; hence p.x = q.x; end; A11: Bags X = dom q by FUNCT_2:def 1; q = p.(EmptyBag X) |(X,L) & Bags X = dom p by FUNCT_2:def 1; hence ex a being Element of L st p = a |(X,L) by A11,A3,FUNCT_1:2; end; 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 8; then dom Z = Bags n; hence (a |(n,L)).EmptyBag n = a by FUNCT_7:31; let b be bag of n; A2: b in Bags n by PRE_POLY:def 12; assume b <> EmptyBag n; hence (a |(n,L)).b = Z.b by FUNCT_7:32 .= 0.L by A1,A2,FUNCOP_1:7; 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 well-unital non empty multLoopStr_0 holds ( 1.L) |(X,L) = 1_(X,L) proof let X be set, L be well-unital non empty multLoopStr_0; set o1 = (1.L) |(X,L), o2 = 1_(X,L); now set m = 0_(X,L)+*(EmptyBag X,1.L); let x be object; 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; assume x in Bags X; then reconsider x9 = x as bag of X; A1: dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A2: m = 0_(X,L)+*(EmptyBag X .--> 1.L) by FUNCT_7:def 3; A3: EmptyBag X in dom(EmptyBag X .--> 1.L) by TARSKI:def 1; A4: m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> 1.L)).(EmptyBag X) by A1, FUNCT_7:def 3 .= (EmptyBag X .--> 1.L).(EmptyBag X) by A3,FUNCT_4:13 .= 1.L by FUNCOP_1:72; per cases; suppose x9 = EmptyBag X; hence o1.x = o2.x by A4,POLYNOM1:25; end; suppose A5: x9 <> EmptyBag X; then not x9 in dom(EmptyBag X .--> 1.L) by TARSKI:def 1; then m.x9 = (0_(X,L)).x9 by A2,FUNCT_4:11 .= 0.L by POLYNOM1:22 .= o2.x9 by A5,POLYNOM1:25; hence o1.x = o2.x; end; end; hence thesis; 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; 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; A1: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1; A2: EmptyBag X in dom(EmptyBag X .--> b) by TARSKI:def 1; dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then A3: k.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> b)).(EmptyBag X) by FUNCT_7:def 3 .= (EmptyBag X .--> b).(EmptyBag X) by A2,FUNCT_4:13 .= b by FUNCOP_1:72; dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by FUNCT_7:def 3 .= (EmptyBag X .--> a).(EmptyBag X) by A1,FUNCT_4:13 .= a by FUNCOP_1:72; hence thesis by A3; 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: EmptyBag X in dom(EmptyBag X .--> a) by TARSKI:def 1; dom(0_(X,L)) = dom((Bags X) --> 0.L) by POLYNOM1:def 8 .= Bags X; then m.(EmptyBag X) = (0_(X,L)+*(EmptyBag X .--> a)).(EmptyBag X) by FUNCT_7:def 3 .= (EmptyBag X .--> a).(EmptyBag X) by A1,FUNCT_4:13 .= a by FUNCOP_1:72; hence thesis by Lm2; end; theorem Th24: for n being Ordinal, L being right_zeroed add-associative right_complementable well-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 well-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) and A2: eval(c,x) = Sum y and A3: for i being Element of 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 A4: coefficient(c) = 0.L; Support c = {} proof set u = the Element of Support c; assume A5: Support c <> {}; then u in Support c; then reconsider u as Element of Bags n; c.u <> 0.L by A5,POLYNOM1:def 4; then u <> EmptyBag n by A4,Lm2; then c.u = 0.L by Def7; hence thesis by A5,POLYNOM1:def 4; end; then reconsider Sc = Support c as empty Subset of Bags n; SgmX(BagOrder n, Sc) = {} by POLYNOM2:18,PRE_POLY:76; then y = <*>(the carrier of L) by A1; hence thesis by A2,A4,RLVECT_1:43; end; case A6: coefficient(c) <> 0.L; reconsider sc = Support c as finite Subset of Bags n; set sg = SgmX(BagOrder n, sc); A7: BagOrder n linearly_orders sc by POLYNOM2:18; A8: for u being object holds u in Support c implies u in {EmptyBag n} proof let u be object; assume A9: u in Support c; assume A10: not u in {EmptyBag n}; reconsider u as Element of Bags n by A9; u <> EmptyBag n by A10,TARSKI:def 1; then c.u = 0.L by Def7; hence thesis by A9,POLYNOM1:def 4; end; for u being object holds u in {EmptyBag n} implies u in Support c proof let u be object; assume A11: u in {EmptyBag n}; then A12: u = EmptyBag n by TARSKI:def 1; reconsider u as Element of Bags n by A11; c.u <> 0.L by A6,A12,Lm2; hence thesis by POLYNOM1:def 4; end; then Support c = {EmptyBag n} by A8,TARSKI:2; then A13: rng sg = {EmptyBag n} by A7,PRE_POLY:def 2; then A14: EmptyBag n in rng sg by TARSKI:def 1; then A15: 1 in dom sg by FINSEQ_3:31; then A16: sg.1 in rng sg by FUNCT_1:3; A17: for u being object holds u in dom sg implies u in {1} proof let u be object; assume A18: u in dom sg; assume A19: not u in {1}; reconsider u as Element of NAT by A18; sg/.u = sg.u by A18,PARTFUN1:def 6; then A20: sg/.u in rng sg by A18,FUNCT_1:3; A21: u <> 1 by A19,TARSKI:def 1; A22: 1 < u proof consider k being Nat such that A23: 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 ex m9 being Nat st m9 = u & 1 <= m9 & m9 <= k by A18,A23; hence thesis by A21,XXREAL_0:1; end; sg/.1 = sg.1 by A14,A18,FINSEQ_3:31,PARTFUN1:def 6; then sg/.1 in rng sg by A15,FUNCT_1:3; then sg/.1 = EmptyBag n by A13,TARSKI:def 1 .= sg/.u by A13,A20,TARSKI:def 1; hence thesis by A7,A15,A18,A22,PRE_POLY:def 2; end; for u being object holds u in {1} implies u in dom sg by A15,TARSKI:def 1; then A24: dom sg = Seg 1 by A17,FINSEQ_1:2,TARSKI:2; then A25: 1 in dom sg by FINSEQ_1:2,TARSKI:def 1; sg/.1 = sg.1 by A15,PARTFUN1:def 6; then sg/.1 in rng sg by A25,FUNCT_1:3; then A26: sg/.1 = EmptyBag n by A13,TARSKI:def 1; A27: len sg = 1 by A24,FINSEQ_1:def 3; dom c = Bags n by FUNCT_2:def 1; then 1 in dom (c * sg) by A13,A15,A16,FUNCT_1:11; then A28: (c * sg)/.1 = (c * sg).1 by PARTFUN1:def 6 .= c.(sg.1) by A15,FUNCT_1:13 .= c.(EmptyBag n) by A13,A16,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 A25,PARTFUN1:def 6 .= coefficient(c) * eval(EmptyBag n,x) by A1,A3,A27,A26,A28 .= coefficient(c) * 1.L by POLYNOM2:14 .= coefficient(c); then y = <* coefficient(c) *> by A1,A27,FINSEQ_1:40; hence thesis by A2,RLVECT_1:44; end; end; hence thesis; end; theorem Th25: for n being Ordinal, L being right_zeroed add-associative right_complementable well-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 well-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; begin :: Multiplication with Coefficients 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 :Def9: 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 FUNCT_2:sch 4; 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 PRE_POLY:def 12; 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 b9 = b as bag of X; thus p1.b = a * p.b9 by A2 .= p2.b by A3; end; hence p1 = p2; end; func p * a -> Series of X,L means :Def10: 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 FUNCT_2:sch 4; 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 PRE_POLY:def 12; 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 b9 = b as bag of X; thus p1.b = p.b9 * a by A5 .= p2.b by A6; end; hence p1 = p2; end; end; registration 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; now let u be object; assume A1: u in Support ap; then reconsider u9 = u as Element of Bags X; ap.u <> 0.L by A1,POLYNOM1:def 4; then a * p.u9 <> 0.L by Def9; then p.u9 <> 0.L by BINOM:2; hence u in Support p by POLYNOM1:def 4; end; then Support p is finite & Support ap c= Support p by POLYNOM1:def 5 ,TARSKI:def 3; hence thesis by POLYNOM1:def 5; end; cluster p * a -> finite-Support; coherence proof set ap = p * a; now let u be object; assume A2: u in Support ap; then reconsider u9 = u as Element of Bags X; ap.u <> 0.L by A2,POLYNOM1:def 4; then p.u9 * a <> 0.L by Def10; then p.u9 <> 0.L by BINOM:1; hence u in Support p by POLYNOM1:def 4; end; then Support p is finite & Support ap c= Support p by POLYNOM1:def 5 ,TARSKI:def 3; hence thesis by POLYNOM1:def 5; 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 b9 = b as bag of n; thus (a * p).b = a * p.b9 by Def9 .= (p * a).b by Def10; end; hence thesis; 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; for x being object st x in Bags n holds (a * p).x = (a |(n,L) *' p).x proof set O = a |(n,L), cL = the carrier of L; let x be object; assume x in Bags n; then reconsider b = x as bag of n; A1: 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 A2: (O*'p).b = Sum s and A3: len s = len decomp b and A4: for k being Element of 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 10; s is non empty by A3; then consider s1 being Element of cL, t being FinSequence of cL such that A5: s1 = s.1 and A6: s = <*s1*>^t by FINSEQ_3:102; A7: Sum s = (Sum <*s1*>) + (Sum t) by A6,RLVECT_1:41; A8: now per cases; suppose t = <*>(cL); hence (Sum t) = 0.L by RLVECT_1:43; end; suppose A9: t <> <*>(cL); now let k be Nat; A10: len s = len t + len <*s1*> by A6,FINSEQ_1:22 .= len t +1 by FINSEQ_1:39; assume A11: k in dom t; then A12: t/.k = t.k by PARTFUN1:def 6 .= s.(k+1) by A6,A11,FINSEQ_3:103; 1 <= k by A11,FINSEQ_3:25; then A13: 1 < k+1 by NAT_1:13; k <= len t by A11,FINSEQ_3:25; then A14: k+1 <= len s by A10,XREAL_1:6; then A15: k+1 in dom decomp b by A3,A13,FINSEQ_3:25; A16: dom s = dom decomp b by A3,FINSEQ_3:29; then A17: s/.(k+1) = s.(k+1) by A15,PARTFUN1:def 6; per cases by A14,XXREAL_0:1; suppose A18: k+1 < len s; reconsider k1=k as Element of NAT by ORDINAL1:def 12; consider b1, b2 being bag of n such that A19: (decomp b)/.(k1+1) = <*b1, b2*> and A20: s/.(k1+1) = O.b1*p.b2 by A4,A16,A15; b1 <> EmptyBag n by A3,A13,A18,A19,PRE_POLY:72; hence t/.k = 0.L*p.b2 by A12,A17,A20,Th18 .= 0.L; end; suppose A21: k+1 = len s; A22: now assume b = EmptyBag n; then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73; then len t +1 = 0+1 by A3,A10,FINSEQ_1:39; hence contradiction by A9; end; consider b1, b2 being bag of n such that A23: (decomp b)/.(k+1) = <*b1, b2*> and A24: s/.(k+1) = O.b1*p.b2 by A4,A16,A15; (decomp b)/.(len s) = <*b,EmptyBag n*> by A3,PRE_POLY:71; then b2 = EmptyBag n & b1 = b by A21,A23,FINSEQ_1:77; then s.(k+1) = 0.L*(p.EmptyBag n) by A17,A24,A22,Th18 .= 0.L; hence t/.k = 0.L by A12; end; end; hence Sum t = 0.L by MATRLIN:11; end; end; A25: s is non empty by A3; then consider b1, b2 being bag of n such that A26: (decomp b)/.1 = <*b1, b2*> and A27: s/.1 = O.b1*p.b2 by A4,FINSEQ_5:6; 1 in dom s by A25,FINSEQ_5:6; then A28: s/.1 = s.1 by PARTFUN1:def 6; (decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71; then A29: b2 = b & b1 = EmptyBag n by A26,FINSEQ_1:77; Sum <*s1*> = s1 by RLVECT_1:44 .= a * p.b by A5,A27,A29,A28,Th18; hence thesis by A2,A7,A8,RLVECT_1:4; end; b is Element of Bags n by PRE_POLY:def 12; then (O*'p).b = a * p.b by A1 .= (a * p).b by Def9; hence thesis; end; hence thesis; 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; for x being object st x in Bags n holds (p * a).x = (p *' (a |(n,L))).x proof set O = a |(n,L), cL = the carrier of L; let x be object; assume x in Bags n; then reconsider b = x as bag of n; A1: 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 A2: (p*'O).b = Sum s and A3: len s = len decomp b and A4: for k being Element of 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 10; consider t being FinSequence of cL,s1 being Element of cL such that A5: s = t^<*s1*> by A3,FINSEQ_2:19; A6: now per cases; suppose t = <*>(cL); hence (Sum t) = 0.L by RLVECT_1:43; end; suppose A7: t <> <*>(cL); now let k be Nat; A8: len s = len t + len <*s1*> by A5,FINSEQ_1:22 .= len t +1 by FINSEQ_1:39; assume A9: k in dom t; then A10: t/.k = t.k by PARTFUN1:def 6 .= s.k by A5,A9,FINSEQ_1:def 7; k <= len t by A9,FINSEQ_3:25; then A11: k < len s by A8,NAT_1:13; A12: 1 <= k by A9,FINSEQ_3:25; then A13: k in dom decomp b by A3,A11,FINSEQ_3:25; A14: dom s = dom decomp b by A3,FINSEQ_3:29; then A15: s/.k = s.k by A13,PARTFUN1:def 6; per cases by A12,XXREAL_0:1; suppose A16: 1 < k; reconsider k1=k as Element of NAT by ORDINAL1:def 12; consider b1, b2 being bag of n such that A17: (decomp b)/.k1 = <*b1, b2*> and A18: s/.k1 = p.b1*O.b2 by A4,A14,A13; b2 <> EmptyBag n by A3,A11,A16,A17,PRE_POLY:72; hence t/.k = p.b1*0.L by A10,A15,A18,Th18 .= 0.L; end; suppose A19: k = 1; A20: now assume b = EmptyBag n; then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73; then len t +1 = 0+1 by A3,A8,FINSEQ_1:39; hence contradiction by A7; end; consider b1, b2 being bag of n such that A21: (decomp b)/.k = <*b1, b2*> and A22: s/.k = p.b1*O.b2 by A4,A14,A13; (decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71; then b1 = EmptyBag n & b2 = b by A19,A21,FINSEQ_1:77; then s.k = (p.EmptyBag n)*0.L by A15,A22,A20,Th18 .= 0.L; hence t/.k = 0.L by A10; end; end; hence Sum t = 0.L by MATRLIN:11; end; end; A23: s.len s = (t^<*s1*>).(len t +1) by A5,FINSEQ_2:16 .= s1 by FINSEQ_1:42; A24: Sum s = (Sum t) + (Sum <*s1*>) by A5,RLVECT_1:41; s is non empty by A3; then A25: len s in dom s by FINSEQ_5:6; then consider b1, b2 being bag of n such that A26: (decomp b)/.len s = <*b1, b2*> and A27: s/.len s = p.b1*O.b2 by A4; A28: s/.len s = s.len s by A25,PARTFUN1:def 6; (decomp b)/.len s = <*b,EmptyBag n*> by A3,PRE_POLY:71; then A29: b1 = b & b2 = EmptyBag n by A26,FINSEQ_1:77; Sum <*s1*> = s1 by RLVECT_1:44 .= p.b * a by A27,A29,A28,A23,Th18; hence thesis by A2,A24,A6,RLVECT_1:4; end; b is Element of Bags n by PRE_POLY:def 12; then (p*'O).b = p.b * a by A1 .= (p * a).b by Def10; hence thesis; end; hence thesis; end; Lm4: for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-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 well-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:25 .= a * eval(p,x) by Th25; end; Lm5: for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-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 well-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:25 .= eval(p,x) * a by Th25; end; theorem for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-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 well-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 left_add-cancelable add-associative right_complementable well-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 left_add-cancelable add-associative right_complementable well-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)) and A2: eval(a*p,x) = Sum y and A3: for i being Element of 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; A4: BagOrder n linearly_orders Support(a*p) by POLYNOM2:18; consider z being FinSequence of the carrier of L such that A5: len z = len SgmX(BagOrder n, Support p) and A6: eval(p,x) = Sum z and A7: for i being Element of 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; per cases; suppose A8: a = 0.L; A9: now let b be bag of n; thus (a*p).b = a * p.b by Def9 .= 0.L by A8; end; now assume Support(a*p) <> {}; then reconsider sp = Support(a*p) as non empty Subset of Bags n; set c = the Element of sp; (a*p).c <> 0.L by POLYNOM1:def 4; hence contradiction by A9; end; then rng(SgmX(BagOrder n, Support(a*p))) = {} by A4,PRE_POLY:def 2; then SgmX(BagOrder n, Support(a*p)) = {} by RELAT_1:41; then y = <*>(the carrier of L) by A1; then Sum y = 0.L by RLVECT_1:43 .= a * Sum z by A8; hence thesis by A2,A6; end; suppose A10: a <> 0.L; A11: for u being object holds u in Support(a*p) implies u in Support p proof let u be object; assume A12: u in Support(a*p); then reconsider u9 = u as Element of Bags n; (a*p).u <> 0.L by A12,POLYNOM1:def 4; then a * p.u9 <> 0.L by Def9; then p.u9 <> 0.L; hence thesis by POLYNOM1:def 4; end; A13: for u being object holds u in Support p implies u in Support(a*p) proof let u be object; assume A14: u in Support p; then reconsider u9 = u as Element of Bags n; p.u <> 0.L by A14,POLYNOM1:def 4; then a * p.u9 <> 0.L by A10,VECTSP_2:def 1; then (a * p).u9 <> 0.L by Def9; hence thesis by POLYNOM1:def 4; end; then A15: len z = len y by A1,A5,A11,TARSKI:2; then A16: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3; A17: Support(a*p) = Support(p) by A13,A11,TARSKI:2; now A18: dom(a*p) = Bags n by FUNCT_2:def 1; now let u be object; assume u in rng(SgmX(BagOrder n, Support(a*p))); then u in Support(a*p) by A4,PRE_POLY:def 2; hence u in dom(a*p) by A18; 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:16; for u being object holds u in rng r implies u in the carrier of L proof let u be object; assume u in rng r; then A19: u in rng(a*p) by FUNCT_1:14; rng(a*p) c= the carrier of L by RELAT_1:def 19; hence thesis by A19; end; then A20: rng r c= the carrier of L by TARSKI:def 3; A21: dom p = Bags n by FUNCT_2:def 1; now let u be object; assume u in rng(SgmX(BagOrder n, Support(a*p))); then u in Support(a*p) by A4,PRE_POLY:def 2; hence u in dom p by A21; 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:16; for u being object holds u in rng q implies u in the carrier of L proof let u be object; assume u in rng q; then A22: u in rng p by FUNCT_1:14; rng p c= the carrier of L by RELAT_1:def 19; hence thesis by A22; end; then A23: rng q c= the carrier of L by TARSKI:def 3; reconsider r as FinSequence of the carrier of L by A20,FINSEQ_1:def 4; reconsider q as FinSequence of the carrier of L by A23,FINSEQ_1:def 4; let i be object; assume A24: 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 A25: i = k and A26: 1 <= k & k <= len z; reconsider k as Element of NAT by ORDINAL1:def 12; A27: dom z = Seg(len SgmX(BagOrder n, Support(a*p))) by A1,A16,FINSEQ_1:def 3 .= dom(SgmX(BagOrder n, Support(a*p))) by FINSEQ_1:def 3; then (SgmX(BagOrder n, Support(a*p))).k = (SgmX(BagOrder n, Support(a*p) ))/.k by A24,A25,PARTFUN1:def 6; then k in dom q by A24,A25,A27,A21,FUNCT_1:11; then A28: (p * SgmX(BagOrder n, Support(a*p)))/.k = q.k by PARTFUN1:def 6 .= p.(SgmX(BagOrder n, Support(a*p)).k) by A24,A25,A27,FUNCT_1:13 .= p.(SgmX(BagOrder n, Support(a*p))/.k) by A24,A25,A27,PARTFUN1:def 6; reconsider c = SgmX(BagOrder n, Support(a*p))/.k as Element of Bags n; reconsider c as bag of n; A29: a * z/.k = a * ((p * SgmX(BagOrder n, Support p))/.k * eval(((SgmX( BagOrder n, Support p))/.k),x)) by A7,A26 .= (a * (p * SgmX(BagOrder n, Support(a*p)))/.k) * eval(((SgmX( BagOrder n, Support(a*p)))/.k),x) by A17,GROUP_1:def 3; A30: (a*p).(SgmX(BagOrder n, Support(a*p))/.k) = a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A28,Def9; (SgmX(BagOrder n, Support(a*p))).k = (SgmX(BagOrder n, Support(a*p) ))/.k by A24,A25,A27,PARTFUN1:def 6; then k in dom r by A24,A25,A27,A18,FUNCT_1:11; then ((a*p) * SgmX(BagOrder n, Support(a*p)))/.k = r.k by PARTFUN1:def 6 .= (a*p).(SgmX(BagOrder n, Support(a*p)).k) by A24,A25,A27,FUNCT_1:13 .= a * (p * SgmX(BagOrder n, Support(a*p)))/.k by A24,A25,A27,A30, PARTFUN1:def 6; hence y/.i = a * z/.i by A3,A15,A25,A26,A29; end; then y = a * z by A16,POLYNOM1:def 1; hence thesis by A2,A6,BINOM:4; end; end; theorem for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-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 well-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 left_add-cancelable add-associative right_complementable well-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 left_add-cancelable add-associative right_complementable well-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)) and A2: eval(p*a,x) = Sum y and A3: for i being Element of 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 A4: len z = len SgmX(BagOrder n, Support p) and A5: eval(p,x) = Sum z and A6: for i being Element of 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 A7: a = 0.L; A8: now let b be bag of n; thus (p*a).b = p.b * a by Def10 .= 0.L by A7; end; A9: now assume Support(p*a) <> {}; then reconsider sp = Support(p*a) as non empty Subset of Bags n; set c = the Element of sp; (p*a).c <> 0.L by POLYNOM1:def 4; hence contradiction by A8; end; BagOrder n linearly_orders Support(p*a) by POLYNOM2:18; then rng(SgmX(BagOrder n, Support(p*a))) = {} by A9,PRE_POLY:def 2; then SgmX(BagOrder n, Support(p*a)) = {} by RELAT_1:41; then y = <*>(the carrier of L) by A1; then Sum y = 0.L by RLVECT_1:43 .= Sum z * a by A7; hence thesis by A2,A5; end; case A10: a <> 0.L; A11: for u being object holds u in Support(p*a) implies u in Support p proof let u be object; assume A12: u in Support(p*a); then reconsider u9 = u as Element of Bags n; (p*a).u <> 0.L by A12,POLYNOM1:def 4; then p.u9 * a <> 0.L by Def10; then p.u9 <> 0.L; hence thesis by POLYNOM1:def 4; end; A13: for u being object holds u in Support p implies u in Support(p*a) proof let u be object; assume A14: u in Support p; then reconsider u9 = u as Element of Bags n; p.u <> 0.L by A14,POLYNOM1:def 4; then p.u9 * a <> 0.L by A10,VECTSP_2:def 1; then (p *a).u9 <> 0.L by Def10; hence thesis by POLYNOM1:def 4; end; then A15: len z = len y by A1,A4,A11,TARSKI:2; then A16: dom z = Seg(len y) by FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3; A17: BagOrder n linearly_orders Support(p*a) by POLYNOM2:18; A18: Support(p*a) = Support(p) by A13,A11,TARSKI:2; now A19: dom(p*a) = Bags n by FUNCT_2:def 1; now let u be object; assume u in rng(SgmX(BagOrder n, Support(p*a))); then u in Support(p*a) by A17,PRE_POLY:def 2; hence u in dom(p*a) by A19; 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:16; for u being object holds u in rng r implies u in the carrier of L proof let u be object; assume u in rng r; then A20: u in rng(p*a) by FUNCT_1:14; rng(p*a) c= the carrier of L by RELAT_1:def 19; hence thesis by A20; end; then A21: rng r c= the carrier of L by TARSKI:def 3; A22: dom p = Bags n by FUNCT_2:def 1; now let u be object; assume u in rng(SgmX(BagOrder n, Support(p*a))); then u in Support(p*a) by A17,PRE_POLY:def 2; hence u in dom p by A22; 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:16; for u being object holds u in rng q implies u in the carrier of L proof let u be object; assume u in rng q; then A23: u in rng p by FUNCT_1:14; rng p c= the carrier of L by RELAT_1:def 19; hence thesis by A23; end; then A24: rng q c= the carrier of L by TARSKI:def 3; reconsider r as FinSequence of the carrier of L by A21,FINSEQ_1:def 4; reconsider q as FinSequence of the carrier of L by A24,FINSEQ_1:def 4; let i be object; assume A25: 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 A26: i = k and A27: 1 <= k & k <= len z; reconsider k as Element of NAT by ORDINAL1:def 12; A28: dom z = Seg(len SgmX(BagOrder n, Support(p*a))) by A1,A16, FINSEQ_1:def 3 .= dom(SgmX(BagOrder n, Support(p*a))) by FINSEQ_1:def 3; then (SgmX(BagOrder n, Support(p*a))).k = (SgmX(BagOrder n, Support(p* a)))/.k by A25,A26,PARTFUN1:def 6; then k in dom q by A25,A26,A28,A22,FUNCT_1:11; then A29: (p * SgmX(BagOrder n, Support(p*a)))/.k = q.k by PARTFUN1:def 6 .= p.(SgmX(BagOrder n, Support(p*a)).k) by A25,A26,A28,FUNCT_1:13 .= p.(SgmX(BagOrder n, Support(p*a))/.k) by A25,A26,A28, PARTFUN1:def 6; reconsider c = SgmX(BagOrder n, Support(p*a))/.k as Element of Bags n; reconsider c as bag of n; A30: z/.k * a = (p * SgmX(BagOrder n, Support(p*a)))/.k * (eval(((SgmX (BagOrder n, Support(p*a)))/.k),x)) * a by A6,A18,A27 .= ((p * SgmX(BagOrder n, Support(p*a)))/.k * a) * eval(((SgmX( BagOrder n, Support(p*a)))/.k),x) by GROUP_1:def 3; A31: (p*a).(SgmX(BagOrder n, Support(p*a))/.k) = (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A29,Def10; (SgmX(BagOrder n, Support(p*a))).k = (SgmX(BagOrder n, Support(p* a)))/.k by A25,A26,A28,PARTFUN1:def 6; then k in dom r by A25,A26,A28,A19,FUNCT_1:11; then ((p*a) * SgmX(BagOrder n, Support(p*a)))/.k = r.k by PARTFUN1:def 6 .= (p*a).(SgmX(BagOrder n, Support(p*a)).k) by A25,A26,A28,FUNCT_1:13 .= (p * SgmX(BagOrder n, Support(p*a)))/.k * a by A25,A26,A28,A31, PARTFUN1:def 6; hence y/.i = z/.i * a by A3,A15,A26,A27,A30; end; then y = z * a by A16,POLYNOM1:def 2; hence thesis by A2,A5,BINOM:5; end; end; hence thesis; end; theorem for n being Ordinal, L being Abelian left_zeroed right_zeroed add-associative right_complementable well-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 well-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 well-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:25 .= eval(p,x) * a by Th25; end;