:: Preliminaries to Polynomials :: by Andrzej Trybulec :: :: Received August 7, 2009 :: Copyright (c) 2009-2018 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 NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0, BINOP_1, FUNCT_1, FINSOP_1, SETWISEO, XXREAL_0, TARSKI, NAT_1, ARYTM_3, WELLORD1, FINSUB_1, SETFAM_1, ORDERS_1, FINSET_1, ZFMISC_1, CARD_1, PARTFUN1, ARROW, ORDINAL2, ORDINAL1, RELAT_2, ARYTM_1, FINSEQ_3, FUNCOP_1, PBOOLE, FUNCT_4, FINSEQ_2, CARD_3, MEMBER_1, VALUED_0, FUNCT_2, BINOP_2, CLASSES1, PRE_POLY, FINSEQ_5, XCMPLX_0, WELLORD2, REAL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, WELLORD2, RELAT_1, XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, FINSET_1, FINSUB_1, SETWISEO, PARTFUN1, FUNCT_2, BINOP_2, FINSOP_1, FINSEQ_1, FINSEQ_4, FUNCT_3, BINOP_1, XREAL_0, FINSEQ_2, FUNCT_4, FINSEQ_5, WELLORD1, ORDERS_1, CARD_3, WSIERP_1, FUNCOP_1, FUNCT_7, NAT_D, INT_1, NAT_1, CLASSES1, VALUED_0, VALUED_1, ORDINAL2, SETFAM_1, DOMAIN_1, ARROW, FINSEQOP; constructors WELLORD2, BINOP_1, SETWISEO, CARD_3, FINSEQOP, FINSOP_1, FINSEQ_4, RFINSEQ, RFUNCT_3, NAT_D, WSIERP_1, FUNCT_7, RECDEF_1, BINOP_2, CLASSES1, BINARITH, ARROW, TOLER_1, ORDINAL2, RELSET_1, ORDERS_1, RELAT_2, WELLORD1, DOMAIN_1, SETFAM_1, ORDINAL3, PBOOLE, FINSEQ_5, REAL_1, FUNCT_4, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL3, FINSET_1, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, FINSEQ_2, CARD_3, PARTFUN1, VALUED_0, VALUED_1, RELSET_1, FUNCT_2, SETFAM_1, FINSUB_1, INT_1, PBOOLE; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: from LANG1 definition let D be set; let p, q be Element of D*; redefine func p^q -> Element of D*; end; registration let D be set; cluster empty for Element of D*; end; definition let D be set; redefine func <*> D -> empty Element of D*; end; definition let D be non empty set; let d be Element of D; redefine func <*d*> -> Element of D*; let e be Element of D; redefine func <*d,e*> -> Element of D*; end; begin :: from DTCONSTR registration let X be set; cluster -> FinSequence-like for Element of X*; end; definition let D be set, F be FinSequence of D*; func FlattenSeq F -> Element of D* means :: PRE_POLY:def 1 ex g being BinOp of D* st (for p, q being Element of D* holds g.(p,q) = p^q) & it = g "**" F; end; theorem :: PRE_POLY:1 for D being set, d be Element of D* holds FlattenSeq <*d*> = d; :: from SCMFSA_7, 2006.03.14, A.T. theorem :: PRE_POLY:2 for D being set holds FlattenSeq <*>(D*) = <*>D; theorem :: PRE_POLY:3 for D being set, F,G be FinSequence of D* holds FlattenSeq (F ^ G) = FlattenSeq F ^ FlattenSeq G; theorem :: PRE_POLY:4 for D being set, p,q be Element of D* holds FlattenSeq <* p,q *> = p ^ q; theorem :: PRE_POLY:5 for D being set, p,q,r be Element of D* holds FlattenSeq <* p,q,r *> = p ^ q ^ r; :: from SCMFSA_7, 2007.07.22, A.T. theorem :: PRE_POLY:6 for D being set, F,G be FinSequence of D* holds F c= G implies FlattenSeq F c= FlattenSeq G; begin :: from TRIANG_1 reserve A for set, x,y,z for object, k for Element of NAT; scheme :: PRE_POLY:sch 1 Regr1 { n() -> Nat, P[set] }: for k st k <= n() holds P[k] provided P[n()] and for k st k < n() & P[k+1] holds P[k]; registration let n be Nat; cluster Seg (n+1) -> non empty; end; theorem :: PRE_POLY:7 {}|_2 A = {}; registration let X be set; cluster non empty for Subset of Fin X; end; registration let X be non empty set; cluster non empty with_non-empty_elements for Subset of Fin X; end; registration let X be non empty set, F be non empty with_non-empty_elements Subset of Fin X; cluster non empty for Element of F; end; registration let X be non empty set; cluster with_non-empty_element for Subset of Fin X; end; definition let X be non empty set, R be Order of X, A be Subset of X; redefine func R|_2 A -> Order of A; end; scheme :: PRE_POLY:sch 2 SubFinite{D()->set, A()->Subset of D(), P[set]}: P[A()] provided A() is finite and P[{}(D())] and for x being Element of D(), B being Subset of D() st x in A() & B c= A() & P[B] holds P[B \/ {x}]; registration let X be non empty set, F be with_non-empty_element Subset of Fin X; cluster finite non empty for Element of F; end; definition let X be set, A be finite Subset of X, R be Order of X; assume R linearly_orders A; func SgmX (R,A) -> FinSequence of X means :: PRE_POLY:def 2 rng it = A & for n,m be Nat st n in dom it & m in dom it & n < m holds it/.n <> it/.m & [it/.n,it/.m] in R; end; ::\$CT theorem :: PRE_POLY:9 for X be set, A be finite Subset of X, R be Order of X, f be FinSequence of X st rng f = A & for n,m be Nat st n in dom f & m in dom f & n < m holds f/.n <> f/.m & [f/.n, f/.m] in R holds f = SgmX(R,A); registration let X be set, F be non empty Subset of Fin X; cluster -> finite for Element of F; end; definition let X be set, F be non empty Subset of Fin X; redefine mode Element of F -> Subset of X; end; theorem :: PRE_POLY:10 for X being set, A being finite Subset of X, R being Order of X st R linearly_orders A holds SgmX(R,A) is one-to-one; theorem :: PRE_POLY:11 for X being set, A being finite Subset of X, R being Order of X st R linearly_orders A holds len(SgmX(R, A)) = card A; begin :: from MATRLIN reserve n for Nat, x for object; theorem :: PRE_POLY:12 for M be FinSequence st len M = n+1 holds len Del(M,n+1) = n; theorem :: PRE_POLY:13 for M being FinSequence st M <> {} holds M = Del(M,len M) ^ <*M.(len M)*>; definition let IT be Function; attr IT is FinSequence-yielding means :: PRE_POLY:def 3 for x st x in dom IT holds IT.x is FinSequence; end; registration cluster FinSequence-yielding for Function; end; definition let F,G be FinSequence-yielding Function; func F^^G -> Function means :: PRE_POLY:def 4 dom it = dom F /\ dom G & for i being set st i in dom it for f,g being FinSequence st f = F.i & g = G.i holds it.i = f^g; end; registration let F,G be FinSequence-yielding Function; cluster F^^G -> FinSequence-yielding; end; begin :: HEYTING2 reserve V, C for set; theorem :: PRE_POLY:14 for V, C being non empty set ex f be Element of PFuncs (V, C) st f <> {}; theorem :: PRE_POLY:15 for f being Element of PFuncs (V, C), g being set st g c= f holds g in PFuncs (V, C); theorem :: PRE_POLY:16 PFuncs(V,C) c= bool [:V,C:]; theorem :: PRE_POLY:17 V is finite & C is finite implies PFuncs (V, C) is finite; registration cluster functional finite non empty for set; end; begin :: GOBRD13 registration let D be set; cluster -> FinSequence-yielding for FinSequence of D*; end; registration cluster FinSequence-yielding -> Function-yielding for Function; end; begin :: POLYNOM1 theorem :: PRE_POLY:18 for X being set, R being Relation st field R c= X holds R is Relation of X; registration let X be set, f be ManySortedSet of X, x, y be object; cluster f+*(x,y) -> X-defined; end; registration let X be set, f be ManySortedSet of X, x, y be object; cluster f+*(x,y) -> total for X-defined Function; end; theorem :: PRE_POLY:19 for f being one-to-one Function holds card f = card rng f; definition let A be set; let X be set, D be non empty FinSequenceSet of A, p be PartFunc of X,D, i be set; redefine func p/.i -> Element of D; end; registration let X be set; cluster being_linear-order well-ordering for Order of X; end; theorem :: PRE_POLY:20 for X being non empty set, A being non empty finite Subset of X, R being Order of X, x being Element of X st x in A & R linearly_orders A & for y being Element of X st y in A holds [x,y] in R holds (SgmX (R,A))/.1 = x; theorem :: PRE_POLY:21 for X being non empty set, A being non empty finite Subset of X, R being Order of X, x being Element of X st x in A & R linearly_orders A & for y being Element of X st y in A holds [y,x] in R holds SgmX (R,A)/.len SgmX (R,A ) = x; registration let X be non empty set, A be non empty finite Subset of X, R be being_linear-order Order of X; cluster SgmX(R, A) -> non empty one-to-one; end; registration cluster empty -> FinSequence-yielding for Function; end; registration let F, G be FinSequence-yielding FinSequence; cluster F^^G -> FinSequence-like; end; registration let i be Element of NAT, f be FinSequence; cluster i |-> f -> FinSequence-yielding; end; registration let F be FinSequence-yielding FinSequence, x be object; cluster F.x -> FinSequence-like; end; registration let F be FinSequence; cluster Card F -> FinSequence-like; end; registration cluster Cardinal-yielding for FinSequence; end; theorem :: PRE_POLY:22 for f being Function holds f is Cardinal-yielding iff for y being set st y in rng f holds y is Cardinal; registration let F, G be Cardinal-yielding FinSequence; cluster F^G -> Cardinal-yielding; end; registration cluster -> Cardinal-yielding for FinSequence of NAT; end; registration cluster Cardinal-yielding for FinSequence of NAT; end; definition let D be set; let F be FinSequence of D*; redefine func Card F -> Cardinal-yielding FinSequence of NAT; end; registration let F be FinSequence of NAT, i be Element of NAT; cluster F|i -> Cardinal-yielding; end; theorem :: PRE_POLY:23 for F being Function, X being set holds Card (F|X) = (Card F)|X; registration let F be empty Function; cluster Card F -> empty; end; theorem :: PRE_POLY:24 for p being set holds Card <*p*> = <*card p*>; theorem :: PRE_POLY:25 for F, G be FinSequence holds Card (F^G) = Card F ^ Card G; registration let X be set; cluster <*>X -> FinSequence-yielding; end; registration let f be FinSequence; cluster <*f*> -> FinSequence-yielding; end; theorem :: PRE_POLY:26 for f being Function holds f is FinSequence-yielding iff for y being set st y in rng f holds y is FinSequence; registration let F, G be FinSequence-yielding FinSequence; cluster F^G -> FinSequence-yielding; end; registration let D be set, F be empty FinSequence of D*; cluster FlattenSeq F -> empty; end; theorem :: PRE_POLY:27 for D being set, F being FinSequence of D* holds len FlattenSeq F = Sum Card F; theorem :: PRE_POLY:28 for D, E being set, F being FinSequence of D*, G being FinSequence of E* st Card F = Card G holds len FlattenSeq F = len FlattenSeq G; theorem :: PRE_POLY:29 for D being set, F being FinSequence of D*, k being set st k in dom FlattenSeq F ex i, j being Nat st i in dom F & j in dom (F.i) & k = (Sum Card (F|(i-'1))) + j & (F.i).j = (FlattenSeq F).k; theorem :: PRE_POLY:30 for D being set, F being FinSequence of D*, i, j being Element of NAT st i in dom F & j in dom (F.i) holds (Sum Card (F|(i-'1))) + j in dom FlattenSeq F & (F.i).j = (FlattenSeq F).((Sum Card (F|(i-'1))) + j); theorem :: PRE_POLY:31 for X, Y being non empty set, f being FinSequence of X*, v being Function of X, Y holds (dom f --> v)**f is FinSequence of Y*; theorem :: PRE_POLY:32 for X, Y being non empty set, f being FinSequence of X*, v being Function of X, Y ex F being FinSequence of Y* st F = (dom f --> v)**f & v* FlattenSeq f = FlattenSeq F; begin :: Functions yielding natural and real numbers ------------------------- registration let f be natural-valued Function, x be object, n be Nat; cluster f+*(x,n) -> natural-valued; end; registration let f be real-valued Function, x be object, n be Real; cluster f+*(x,n) -> real-valued; end; definition let X be set, b1, b2 be complex-valued ManySortedSet of X; redefine func b1+b2 -> ManySortedSet of X means :: PRE_POLY:def 5 for x being object holds it.x = b1.x+b2.x; end; definition let X be set, b1, b2 be natural-valued ManySortedSet of X; func b1 -' b2 -> ManySortedSet of X means :: PRE_POLY:def 6 for x being object holds it.x = b1.x -' b2.x; end; theorem :: PRE_POLY:33 for X being set, b, b1, b2 being real-valued ManySortedSet of X st for x being object st x in X holds b.x = b1.x+b2.x holds b = b1+b2; theorem :: PRE_POLY:34 for X being set, b, b1, b2 being natural-valued ManySortedSet of X st for x being object st x in X holds b.x = b1.x-'b2.x holds b = b1-'b2; registration let X be set, b1, b2 be natural-valued ManySortedSet of X; cluster b1+b2 -> natural-valued; cluster b1-'b2 -> natural-valued; end; theorem :: PRE_POLY:35 for X being set, b1, b2, b3 being real-valued ManySortedSet of X holds (b1+b2)+b3 = b1+(b2+b3); theorem :: PRE_POLY:36 for X being set, b, c, d being natural-valued ManySortedSet of X holds b-'c-'d = b-'(c+d); begin :: The support of a function -------------------------------------------- definition let f be Function; func support f -> set means :: PRE_POLY:def 7 for x being object holds x in it iff f.x <> 0; end; theorem :: PRE_POLY:37 for f being Function holds support f c= dom f; definition let f be Function; attr f is finite-support means :: PRE_POLY:def 8 support f is finite; end; registration cluster finite -> finite-support for Function; end; registration cluster natural-valued finite-support non empty for Function; end; registration let f be finite-support Function; cluster support f -> finite; end; registration let X be set; cluster finite-support for Function of X, NAT; end; registration let f be finite-support Function, x, y be set; cluster f+*(x,y) -> finite-support; end; registration let X be set; cluster natural-valued finite-support for ManySortedSet of X; end; theorem :: PRE_POLY:38 for X being set, b1, b2 being natural-valued ManySortedSet of X holds support (b1+b2) = support b1 \/ support b2; theorem :: PRE_POLY:39 for X being set, b1, b2 being natural-valued ManySortedSet of X holds support (b1-'b2) c= support b1; begin :: Bags ----------------------------------------------------------------- definition let X be set; mode bag of X is natural-valued finite-support ManySortedSet of X; end; registration let X be finite set; cluster -> finite-support for ManySortedSet of X; end; registration let X be set, b1, b2 be bag of X; cluster b1+b2 -> finite-support; cluster b1-'b2 -> finite-support; end; theorem :: PRE_POLY:40 for X being set holds X--> 0 is bag of X; definition let n be Ordinal, p, q be bag of n; pred p < q means :: PRE_POLY:def 9 ex k being Ordinal st p.k < q.k & for l being Ordinal st l in k holds p.l = q.l; asymmetry; end; theorem :: PRE_POLY:41 for n being Ordinal, p, q, r being bag of n st p < q & q < r holds p < r; definition let n be Ordinal, p, q be bag of n; pred p <=' q means :: PRE_POLY:def 10 p < q or p = q; reflexivity; end; theorem :: PRE_POLY:42 for n being Ordinal, p, q, r being bag of n st p <=' q & q <=' r holds p <=' r; theorem :: PRE_POLY:43 for n being Ordinal, p, q, r being bag of n st p < q & q <=' r holds p < r; theorem :: PRE_POLY:44 for n being Ordinal, p, q, r being bag of n st p <=' q & q < r holds p < r; theorem :: PRE_POLY:45 for n being Ordinal, p, q being bag of n holds p <=' q or q <=' p; definition let X be set, d, b be bag of X; pred d divides b means :: PRE_POLY:def 11 for k being object holds d.k <= b.k; reflexivity; end; theorem :: PRE_POLY:46 for n being set, d, b being bag of n st for k being object st k in n holds d.k <= b.k holds d divides b; theorem :: PRE_POLY:47 for n being set, b1, b2 being bag of n st b1 divides b2 holds b2 -' b1 + b1 = b2; theorem :: PRE_POLY:48 for X being set, b1, b2 being bag of X holds b2 + b1 -' b1 = b2; theorem :: PRE_POLY:49 for n being Ordinal, d, b being bag of n st d divides b holds d <=' b; theorem :: PRE_POLY:50 for n being set, b,b1,b2 being bag of n st b = b1 + b2 holds b1 divides b; definition let X be set; func Bags X -> set means :: PRE_POLY:def 12 for x being set holds x in it iff x is bag of X; end; definition let X be set; redefine func Bags X -> Subset of Bags X; end; theorem :: PRE_POLY:51 Bags {} = {{}}; registration let X be set; cluster Bags X -> non empty; end; registration let X be set; cluster -> functional for Subset of Bags X; end; registration let X be set, B be Subset of Bags X; cluster -> X-defined for Element of B; end; registration let X be set, B be non empty Subset of Bags X; cluster -> total natural-valued finite-support for Element of B; end; notation let X be set; synonym EmptyBag X for EmptyMS X; end; definition let X be set; redefine func EmptyBag X -> Element of Bags X; ::\$CD end; ::\$CT theorem :: PRE_POLY:53 for X be set, b being bag of X holds b+EmptyBag X = b; theorem :: PRE_POLY:54 for X be set, b being bag of X holds b-'EmptyBag X = b; theorem :: PRE_POLY:55 for X be set, b being bag of X holds (EmptyBag X) -' b = EmptyBag X; theorem :: PRE_POLY:56 for X being set, b being bag of X holds b-'b = EmptyBag X; theorem :: PRE_POLY:57 for n being set, b1, b2 be bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds b2 = b1; theorem :: PRE_POLY:58 for n being set, b being bag of n st b divides EmptyBag n holds EmptyBag n = b; theorem :: PRE_POLY:59 for n being set, b being bag of n holds EmptyBag n divides b; theorem :: PRE_POLY:60 for n being Ordinal, b being bag of n holds EmptyBag n <=' b; definition let n be Ordinal; func BagOrder n -> Order of Bags n means :: PRE_POLY:def 14 for p, q being bag of n holds [p, q] in it iff p <=' q; end; registration let n be Ordinal; cluster BagOrder n -> being_linear-order; end; definition let X be set, f be Function of X, NAT; func NatMinor f -> Subset of Funcs(X, NAT) means :: PRE_POLY:def 15 for g being natural-valued ManySortedSet of X holds g in it iff for x being set st x in X holds g.x <= f.x; end; theorem :: PRE_POLY:61 for X being set, f being Function of X, NAT holds f in NatMinor f; registration let X be set, f be Function of X, NAT; cluster NatMinor f -> non empty functional; end; registration let X be set, f be Function of X, NAT; cluster -> natural-valued for Element of NatMinor f; end; theorem :: PRE_POLY:62 for X being set, f being finite-support Function of X, NAT holds NatMinor f c= Bags X; definition let X be set, f be finite-support Function of X, NAT; redefine func support f -> Element of Fin X; end; theorem :: PRE_POLY:63 for X being non empty set, f being finite-support Function of X, NAT holds card NatMinor f = multnat \$\$ (support f, addnat[:](f,1)); registration let X be set, f be finite-support Function of X, NAT; cluster NatMinor f -> finite; end; definition let n be Ordinal, b be bag of n; func divisors b -> FinSequence of Bags n means :: PRE_POLY:def 16 ex S being non empty finite Subset of Bags n st it = SgmX(BagOrder n, S) & for p being bag of n holds p in S iff p divides b; end; registration let n be Ordinal, b be bag of n; cluster divisors b -> non empty one-to-one; end; theorem :: PRE_POLY:64 for n being Ordinal,i being Element of NAT, b being bag of n st i in dom divisors b holds ((divisors b)/.i) qua Element of Bags n divides b; theorem :: PRE_POLY:65 for n being Ordinal, b being bag of n holds (divisors b)/.1 = EmptyBag n & (divisors b)/.len divisors b = b; theorem :: PRE_POLY:66 for n being Ordinal, i being Nat, b, b1, b2 being bag of n st i > 1 & i < len divisors b holds (divisors b)/.i <> EmptyBag n & (divisors b)/.i <> b; theorem :: PRE_POLY:67 for n being Ordinal holds divisors EmptyBag n = <* EmptyBag n *>; definition let n be Ordinal, b be bag of n; func decomp b -> FinSequence of 2-tuples_on Bags n means :: PRE_POLY:def 17 dom it = dom divisors b & for i being Element of NAT, p being bag of n st i in dom it & p = (divisors b)/.i holds it/.i = <*p, b-'p*>; end; theorem :: PRE_POLY:68 for n being Ordinal, i being Element of NAT, b being bag of n st i in dom decomp b ex b1, b2 being bag of n st (decomp b)/.i = <*b1, b2*> & b = b1+b2; theorem :: PRE_POLY:69 for n being Ordinal, b, b1, b2 being bag of n st b = b1+b2 ex i being Element of NAT st i in dom decomp b & (decomp b)/.i = <*b1, b2*>; theorem :: PRE_POLY:70 for n being Ordinal, i being Element of NAT, b,b1,b2 being bag of n st i in dom decomp b & (decomp b)/.i = <*b1, b2*> holds b1 = (divisors b) /.i; registration let n be Ordinal, b be bag of n; cluster decomp b -> non empty one-to-one FinSequence-yielding; end; registration let n be Ordinal, b be Element of Bags n; cluster decomp b -> non empty one-to-one FinSequence-yielding; end; theorem :: PRE_POLY:71 for n being Ordinal, b being bag of n holds (decomp b)/.1 = <* EmptyBag n, b*> & (decomp b)/.len decomp b = <*b, EmptyBag n*>; theorem :: PRE_POLY:72 for n being Ordinal, i being Nat, b, b1, b2 being bag of n st i > 1 & i < len decomp b & (decomp b)/.i = <*b1, b2*> holds b1 <> EmptyBag n & b2 <> EmptyBag n; theorem :: PRE_POLY:73 for n being Ordinal holds decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *>; theorem :: PRE_POLY:74 for n being Ordinal, b being bag of n, f, g being FinSequence of (3-tuples_on Bags n)* st dom f = dom decomp b & dom g = dom decomp b & (for k being Nat st k in dom f holds f.k = ((decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1) qua Element of Bags n))) ^^ ((len (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1) qua Element of Bags n))) |-> <*(((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)*>)) & (for k being Nat st k in dom g holds g.k = (( len (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2) qua Element of Bags n))) |-> <*((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1*>) ^^ (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2) qua Element of Bags n))) ex p being Permutation of dom FlattenSeq f st FlattenSeq g = (FlattenSeq f)*p; theorem :: PRE_POLY:75 for X being set, b1, b2 being real-valued ManySortedSet of X holds support (b1+b2) c= support b1 \/ support b2; registration let D be non empty set; let n be Nat; cluster -> FinSequence-yielding for FinSequence of n-tuples_on D; end; registration let k be Nat; let D be non empty set, M be FinSequence of k-tuples_on D; let x be set; cluster M/.x -> Function-like Relation-like; end; registration let k be Element of NAT; let D be non empty set, M be FinSequence of k-tuples_on D; let x be set; cluster M/.x -> D-valued FinSequence-like; end; begin :: from POLYNOM2, 2012.02.16, A.T. theorem :: PRE_POLY:76 for X being set, A being empty Subset of X, R being Order of X st R linearly_orders A holds SgmX(R,A) = {}; theorem :: PRE_POLY:77 for X being set, A being finite Subset of X, R be Order of X st R linearly_orders A for i,j being Element of NAT st i in dom(SgmX(R,A)) & j in dom(SgmX(R,A)) holds SgmX(R,A)/.i = SgmX(R,A)/.j implies i = j; theorem :: PRE_POLY:78 for X being set, A being finite Subset of X, a being Element of X st not a in A for B being finite Subset of X st B = {a} \/ A for R being Order of X st R linearly_orders B for k being Element of NAT st k in dom(SgmX(R ,B)) & SgmX(R,B)/.k = a for i being Element of NAT st 1 <= i & i <= k - 1 holds SgmX(R,B)/.i = SgmX(R,A)/.i; theorem :: PRE_POLY:79 for X being set, A being finite Subset of X, a being Element of X st not a in A for B being finite Subset of X st B = {a} \/ A for R being Order of X st R linearly_orders B for k being Element of NAT st k in dom(SgmX(R ,B)) & SgmX(R,B)/.k = a for i being Element of NAT st k <= i & i <= len(SgmX(R, A)) holds SgmX(R,B)/.(i+1) = SgmX(R,A)/.i; theorem :: PRE_POLY:80 for X being non empty set, A being finite Subset of X, a being Element of X st not a in A for B being finite Subset of X st B = {a} \/ A for R being Order of X st R linearly_orders B for k being Element of NAT st k + 1 in dom(SgmX(R,B)) & SgmX(R,B)/.(k+1) = a holds SgmX(R,B) = Ins(SgmX(R,A),k,a); theorem :: PRE_POLY:81 for X being set, b being bag of X st support b = {} holds b = EmptyBag X; definition let X be set, b be bag of X; redefine attr b is empty-yielding means :: PRE_POLY:def 18 b = EmptyBag X; end; registration let X be non empty set; cluster non empty-yielding for bag of X; end; definition let X be set, b be bag of X; redefine func support b -> finite Subset of X; end; theorem :: PRE_POLY:82 for n being Ordinal, b being bag of n holds RelIncl n linearly_orders support b; definition let X be set; let x be FinSequence of X, b be bag of X; redefine func b * x -> PartFunc of NAT,NAT; end; registration let X be set; cluster support EmptyBag X -> empty; end;