### The Mizar article:

### Multivariate Polynomials with Arbitrary Number of Variables

**by****Piotr Rudnicki, and****Andrzej Trybulec**

- Received September 22, 1999
Copyright (c) 1999 Association of Mizar Users

- MML identifier: POLYNOM1
- [ MML identifier index ]

environ vocabulary MONOID_0, FUNCT_1, VECTSP_1, RELAT_1, BINOP_1, FUNCOP_1, PARTFUN1, ARYTM_1, RLVECT_1, FINSEQ_1, BOOLE, FUNCT_4, CAT_1, PBOOLE, CARD_1, FINSEQ_2, ORDERS_2, WELLORD1, ORDERS_1, RELAT_2, FINSET_1, TRIANG_1, MATRLIN, MEASURE6, SQUARE_1, CARD_3, REALSET1, GROUP_1, ALGSTR_1, LATTICES, DTCONSTR, MSUALG_3, SEQM_3, ALGSEQ_1, ORDINAL1, ARYTM_3, FUNCT_2, FRAENKEL, FINSUB_1, SETWISEO, TARSKI, RFINSEQ, POLYNOM1, FVSUM_1, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, RELAT_1, RELSET_1, RELAT_2, FUNCT_1, FINSET_1, FINSUB_1, SETWISEO, ORDINAL1, PBOOLE, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_4, NAT_1, REALSET1, ALGSTR_1, RLVECT_1, ORDERS_1, ORDERS_2, FINSEQ_1, FINSEQ_2, WELLORD1, SEQM_3, CARD_1, CARD_3, FINSEQ_4, CQC_LANG, VECTSP_1, GROUP_1, TRIANG_1, TREES_4, WSIERP_1, MONOID_0, MSUALG_3, FUNCOP_1, FUNCT_7, FRAENKEL, DTCONSTR, BINARITH, MATRLIN, RFUNCT_3, RFINSEQ, TOPREAL1, FVSUM_1; constructors ORDERS_2, WELLORD2, CQC_LANG, WELLFND1, TRIANG_1, FINSEQOP, REAL_1, FUNCT_7, DOMAIN_1, BINARITH, MATRLIN, MSUALG_3, WSIERP_1, TOPREAL1, ALGSTR_2, FVSUM_1, SETWOP_2, SETWISEO, MONOID_0, MEMBERED; clusters XREAL_0, STRUCT_0, RELAT_1, FUNCT_1, FINSET_1, RELSET_1, CARD_3, FINSEQ_5, CARD_1, ALGSTR_1, ALGSTR_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, PRALG_1, CIRCCOMB, CQC_LANG, BINARITH, ORDINAL3, HEYTING2, MONOID_0, GOBRD13, VECTSP_1, FRAENKEL, MEMBERED, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0, RLVECT_1, FUNCT_1, VECTSP_1, MATRLIN, CARD_3, RELAT_2, PBOOLE, RELSET_1, WELLORD2, FRAENKEL, RELAT_1, SEQM_3, GROUP_1, ANPROJ_1; theorems FUNCT_1, FINSET_1, FINSEQ_3, FINSEQ_4, ZFMISC_1, FINSEQ_1, FUNCT_2, RLVECT_1, VECTSP_1, FUNCOP_1, STRUCT_0, TARSKI, FUNCT_7, BINOP_1, RELAT_1, MSUALG_3, MATRLIN, FINSEQ_2, CARD_3, RFINSEQ, VECTSP_9, SCMFSA_7, DTCONSTR, GROUP_5, GROUP_7, CQC_LANG, RELSET_1, FUNCT_4, CARD_1, ORDINAL1, TOPREAL1, RVSUM_1, FINSEQ_5, AXIOMS, NAT_1, BINARITH, GOBOARD9, AMI_5, SPRECT_3, AMI_1, PBOOLE, NAT_2, SUBSET_1, ORDERS_1, ORDERS_2, EULER_1, WELLSET1, WELLORD1, RELAT_2, REAL_1, FVSUM_1, FUNCT_3, JORDAN3, JORDAN4, YELLOW_6, TRIANG_1, PRE_CIRC, ORDINAL3, CARD_4, SETWISEO, MONOID_0, SETWOP_2, SCMFSA6A, CARD_2, FUNCT_5, ALTCAT_1, FINSUB_1, SEQM_3, GROUP_1, ANPROJ_1, FSM_1, PARTFUN2, XBOOLE_0, XBOOLE_1, RLVECT_2, XCMPLX_1, PARTFUN1; schemes FRAENKEL, SETWISEO, FUNCT_2, FINSEQ_2, FINSEQ_5, GOBOARD2, MSUALG_1, RELSET_1, GOBOARD1, ORDINAL1, FUNCT_7, SUBSET_1, XBOOLE_0; begin :: Basics --------------------------------------------------------------- theorem Th1: for i, j being Nat holds multnat.(i,j) = i*j proof let i, j be Nat; A1: [i,j] in [:NAT,NAT:] by ZFMISC_1:106; thus multnat.(i,j) = (multreal|([:NAT,NAT:] qua set)).[i,j] by BINOP_1:def 1,MONOID_0:66 .= multreal.[i,j] by A1,FUNCT_1:72 .= multreal.(i,j) by BINOP_1:def 1 .= i*j by VECTSP_1:def 14; end; theorem Th2: for X being set, A being non empty set, F being BinOp of A, f being Function of X, A, x being Element of A holds dom (F[:](f,x)) = X proof let X be set, A be non empty set, F be BinOp of A, f be Function of X, A, x be Element of A; A1: rng (dom f --> x) c= {x} by FUNCOP_1:19; {x} c= A by ZFMISC_1:37; then A2: rng (dom f --> x) c= A by A1,XBOOLE_1:1; A3: rng f c= A by RELSET_1:12; A4: rng <:f, dom f --> x:> c= [:rng f, rng (dom f --> x):] by FUNCT_3:71; A5: [:rng f, rng (dom f --> x):] c= [:A,A:] by A2,A3,ZFMISC_1:119; dom F = [:A,A:] by FUNCT_2:def 1; then A6: rng <:f, dom f --> x:> c= dom F by A4,A5,XBOOLE_1:1; A7: dom (dom f --> x) = dom f by FUNCOP_1:19; thus dom (F[:](f,x)) = dom (F*<:f, dom f --> x:>) by FUNCOP_1:def 4 .= dom <:f, dom f --> x:> by A6,RELAT_1:46 .= dom f by A7,FUNCT_3:70 .= X by FUNCT_2:def 1; end; theorem Th3: for a, b, c being Nat holds a-'b-'c = a-'(b+c) proof let a, b, c be Nat; per cases; suppose A1: a <= b; then A2: a <= b+c by NAT_1:37; A3: 0 <= c by NAT_1:18; thus a-'b-'c = 0-'c by A1,NAT_2:10 .= 0 by A3,NAT_2:10 .= a-'(b+c) by A2,NAT_2:10; suppose A4: b <= a & a-b <= c; then A5: a <= b+c by REAL_1:86; a-'b = a-b by A4,SCMFSA_7:3; hence a-'b-'c = 0 by A4,NAT_2:10 .= a-'(b+c) by A5,NAT_2:10; suppose A6: b <= a & c <= a-b; then A7: c+b <= a by REAL_1:84; a-'b = a-b by A6,SCMFSA_7:3; hence a-'b-'c = a-b-c by A6,SCMFSA_7:3 .= a-(b+c) by XCMPLX_1:36 .= a-'(b+c) by A7,SCMFSA_7:3; end; theorem Th4: for X being set, R being Relation st field R c= X holds R is Relation of X proof let X be set, R be Relation; assume A1: field R c= X; let r be set; assume A2: r in R; then consider x, y being set such that A3: r = [x,y] by RELAT_1:def 1; x in field R & y in field R by A2,A3,RELAT_1:30; hence r in [:X, X:] by A1,A3,ZFMISC_1:def 2; end; theorem Th5: for K being non empty LoopStr, p1,p2 be FinSequence of the carrier of K st dom p1 = dom p2 holds dom(p1+p2) = dom p1 proof let K be non empty LoopStr, p1,p2 be FinSequence of the carrier of K; assume A1: dom p1 = dom p2; A2: rng p1 c= the carrier of K by FINSEQ_1:def 4; A3: rng p2 c= the carrier of K by FINSEQ_1:def 4; A4: rng <:p1,p2:> c= [:rng p1,rng p2:] by FUNCT_3:71; A5: [:rng p1,rng p2:] c= [:the carrier of K,the carrier of K:] by A2,A3,ZFMISC_1:119; [:the carrier of K,the carrier of K:] = dom (the add of K) by FUNCT_2:def 1; then A6: rng <:p1,p2:> c= dom (the add of K) by A4,A5,XBOOLE_1:1; thus dom (p1+p2) = dom ((the add of K).:(p1,p2)) by FVSUM_1:def 3 .= dom ((the add of K)*<:p1,p2:>) by FUNCOP_1:def 3 .= dom <:p1,p2:> by A6,RELAT_1:46 .= dom p1 /\ dom p2 by FUNCT_3:def 8 .= dom p1 by A1; end; theorem Th6: for f being Function, x,y being set holds rng (f+*(x,y)) c= rng f \/ {y} proof let f be Function, x,y be set; per cases; suppose not x in dom f; then (f+*(x,y)) = f by FUNCT_7:def 3; hence thesis by XBOOLE_1:7; suppose x in dom f; then (f+*(x,y)) = (f+*(x .--> y)) by FUNCT_7:def 3; then rng (f+*(x,y)) c= rng f \/ rng (x .--> y) by FUNCT_4:18; hence rng (f+*(x,y)) c= rng f \/ {y} by CQC_LANG:5; end; definition let A, B be set, f be Function of A, B, x be set, y be Element of B; redefine func f+*(x,y) -> Function of A, B; coherence proof set F = f+*(x,y); A1: rng F c= rng f \/ {y} by Th6; per cases; suppose A2: B is empty; rng f c= B by RELSET_1:12; then rng f = {} by A2,XBOOLE_1:3; then dom f is empty by RELAT_1:65; hence thesis by FUNCT_7:def 3; suppose A3: B is non empty; then A4: dom f = A & rng f c= B by FUNCT_2:def 1,RELSET_1:12; then A5: dom F = A by FUNCT_7:32; {y} c= B by A3,ZFMISC_1:37; then rng f \/ {y} c= B by A4,XBOOLE_1:8; then rng F c= B by A1,XBOOLE_1:1; hence thesis by A3,A5,FUNCT_2:def 1,RELSET_1:11; end; end; definition let X be set, f be ManySortedSet of X, x, y be set; redefine func f+*(x,y) -> ManySortedSet of X; coherence proof thus dom (f+*(x,y)) = dom f by FUNCT_7:32 .= X by PBOOLE:def 3; end; end; theorem Th7: for f being one-to-one Function holds Card (f qua set) = Card rng f proof let f be one-to-one Function; A1: Card rng f c= Card dom f by YELLOW_6:3; A2: Card rng (f") c= Card dom (f") by YELLOW_6:3; rng f = dom(f") & dom f = rng(f") by FUNCT_1:55; then Card rng f = Card dom f by A1,A2,XBOOLE_0:def 10; hence Card (f qua set) = Card rng f by PRE_CIRC:21; end; definition let A be non empty set; let F, G be BinOp of A, z, u be Element of A; cluster doubleLoopStr(# A, F, G, z, u #) -> non empty; coherence by STRUCT_0:def 1; end; definition let A be set; let X be set, D be FinSequence-DOMAIN of A, p be PartFunc of X,D, i be set; redefine func p/.i -> Element of D; coherence; end; definition let X be set, S be 1-sorted; mode Function of X, S is Function of X, the carrier of S; canceled; end; definition let X be set; cluster being_linear-order well-ordering Order of X; existence proof consider R being Relation such that A1: R is well-ordering and A2: field R = X by WELLSET1:9; reconsider R as Relation of X by A2,Th4; A3: R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded by A1,WELLORD1:def 4; A4: R is_reflexive_in X by A2,A3,RELAT_2:def 9; dom R = X by A4,ORDERS_1:98; then reconsider R as Order of X by A3,PARTFUN1:def 4; take R; thus thesis by A1,A3,ORDERS_2:def 3; end; end; theorem Th8: 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 proof let X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X; assume that A1: x in A and A2: R linearly_orders A and A3: for y being Element of X st y in A holds [x,y] in R and A4: SgmX (R,A)/.1 <> x; A5: A = rng SgmX (R,A) by A2,TRIANG_1:def 2; then consider i being Nat such that A6: i in dom SgmX (R,A) and A7: SgmX (R,A)/.i = x by A1,PARTFUN2:4; 1 <= i by A6,FINSEQ_3:27; then A8: 1 < i by A4,A7,AXIOMS:21; SgmX (R,A) is non empty by A2,RELAT_1:60,TRIANG_1:def 2; then A9: 1 in dom SgmX (R,A) by FINSEQ_5:6; then A10: [SgmX (R,A)/.1, x] in R by A2,A6,A7,A8,TRIANG_1:def 2; SgmX (R,A)/.1 in A by A5,A9,PARTFUN2:4; then A11: [x, SgmX (R,A)/.1] in R by A3; field R = X by ORDERS_1:97; then R is_antisymmetric_in X by RELAT_2:def 12; hence contradiction by A4,A10,A11,RELAT_2:def 4; end; theorem Th9: 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 proof let X be non empty set, A be non empty finite Subset of X, R be Order of X, x be Element of X; assume that A1: x in A and A2: R linearly_orders A and A3: for y being Element of X st y in A holds [y,x] in R and A4: SgmX (R,A)/.len SgmX (R,A) <> x; A5: A = rng SgmX (R,A) by A2,TRIANG_1:def 2; then consider i being Nat such that A6: i in dom SgmX (R,A) and A7: SgmX (R,A)/.i = x by A1,PARTFUN2:4; set L = len SgmX (R,A); i <= L by A6,FINSEQ_3:27; then A8: i < L by A4,A7,AXIOMS:21; SgmX (R,A) is non empty by A2,RELAT_1:60,TRIANG_1:def 2; then A9: L in dom SgmX (R,A) by FINSEQ_5:6; then A10: [x, SgmX (R,A)/.L] in R by A2,A6,A7,A8,TRIANG_1:def 2; SgmX (R,A)/.L in A by A5,A9,PARTFUN2:4; then A11: [SgmX (R,A)/.L,x] in R by A3; field R = X by ORDERS_1:97; then R is_antisymmetric_in X by RELAT_2:def 12; hence contradiction by A4,A10,A11,RELAT_2:def 4; end; definition 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; coherence proof A1: field R = X by ORDERS_2:2; R linearly_orders field R by ORDERS_2:35; then R linearly_orders A by A1,ORDERS_2:36; hence thesis by RELAT_1:60,TRIANG_1:8,def 2; end; end; definition cluster {} -> FinSequence-yielding; coherence proof let x be set; thus thesis; end; end; definition cluster FinSequence-yielding FinSequence; existence proof take {}; thus thesis; end; end; definition let F, G be FinSequence-yielding FinSequence; redefine func F^^G -> FinSequence-yielding FinSequence; coherence proof dom (F^^G) = dom F /\ dom G by MATRLIN:def 2 .= Seg len F /\ dom G by FINSEQ_1:def 3 .= Seg len F /\ Seg len G by FINSEQ_1:def 3 .= Seg min(len F, len G) by FINSEQ_2:2; hence thesis by FINSEQ_1:def 2; end; end; definition let i be Nat, f be FinSequence; cluster i |-> f -> FinSequence-yielding; coherence proof let x be set; assume x in dom (i |-> f); then x in Seg i by FINSEQ_2:68; hence thesis by FINSEQ_2:70; end; end; definition let F be FinSequence-yielding FinSequence, x be set; cluster F.x -> FinSequence-like; coherence proof per cases; suppose not x in dom F; hence thesis by FUNCT_1:def 4; suppose x in dom F; hence thesis by MATRLIN:def 1; end; end; definition let F be FinSequence; cluster Card F -> FinSequence-like; coherence proof dom Card F = dom F by CARD_3:def 2 .= Seg len F by FINSEQ_1:def 3; hence Card F is FinSequence-like by FINSEQ_1:def 2; end; end; definition cluster Cardinal-yielding FinSequence; existence proof take {}; {} is Cardinal-yielding proof let x be set; thus thesis; end; hence thesis; end; end; theorem Th10: for f being Function holds f is Cardinal-yielding iff for y being set st y in rng f holds y is Cardinal proof let f be Function; hereby assume A1: f is Cardinal-yielding; let y be set; assume y in rng f; then ex x being set st x in dom f & y = f.x by FUNCT_1:def 5; hence y is Cardinal by A1,CARD_3:def 1; end; assume A2: for y being set st y in rng f holds y is Cardinal; let x be set; assume x in dom f; then f.x in rng f by FUNCT_1:def 5; hence thesis by A2; end; definition let F, G be Cardinal-yielding FinSequence; cluster F^G -> Cardinal-yielding; coherence proof A1: rng (F^G) = rng F \/ rng G by FINSEQ_1:44; now let y be set; assume y in rng (F^G); then y in rng F or y in rng G by A1,XBOOLE_0:def 2; hence y is Cardinal by Th10; end; hence thesis by Th10; end; end; definition cluster -> Cardinal-yielding FinSequence of NAT; coherence proof let f be FinSequence of NAT; let x be set; assume x in dom f; then f.x in NAT by FINSEQ_2:13; hence f.x is Cardinal by CARD_1:65; end; end; definition cluster Cardinal-yielding FinSequence of NAT; existence proof take <*>NAT; thus thesis; end; end; definition let D be set; let F be FinSequence of D*; redefine func Card F -> Cardinal-yielding FinSequence of NAT; coherence proof rng Card F c= NAT proof let y be set; assume y in rng Card F; then consider x being set such that A1: x in dom Card F & y = (Card F).x by FUNCT_1:def 5; A2: x in dom F by A1,CARD_3:def 2; reconsider Fx = F.x as finite set; y = card Fx by A1,A2,CARD_3:def 2; hence thesis; end; hence thesis by FINSEQ_1:def 4; end; end; definition let F be FinSequence of NAT, i be Nat; cluster F|i -> Cardinal-yielding; coherence; end; theorem Th11: for F being Function, X being set holds Card (F|X) = (Card F)|X proof let F be Function, X be set; A1: dom ((Card F)|X) = dom (Card F) /\ X by RELAT_1:90 .= dom F /\ X by CARD_3:def 2 .= dom (F|X) by RELAT_1:90; now let x be set; assume A2: x in dom (F|X); A3: dom (F|X) c= dom F by RELAT_1:89; thus ((Card F)|X).x = (Card F).x by A1,A2,FUNCT_1:70 .= Card (F.x) by A2,A3,CARD_3:def 2 .= Card ((F|X).x) by A2,FUNCT_1:70; end; hence Card (F|X) = (Card F)|X by A1,CARD_3:def 2; end; definition let F be empty Function; cluster Card F -> empty; coherence proof dom F is empty; then dom Card F is empty by CARD_3:def 2; hence Card F is empty by RELAT_1:64; end; end; theorem Th12: for p being set holds Card <*p*> = <*Card p*> proof let p be set; set Cp = <*Card p*>; A1: dom Cp = {1} by FINSEQ_1:4,55; now let x be set; assume x in dom Cp; then x = 1 by A1,TARSKI:def 1; hence Cp.x is Cardinal by FINSEQ_1:57; end; then reconsider Cp as Cardinal-Function by CARD_3:def 1; A2: dom <*p*> = {1} by FINSEQ_1:4,55; now let x be set; assume x in dom <*p*>; then A3: x = 1 by A2,TARSKI:def 1; hence <*Card p*>.x = Card p by FINSEQ_1:57 .= Card (<*p*>.x) by A3,FINSEQ_1:57; end; then Card <*p*> = Cp by A1,A2,CARD_3:def 2; hence Card <*p*> = <*Card p*>; end; theorem Th13: for F, G be FinSequence holds Card (F^G) = Card F ^ Card G proof let F, G be FinSequence; A1: dom Card F = dom F by CARD_3:def 2; A2: dom Card G = dom G by CARD_3:def 2; A3: len Card F = len F by A1,FINSEQ_3:31; A4: len Card G = len G by A2,FINSEQ_3:31; A5: dom (Card F ^ Card G) = Seg (len Card F + len Card G) by FINSEQ_1:def 7 .= dom (F ^ G) by A3,A4,FINSEQ_1:def 7; now let x be set; assume A6: x in dom (F^G); then A7: x in Seg (len F + len G) by FINSEQ_1:def 7; reconsider k = x as Nat by A6; A8: 1 <= k & k <= len F + len G by A7,FINSEQ_1:3; per cases; suppose k <= len F; then A9: k in dom F by A8,FINSEQ_3:27; hence (Card F ^ Card G).x = (Card F).k by A1,FINSEQ_1:def 7 .= Card (F.k) by A9,CARD_3:def 2 .= Card ((F^G).x) by A9,FINSEQ_1:def 7; suppose len F < k; then not k in dom F by FINSEQ_3:27; then consider n being Nat such that A10: n in dom G & k = len F + n by A6,FINSEQ_1:38; thus (Card F ^ Card G).x = (Card G).n by A2,A3,A10,FINSEQ_1:def 7 .= Card (G.n) by A10,CARD_3:def 2 .= Card ((F^G).x) by A10,FINSEQ_1:def 7; end; hence Card (F^G) = Card F ^ Card G by A5,CARD_3:def 2; end; definition let X be set; cluster <*>X -> FinSequence-yielding; coherence; end; definition let f be FinSequence; cluster <*f*> -> FinSequence-yielding; coherence proof let x be set; assume x in dom <*f*>; then x in {1} by FINSEQ_1:4,55; then x = 1 by TARSKI:def 1; hence thesis by FINSEQ_1:57; end; end; theorem Th14: for f being Function holds f is FinSequence-yielding iff for y being set st y in rng f holds y is FinSequence proof let f be Function; hereby assume A1: f is FinSequence-yielding; let y be set; assume y in rng f; then ex x being set st x in dom f & y = f.x by FUNCT_1:def 5; hence y is FinSequence by A1,MATRLIN:def 1; end; assume A2: for y being set st y in rng f holds y is FinSequence; let x be set; assume x in dom f; then f.x in rng f by FUNCT_1:def 5; hence thesis by A2; end; definition let F, G be FinSequence-yielding FinSequence; cluster F^G -> FinSequence-yielding; coherence proof A1: rng (F^G) = rng F \/ rng G by FINSEQ_1:44; now let y be set; assume y in rng (F^G); then y in rng F or y in rng G by A1,XBOOLE_0:def 2; hence y is FinSequence by Th14; end; hence thesis by Th14; end; end; theorem Th15: for L being non empty LoopStr, F being FinSequence of (the carrier of L)* holds dom Sum F = dom F proof let L be non empty LoopStr, F be FinSequence of (the carrier of L)*; len Sum F = len F by MATRLIN:def 8; hence dom Sum F = dom F by FINSEQ_3:31; end; theorem Th16: for L being non empty LoopStr, F being FinSequence of (the carrier of L)* holds Sum (<*>((the carrier of L)*)) = <*>(the carrier of L) proof let L be non empty LoopStr, F be FinSequence of (the carrier of L)*; dom Sum (<*>((the carrier of L)*)) = dom (<*>((the carrier of L)* )) by Th15; hence Sum (<*>((the carrier of L)*)) = <*>(the carrier of L) by FINSEQ_1:26; end; theorem Th17: for L being non empty LoopStr, p being Element of (the carrier of L)* holds <*Sum p*> = Sum<*p*> proof let L be non empty LoopStr, p be Element of (the carrier of L)*; A1: dom <*Sum p*> = Seg 1 by FINSEQ_1:55 .= dom <*p*> by FINSEQ_1:55; then A2: len <*Sum p*> = len <*p*> by FINSEQ_3:31; now let i be Nat; assume i in dom<*p*>; then i in {1} by FINSEQ_1:4,55; then A3: i = 1 by TARSKI:def 1; hence <*Sum p*>/.i = Sum p by FINSEQ_4:25 .= Sum(<*p*>/.i) by A3,FINSEQ_4:25; end; hence <*Sum p*> = Sum<*p*> by A1,A2,MATRLIN:def 8; end; theorem Th18: for L being non empty LoopStr, F,G being FinSequence of (the carrier of L)* holds Sum(F^G) = Sum F ^ Sum G proof let L be non empty LoopStr, F, G be FinSequence of (the carrier of L)*; A1: dom Sum F = dom F by Th15; A2: dom Sum G = dom G by Th15; A3: len Sum F = len F by A1,FINSEQ_3:31; A4: len (Sum F^Sum G) = len Sum F + len Sum G by FINSEQ_1:35 .= len F + len Sum G by A1,FINSEQ_3:31 .= len F + len G by A2,FINSEQ_3:31 .= len (F^G) by FINSEQ_1:35; then A5: dom (Sum F^Sum G) = dom (F^G) by FINSEQ_3:31; now let i be Nat such that A6: i in dom (F^G); per cases by A6,FINSEQ_1:38; suppose A7: i in dom F; thus (Sum F^Sum G)/.i = (Sum F^Sum G).i by A5,A6,FINSEQ_4:def 4 .= (Sum F).i by A1,A7,FINSEQ_1:def 7 .= (Sum F)/.i by A1,A7,FINSEQ_4:def 4 .= Sum (F/.i) by A1,A7,MATRLIN:def 8 .= Sum((F^G)/.i) by A7,GROUP_5:95; suppose ex n being Nat st n in dom G & i = len F + n; then consider n being Nat such that A8: n in dom G and A9: i = len F + n; thus (Sum F^Sum G)/.i = (Sum F^Sum G).i by A5,A6,FINSEQ_4:def 4 .= (Sum G).n by A2,A3,A8,A9,FINSEQ_1:def 7 .= (Sum G)/.n by A2,A8,FINSEQ_4:def 4 .= Sum(G/.n) by A2,A8,MATRLIN:def 8 .= Sum((F^G)/.i) by A8,A9,GROUP_5:96; end; hence thesis by A4,A5,MATRLIN:def 8; end; definition let L be non empty HGrStr, p be FinSequence of the carrier of L, a be Element of L; redefine func a*p -> FinSequence of the carrier of L means :Def2: dom it = dom p & for i being set st i in dom p holds it/.i = a*(p/.i); compatibility proof set F = a*p; A1: F = (a multfield)*p by FVSUM_1:def 6; t1: rng p c= dom (a multfield) proof let x be set; B1: dom (a multfield) = the carrier of L by FUNCT_2:def 1; rng p c= the carrier of L by FINSEQ_1:def 4; hence thesis by B1; end; then T1: dom F = dom p by A1, RELAT_1:46; T2: for i being set st i in dom p holds F/.i = a*(p/.i) proof let i be set; assume AA: i in dom p; F.i = ((a multfield)*p).i by FVSUM_1:def 6 .= (a multfield).(p.i) by AA, FUNCT_1:23 .= (a multfield).(p/.i) by AA, FINSEQ_4:def 4 .= a * (p/.i) by FVSUM_1:61; hence thesis by AA, T1, FINSEQ_4:def 4; end; now let G be FinSequence of the carrier of L; assume F0: dom G = dom p & for i being set st i in dom p holds G/.i = a*(p/.i); set R = (a multfield)*p; F2: rng p c= the carrier of L by FINSEQ_1:def 4; dom (a multfield) = the carrier of L by FUNCT_2:def 1; then F1: dom G = dom R by F0, F2, RELAT_1:46; for k being set st k in dom G holds G.k = R.k proof let k be set; assume F3: k in dom G; then G.k = G/.k by FINSEQ_4:def 4 .= a*(p/.k) by F3, F0 .= (a multfield).(p/.k) by FVSUM_1:61 .= (a multfield).(p.k) by F3, F0, FINSEQ_4:def 4 .= R.k by F3, F0, FUNCT_1:23; hence thesis; end; then G = R by F1, FUNCT_1:9; hence G = a * p by FVSUM_1:def 6; end; hence thesis by t1, T2, A1, RELAT_1:46; end; correctness; end; definition let L be non empty HGrStr, p be FinSequence of the carrier of L, a be Element of L; func p*a -> FinSequence of the carrier of L means :Def3: dom it = dom p & for i being set st i in dom p holds it/.i = (p/.i)*a; existence proof deffunc F(set) = (p/.$1)*a; consider f being FinSequence of the carrier of L such that A9: len f = len p and A10: for j being Nat st j in dom f holds f/.j = F(j) from PiLambdaD; take f; thus A11: dom f = dom p by A9,FINSEQ_3:31; let j be set; assume j in dom p; hence f/.j = (p/.j)*a by A10,A11; end; uniqueness proof let it1, it2 be FinSequence of the carrier of L such that A12: dom it1 = dom p and A13: for i being set st i in dom p holds it1/.i = (p/.i)*a and A14: dom it2 = dom p and A15: for i being set st i in dom p holds it2/.i = (p/.i)*a; now let j be Nat; assume A16: j in dom p; hence it1/.j = (p/.j)*a by A13 .= it2/.j by A15,A16; end; hence it1 = it2 by A12,A14,FINSEQ_5:13; end; end; theorem Th19: for L being non empty HGrStr, a being Element of L holds a*<*>(the carrier of L) = <*>(the carrier of L) proof let L be non empty HGrStr, a be Element of L; dom (a*<*>(the carrier of L)) = dom <*>(the carrier of L) by Def2; hence a*<*>(the carrier of L) = <*>(the carrier of L) by RELAT_1:64; end; theorem Th20: for L being non empty HGrStr, a being Element of L holds (<*>the carrier of L)*a = <*>(the carrier of L) proof let L be non empty HGrStr, a be Element of L; dom((<*>the carrier of L)*a) = dom <*>(the carrier of L) by Def3; hence (<*>the carrier of L)*a = <*>(the carrier of L) by RELAT_1:64; end; theorem Th21: for L being non empty HGrStr, a, b being Element of L holds a*<*b*> = <*a*b*> proof let L be non empty HGrStr, a, b be Element of L; A1: dom<*a*b*> = Seg 1 by FINSEQ_1:55 .= dom<*b*> by FINSEQ_1:55; for i being set st i in dom<*b*> holds <*a*b*>/.i = a*(<*b*>/.i) proof let i be set; assume i in dom<*b*>; then i in {1} by FINSEQ_1:4,55; then A2: i = 1 by TARSKI:def 1; hence <*a*b*>/.i = a*b by FINSEQ_4:25 .= a*(<*b*>/.i) by A2,FINSEQ_4:25; end; hence a*<*b*> = <*a*b*> by A1,Def2; end; theorem Th22: for L being non empty HGrStr, a, b being Element of L holds <*b*>*a = <*b*a*> proof let L be non empty HGrStr, a, b be Element of L; A1: dom<*b*a*> = Seg 1 by FINSEQ_1:55 .= dom<*b*> by FINSEQ_1:55; for i being set st i in dom<*b*> holds <*b*a*>/.i = (<*b*>/.i)*a proof let i be set; assume i in dom<*b*>; then i in {1} by FINSEQ_1:4,55; then A2: i = 1 by TARSKI:def 1; hence <*b*a*>/.i = b*a by FINSEQ_4:25 .= (<*b*>/.i)*a by A2,FINSEQ_4:25; end; hence <*b*>*a = <*b*a*> by A1,Def3; end; theorem Th23: for L being non empty HGrStr, a being Element of L, p, q being FinSequence of the carrier of L holds a*(p^q) = (a*p)^(a*q) proof let L be non empty HGrStr, a be Element of L, p, q be FinSequence of the carrier of L; A1: dom (a*p) = dom p by Def2; then A2: len (a*p) = len p by FINSEQ_3:31; A3: dom (a*q) = dom q by Def2; then A4: len (a*q) = len q by FINSEQ_3:31; A5: len ((a*p)^(a*q)) = len (a*p) + len (a*q) by FINSEQ_1:35 .= len (p^q) by A2,A4,FINSEQ_1:35; A6: dom (a*(p^q)) = dom (p^q) by Def2; then A7: dom (a*(p^q)) = dom ((a*p)^(a*q)) by A5,FINSEQ_3:31; now let i be Nat; assume A8: i in dom (a*(p^q)); per cases by A6,A8,FINSEQ_1:38; suppose A9: i in dom p; thus (a*(p^q))/.i = a*((p^q)/.i) by A6,A8,Def2 .= a*(p/.i) by A9,GROUP_5:95 .= (a*p)/.i by A9,Def2 .= ((a*p)^(a*q))/.i by A1,A9,GROUP_5:95; suppose ex n being Nat st n in dom q & i = len p+n; then consider n being Nat such that A10: n in dom q & i = len p+n; thus (a*(p^q))/.i = a*((p^q)/.i) by A6,A8,Def2 .= a*(q/.n) by A10,GROUP_5:96 .= (a*q)/.n by A10,Def2 .= ((a*p)^(a*q))/.i by A2,A3,A10,GROUP_5:96; end; hence a*(p^q) = (a*p)^(a*q) by A7,FINSEQ_5:13; end; theorem Th24: for L being non empty HGrStr, a being Element of L, p, q being FinSequence of the carrier of L holds (p^q)*a = (p*a)^(q*a) proof let L be non empty HGrStr, a be Element of L, p, q be FinSequence of the carrier of L; A1: dom (p*a) = dom p by Def3; then A2: len (p*a) = len p by FINSEQ_3:31; A3: dom (q*a) = dom q by Def3; then A4: len (q*a) = len q by FINSEQ_3:31; A5: len ((p*a)^(q*a)) = len (p*a) + len (q*a) by FINSEQ_1:35 .= len (p^q) by A2,A4,FINSEQ_1:35; A6: dom ((p^q)*a) = dom (p^q) by Def3; then A7: dom ((p^q)*a) = dom ((p*a)^(q*a)) by A5,FINSEQ_3:31; now let i be Nat; assume A8: i in dom ((p^q)*a); per cases by A6,A8,FINSEQ_1:38; suppose A9: i in dom p; thus ((p^q)*a)/.i = ((p^q)/.i)*a by A6,A8,Def3 .= (p/.i)*a by A9,GROUP_5:95 .= (p*a)/.i by A9,Def3 .= ((p*a)^(q*a))/.i by A1,A9,GROUP_5:95; suppose ex n being Nat st n in dom q & i = len p+n; then consider n being Nat such that A10: n in dom q & i = len p+n; thus (p^q*a)/.i = ((p^q)/.i)*a by A6,A8,Def3 .= (q/.n)*a by A10,GROUP_5:96 .= (q*a)/.n by A10,Def3 .= ((p*a)^(q*a))/.i by A2,A3,A10,GROUP_5:96; end; hence (p^q)*a = (p*a)^(q*a) by A7,FINSEQ_5:13; end; definition cluster non degenerated -> non trivial (non empty multLoopStr_0); coherence proof let K be non empty multLoopStr_0; assume 0.K <> 1_ K; hence thesis by ANPROJ_1:def 8; end; end; definition cluster unital (non empty strict multLoopStr_0); existence proof take multEX_0; thus thesis; end; end; definition cluster strict Abelian add-associative right_zeroed right_complementable associative commutative distributive Field-like unital non trivial (non empty doubleLoopStr); existence proof take F_Real; thus thesis; end; end; canceled 2; theorem Th27: for L being add-associative right_zeroed right_complementable unital right-distributive (non empty doubleLoopStr) st 0.L = 1.L holds L is trivial proof let L be add-associative right_zeroed right_complementable unital right-distributive (non empty doubleLoopStr) such that A1: 0.L = 1.L; let u be Element of L; thus u = u*0.L by A1,GROUP_1:def 4 .= 0.L by VECTSP_1:36; end; theorem Th28: for L being add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a being Element of L, p being FinSequence of the carrier of L holds Sum (a*p) = a*Sum p proof let L be add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a be Element of L; set p = <*>(the carrier of L); A1: Sum p = 0.L by RLVECT_1:60; defpred P[FinSequence of the carrier of L] means Sum (a*$1) = a*Sum $1; Sum (a*p) = Sum p by Th19; then A2: P[p] by A1,VECTSP_1:36; A3: now let p be FinSequence of the carrier of L, r be Element of L such that A4: P[p]; Sum (a*(p^<*r*>)) = Sum ((a*p)^(a*<*r*>)) by Th23 .= Sum (a*p) + Sum (a*<*r*>) by RLVECT_1:58 .= Sum (a*p) + Sum (<*a*r*>) by Th21 .= Sum (a*p) + a*r by RLVECT_1:61 .= a*Sum p + a*Sum<*r*> by A4,RLVECT_1:61 .= a*(Sum p + Sum<*r*>) by VECTSP_1:def 18 .= a*Sum (p^<*r*>) by RLVECT_1:58; hence P[p^<*r*>]; end; thus for p being FinSequence of the carrier of L holds P[p] from IndSeqD(A2,A3); end; theorem Th29: for L being add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a being Element of L, p being FinSequence of the carrier of L holds Sum (p*a) = (Sum p)*a proof let L be add-associative right_zeroed right_complementable unital distributive (non empty doubleLoopStr), a be Element of L; set p = <*>(the carrier of L); A1: Sum p = 0.L by RLVECT_1:60; defpred P[FinSequence of the carrier of L] means Sum ($1*a) = (Sum $1)*a; Sum (p*a) = Sum p by Th20; then A2: P[p] by A1,VECTSP_1:39; A3: now let p be FinSequence of the carrier of L, r be Element of L such that A4: P[p]; Sum ((p^<*r*>)*a) = Sum ((p*a)^(<*r*>*a)) by Th24 .= Sum (p*a) + Sum (<*r*>*a) by RLVECT_1:58 .= Sum (p*a) + Sum (<*r*a*>) by Th22 .= Sum (p*a) + r*a by RLVECT_1:61 .= (Sum p)*a + (Sum<*r*>)*a by A4,RLVECT_1:61 .= (Sum p + Sum<*r*>)*a by VECTSP_1:def 18 .= (Sum (p^<*r*>))*a by RLVECT_1:58; hence P[p^<*r*>]; end; thus for p being FinSequence of the carrier of L holds P[p] from IndSeqD(A2,A3); end; begin :: Sequence flattening -------------------------------------------------- definition let D be set, F be empty FinSequence of D*; cluster FlattenSeq F -> empty; coherence proof F = <*>(D*); then FlattenSeq F = <*>D by SCMFSA_7:13; hence thesis; end; end; theorem Th30: for D being set, F being FinSequence of D* holds len FlattenSeq F = Sum Card F proof let D be set; defpred P[FinSequence of D*] means len FlattenSeq $1 = Sum Card $1; A1: P[<*>(D*)] by FINSEQ_1:25,RVSUM_1:102; A2: now let F be FinSequence of D*, p be Element of D* such that A3: P[F]; len FlattenSeq (F^<*p*>) = len (FlattenSeq F ^ FlattenSeq <*p*>) by SCMFSA_7:14 .= (Sum Card F) + len FlattenSeq <*p*> by A3,FINSEQ_1:35 .= (Sum Card F) + len p by DTCONSTR:13 .= Sum ((Card F)^<*len p*>) by RVSUM_1:104 .= Sum ((Card F) ^ Card <*p*>) by Th12 .= Sum Card (F^<*p*>) by Th13; hence P[F^<*p*>]; end; thus for F be FinSequence of D* holds P[F] from IndSeqD(A1,A2); end; theorem Th31: 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 proof let D, E be set, F be FinSequence of D*, G be FinSequence of E*; assume Card F = Card G; hence len FlattenSeq F = Sum Card G by Th30 .= len FlattenSeq G by Th30; end; theorem Th32: 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 proof let D be set; set F = <*>(D*); defpred P[FinSequence of D*] means for k being set st k in dom FlattenSeq $1 ex i,j be Nat st i in dom $1 & j in dom ($1.i) & k = (Sum Card ($1|(i-'1))) + j & ($1.i).j = (FlattenSeq $1).k; A1: P[F]; A2: for F be FinSequence of D*, p be Element of D* st P[F] holds P[F^<*p*>] proof let F be FinSequence of D*, p be Element of D*; assume A3: P[F]; let k be set; assume A4: k in dom FlattenSeq (F^<*p*>); then reconsider m = k as Nat; A5: FlattenSeq (F^<*p*>) = FlattenSeq F ^ FlattenSeq <*p*> by SCMFSA_7:14 .= FlattenSeq F ^ p by DTCONSTR:13; A6: Sum Card F = len FlattenSeq F by Th30; A7: (F^<*p*>)|len F = F by FINSEQ_5:26; per cases; suppose A8: not k in dom FlattenSeq F; take i = len F + 1; take j = m-'Sum Card ((F^<*p*>)|(i-'1)); A9: (Sum Card ((F^<*p*>)|(i-'1))) = len FlattenSeq F by A6,A7,BINARITH:39; 1 <= m by A4,FINSEQ_3:27; then A10: len FlattenSeq F < m by A8,FINSEQ_3:27; A11: len (F^<*p*>) = len F + len <*p*> by FINSEQ_1:35 .= len F +1 by FINSEQ_1:56; 1 in dom <*p*> by FINSEQ_5:6; then A12: (F^<*p*>).i = <*p*>.1 by FINSEQ_1:def 7 .= p by FINSEQ_1:57; 1 <= len F +1 by NAT_1:29; hence i in dom (F^<*p*>) by A11,FINSEQ_3:27; len FlattenSeq F +1 <= m by A10,NAT_1:38; then A13: 1 <= j by A9,SPRECT_3:8; m <= len (FlattenSeq F ^ p) by A4,A5,FINSEQ_3:27; then m <= len FlattenSeq F + len p by FINSEQ_1:35; then j <= len p by A9,SPRECT_3:6; hence A14: j in dom ((F^<*p*>).i) by A12,A13,FINSEQ_3:27; thus k = (Sum Card ((F^<*p*>)|(i-'1))) + j by A9,A10,AMI_5:4; hence ((F^<*p*>).i).j = (FlattenSeq (F^<*p*>)).k by A5,A9,A12,A14,FINSEQ_1:def 7; suppose A15: k in dom FlattenSeq F; then consider i, j being Nat such that A16: i in dom F and A17: j in dom (F.i) and A18: k = (Sum Card (F|(i-'1))) + j and A19: (F.i).j = (FlattenSeq F).k by A3; take i, j; dom F c= dom (F^<*p*>) by FINSEQ_1:39; hence i in dom (F^<*p*>) by A16; A20: (F^<*p*>).i = (F.i) by A16,FINSEQ_1:def 7; thus j in dom ((F^<*p*>).i) by A16,A17,FINSEQ_1:def 7; A21: i <= len F by A16,FINSEQ_3:27; i-'1 <= i by GOBOARD9:2; then i-'1 <= len F by A21,AXIOMS:22; hence k = (Sum Card ((F^<*p*>)|(i-'1))) + j by A18,FINSEQ_5:25; thus ((F^<*p*>).i).j = (FlattenSeq (F^<*p*>)).k by A5,A15,A19,A20,FINSEQ_1:def 7; end; thus for F being FinSequence of D* holds P[F] from IndSeqD(A1,A2); end; theorem Th33: for D being set, F being FinSequence of D*, i, j being 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) proof let D be set; set F = <*>(D*); defpred P[FinSequence of D*] means for i, j be Nat st i in dom $1 & j in dom ($1.i) holds (Sum Card ($1|(i-'1))) + j in dom FlattenSeq $1 & ($1.i).j = (FlattenSeq $1).((Sum Card ($1|(i-'1))) + j); A1: P[F]; A2: for F be FinSequence of D*, p be Element of D* st P[F] holds P[F^<*p*>] proof let F be FinSequence of D*, p be Element of D*; assume A3: for i, j being 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); let i, j be Nat; assume that A4: i in dom (F^<*p*>) and A5: j in dom ((F^<*p*>).i); A6: FlattenSeq (F^<*p*>) = FlattenSeq F ^ FlattenSeq <*p*> by SCMFSA_7:14 .= FlattenSeq F ^ p by DTCONSTR:13; per cases; suppose A7: not i in dom F; A8: len (F^<*p*>) = len F + len <*p*> by FINSEQ_1:35 .= len F + 1 by FINSEQ_1:57; A9: 1 <= i & i <= len (F^<*p*>) by A4,FINSEQ_3:27; then len F < i by A7,FINSEQ_3:27; then len F + 1 <= i by NAT_1:38; then A10: i = len F + 1 by A8,A9,AXIOMS:21; then A11: i-'1 = len F by BINARITH:39; 1 in dom <*p*> by FINSEQ_5:6; then A12: (F^<*p*>).i = <*p*>.1 by A10,FINSEQ_1:def 7 .= p by FINSEQ_1:57; A13: (F^<*p*>)|(i-'1) = F by A11,FINSEQ_5:26; A14: Sum Card F = len FlattenSeq F by Th30; hence (Sum Card ((F^<*p*>)|(i-'1))) + j in dom FlattenSeq (F^<*p*>) by A5,A6,A12,A13,FINSEQ_1:41; thus ((F^<*p*>).i).j = (FlattenSeq (F^<*p*>)).((Sum Card ((F^<*p*>)|(i-'1)))+j) by A5,A6,A12,A13,A14,FINSEQ_1:def 7; suppose A15: i in dom F; then A16: i <= len F by FINSEQ_3:27; i-'1 <= i by GOBOARD9:2; then i-'1 <= len F by A16,AXIOMS:22; then A17: (F^<*p*>)|(i-'1) = F|(i-'1) by FINSEQ_5:25; A18: dom FlattenSeq F c= dom FlattenSeq (F^<*p*>) by A6,FINSEQ_1:39; A19: j in dom (F.i) by A5,A15,FINSEQ_1:def 7; then A20: (Sum Card (F|(i-'1))) + j in dom FlattenSeq F by A3,A15; hence (Sum Card ((F^<*p*>)|(i-'1))) + j in dom FlattenSeq (F^<*p*>) by A17,A18; thus ((F^<*p*>).i).j = (F.i).j by A15,FINSEQ_1:def 7 .= (FlattenSeq F).((Sum Card (F|(i-'1))) + j) by A3,A15,A19 .= (FlattenSeq (F^<*p*>)).((Sum Card ((F^<*p*>)|(i-'1)))+j) by A6,A17,A20,FINSEQ_1:def 7; end; thus for F being FinSequence of D* holds P[F] from IndSeqD(A1,A2); end; theorem Th34: for L being add-associative right_zeroed right_complementable (non empty LoopStr), F being FinSequence of (the carrier of L)* holds Sum FlattenSeq F = Sum Sum F proof let L be add-associative right_zeroed right_complementable (non empty LoopStr); defpred P[FinSequence of (the carrier of L)*] means Sum FlattenSeq $1 = Sum Sum $1; Sum FlattenSeq(<*>((the carrier of L)*)) = Sum <*>(the carrier of L); then A1: P[<*>((the carrier of L)*)] by Th16; A2: for f being FinSequence of (the carrier of L)*, p being Element of (the carrier of L)* st P[f] holds P[f^<*p*>] proof let f be FinSequence of (the carrier of L)*, p be Element of (the carrier of L)* such that A3: Sum FlattenSeq f = Sum Sum f; thus Sum FlattenSeq(f^<*p*>) = Sum((FlattenSeq f)^FlattenSeq <*p*>) by SCMFSA_7:14 .= Sum((FlattenSeq f)^p) by DTCONSTR:13 .= Sum Sum f +Sum p by A3,RLVECT_1:58 .= Sum Sum f+Sum<*Sum p*> by RLVECT_1:61 .= Sum(Sum f^<*Sum p*>) by RLVECT_1:58 .= Sum(Sum f^Sum<*p*>) by Th17 .= Sum Sum(f^<*p*>) by Th18; end; thus for f be FinSequence of (the carrier of L)* holds P[f] from IndSeqD(A1,A2); end; theorem Th35: 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* proof let X, Y be non empty set, f be FinSequence of X*, v be Function of X, Y; set F = (dom f --> v)**f; A1: dom F = dom (dom f --> v) /\ dom f by MSUALG_3:def 4 .= dom f /\ dom f by FUNCOP_1:19 .= dom f; then dom F = Seg len f by FINSEQ_1:def 3; then A2: F is FinSequence-like by FINSEQ_1:def 2; rng F c= Y* proof let y be set; assume y in rng F; then consider x being set such that A3: x in dom F & y = F.x by FUNCT_1:def 5; A4: y = (dom f --> v).x * (f.x) by A3,MSUALG_3:def 4 .= v*(f.x) by A1,A3,FUNCOP_1:13; f.x in X* by A1,A3,FINSEQ_2:13; then f.x is FinSequence of X by FINSEQ_1:def 11; then y is FinSequence of Y by A4,FINSEQ_2:36; hence y in Y* by FINSEQ_1:def 11; end; hence (dom f --> v)**f is FinSequence of Y* by A2,FINSEQ_1:def 4; end; theorem Th36: 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 proof let X, Y be non empty set, f be FinSequence of X*, v be Function of X, Y; reconsider F = (dom f --> v)**f as FinSequence of Y* by Th35; take F; thus F = (dom f --> v)**f; set Fl = FlattenSeq F; set fl = FlattenSeq f; reconsider vfl = v*fl as FinSequence of Y by FINSEQ_2:36; now len fl = len vfl by FINSEQ_2:37; hence A1: dom fl = dom vfl by FINSEQ_3:31; A2: dom f = dom Card f by CARD_3:def 2; A3: dom F = dom (dom f --> v) /\ dom f by MSUALG_3:def 4 .= dom f /\ dom f by FUNCOP_1:19 .= dom f; then A4: dom f = dom Card F by CARD_3:def 2; now let k be set; assume A5: k in dom f; then A6: F.k = ((dom f --> v).k)*(f.k) by A3,MSUALG_3:def 4 .= v*(f.k) by A5,FUNCOP_1:13; f.k in X* by A5,FINSEQ_2:13; then reconsider fk = f.k as FinSequence of X by FINSEQ_1:def 11; thus (Card f).k = len fk by A5,CARD_3:def 2 .= len (F.k) by A6,FINSEQ_2:37 .= (Card F).k by A3,A5,CARD_3:def 2; end; then A7: Card f = Card F by A2,A4,FUNCT_1:9; then len fl = len Fl by Th31; hence dom fl = dom Fl by FINSEQ_3:31; let k be Nat; assume A8: k in dom fl; then consider i, j being Nat such that A9: i in dom f and A10: j in dom (f.i) and A11: k = (Sum Card (f|(i-'1))) + j and A12: (f.i).j = fl.k by Th32; A13: dom v = X by FUNCT_2:def 1; f.i in X* by A9,FINSEQ_2:13; then f.i is FinSequence of X by FINSEQ_1:def 11; then rng (f.i) c= dom v by A13,FINSEQ_1:def 4; then A14: j in dom (v*(f.i)) by A10,RELAT_1:46; A15: F.i = ((dom f --> v).i)*(f.i) by A3,A9,MSUALG_3:def 4 .= v*(f.i) by A9,FUNCOP_1:13; f.i in X* by A9,FINSEQ_2:13; then reconsider fi = f.i as FinSequence of X by FINSEQ_1:def 11; len fi = len (F.i) by A15,FINSEQ_2:37; then A16: j in dom (F.i) by A10,FINSEQ_3:31; Card (F|(i-'1)) = Card (F|Seg (i-'1)) by TOPREAL1:def 1 .= (Card f)|Seg (i-'1) by A7,Th11 .= Card (f|Seg(i-'1)) by Th11 .= Card (f|(i-'1)) by TOPREAL1:def 1; then Fl.k = (F.i).j by A3,A9,A11,A16,Th33 .= (((dom f --> v).i)*(f.i)).j by A3,A9,MSUALG_3:def 4 .= (v*(f.i)).j by A9,FUNCOP_1:13 .= v.((f.i).j) by A14,FUNCT_1:22; hence vfl.k = Fl.k by A1,A8,A12,FUNCT_1:22; end; hence v*FlattenSeq f = FlattenSeq F by FINSEQ_1:17; end; begin :: Functions yielding natural numbers ----------------------------------- definition cluster {} -> natural-yielding; coherence proof thus rng {} c= NAT by XBOOLE_1:2; end; end; definition cluster natural-yielding Function; existence proof take {}; thus thesis; end; end; definition let f be natural-yielding Function; let x be set; redefine func f.x -> Nat; coherence proof per cases; suppose x in dom f; then f.x in rng f & rng f c= NAT by FUNCT_1:def 5,SEQM_3:def 8; hence thesis; suppose not x in dom f; hence thesis by CARD_1:51,FUNCT_1:def 4; end; end; definition let f be natural-yielding Function, x be set, n be Nat; cluster f+*(x,n) -> natural-yielding; coherence proof set F = f+*(x,n); let y be set; assume y in rng F; then consider a being set such that A1: a in dom F & y = F.a by FUNCT_1:def 5; per cases; suppose x in dom f & x = a; then F.a = n by FUNCT_7:33; hence y in NAT by A1; suppose x in dom f & x <> a; then F.a = f.a by FUNCT_7:34; hence y in NAT by A1; suppose not x in dom f; then F.a = f.a by FUNCT_7:def 3; hence y in NAT by A1; end; end; definition let X be set; cluster -> natural-yielding Function of X, NAT; coherence proof let f be Function of X, NAT; rng f c= NAT by RELSET_1:12; hence thesis by SEQM_3:def 8; end; end; definition let X be set; cluster natural-yielding ManySortedSet of X; existence proof set f = X --> 0; dom f = X by FUNCOP_1:19; then reconsider f as ManySortedSet of X by PBOOLE:def 3; take f; A1: rng f c= {0} by FUNCOP_1:19; {0} c= NAT by ZFMISC_1:37; then rng f c= NAT by A1,XBOOLE_1:1; hence f is natural-yielding by SEQM_3:def 8; end; end; definition let X be set, b1, b2 be natural-yielding ManySortedSet of X; canceled; func b1+b2 -> ManySortedSet of X means :Def5: for x being set holds it.x = b1.x+b2.x; existence proof deffunc F(set) = b1.$1+b2.$1; consider f being ManySortedSet of X such that A1: for i being set st i in X holds f.i = F(i) from MSSLambda; take f; let x be set; per cases; suppose x in X; hence thesis by A1; suppose A2: not x in X; A3: dom f = X by PBOOLE:def 3; A4: dom b1 = X by PBOOLE:def 3; A5: dom b2 = X by PBOOLE:def 3; thus f.x = 0+0 by A2,A3,FUNCT_1:def 4 .= 0+b2.x by A2,A5,FUNCT_1:def 4 .= b1.x+b2.x by A2,A4,FUNCT_1:def 4; end; uniqueness proof let it1, it2 be ManySortedSet of X such that A6: for x being set holds it1.x = b1.x+b2.x and A7: for x being set holds it2.x = b1.x+b2.x; A8: dom it1 = X by PBOOLE:def 3; A9: dom it2 = X by PBOOLE:def 3; now let x be set; assume x in X; thus it1.x = b1.x+b2.x by A6 .= it2.x by A7; end; hence it1 = it2 by A8,A9,FUNCT_1:9; end; commutativity; func b1 -' b2 -> ManySortedSet of X means :Def6: for x being set holds it.x = b1.x -' b2.x; existence proof deffunc F(set) = b1.$1 -' b2.$1; consider f being ManySortedSet of X such that A10: for i being set st i in X holds f.i = F(i) from MSSLambda; take f; let x be set; per cases; suppose x in X; hence thesis by A10; suppose A11: not x in X; A12: dom f = X by PBOOLE:def 3; A13: dom b1 = X by PBOOLE:def 3; A14: dom b2 = X by PBOOLE:def 3; thus f.x = 0 by A11,A12,FUNCT_1:def 4 .= 0-'0 by GOBOARD9:1 .= 0-'b2.x by A11,A14,FUNCT_1:def 4 .= b1.x-'b2.x by A11,A13,FUNCT_1:def 4; end; uniqueness proof let it1, it2 be ManySortedSet of X such that A15: for x being set holds it1.x = b1.x-'b2.x and A16: for x being set holds it2.x = b1.x-'b2.x; now let x be set; assume x in X; thus it1.x = b1.x-'b2.x by A15 .= it2.x by A16; end; hence it1 = it2 by PBOOLE:3; end; end; theorem for X being set, b, b1, b2 being natural-yielding ManySortedSet of X st for x being set st x in X holds b.x = b1.x+b2.x holds b = b1+b2 proof let X be set, b, b1, b2 be natural-yielding ManySortedSet of X; assume A1: for x being set st x in X holds b.x = b1.x+b2.x; now let x be set; per cases; suppose x in X; hence b.x = b1.x+b2.x by A1; suppose A2: not x in X; A3: dom b = X by PBOOLE:def 3; A4: dom b1 = X by PBOOLE:def 3; A5: dom b2 = X by PBOOLE:def 3; thus b.x = 0+0 by A2,A3,FUNCT_1:def 4 .= 0+b2.x by A2,A5,FUNCT_1:def 4 .= b1.x+b2.x by A2,A4,FUNCT_1:def 4; end; hence b = b1+b2 by Def5; end; theorem Th38: for X being set, b, b1, b2 being natural-yielding ManySortedSet of X st for x being set st x in X holds b.x = b1.x-'b2.x holds b = b1-'b2 proof let X be set, b, b1, b2 be natural-yielding ManySortedSet of X; assume A1: for x being set st x in X holds b.x = b1.x-'b2.x; now let x be set; per cases; suppose x in X; hence b.x = b1.x -' b2.x by A1; suppose A2: not x in X; A3: dom b = X by PBOOLE:def 3; A4: dom b1 = X by PBOOLE:def 3; A5: dom b2 = X by PBOOLE:def 3; thus b.x = 0 by A2,A3,FUNCT_1:def 4 .= 0-'0 by GOBOARD9:1 .= 0-'b2.x by A2,A5,FUNCT_1:def 4 .= b1.x-'b2.x by A2,A4,FUNCT_1:def 4; end; hence b = b1-'b2 by Def6; end; definition let X be set, b1, b2 be natural-yielding ManySortedSet of X; cluster b1+b2 -> natural-yielding; coherence proof set f = b1+b2; rng f c= NAT proof let y be set; assume y in rng f; then consider x being set such that A1: x in dom f & y = f.x by FUNCT_1:def 5; f.x = b1.x+b2.x by Def5; hence y in NAT by A1; end; hence f is natural-yielding by SEQM_3:def 8; end; cluster b1-'b2 -> natural-yielding; coherence proof set f = b1 -' b2; rng f c= NAT proof let y be set; assume y in rng f; then consider x being set such that A2: x in dom f & y = f.x by FUNCT_1:def 5; f.x = b1.x -' b2.x by Def6; hence y in NAT by A2; end; hence f is natural-yielding by SEQM_3:def 8; end; end; theorem Th39: for X being set, b1, b2, b3 being natural-yielding ManySortedSet of X holds (b1+b2)+b3 = b1+(b2+b3) proof let X be set, b1, b2, b3 be natural-yielding ManySortedSet of X; now let x be set; assume x in X; thus ((b1+b2)+b3).x = (b1+b2).x+b3.x by Def5 .= b1.x+b2.x+b3.x by Def5 .= b1.x+(b2.x+b3.x) by XCMPLX_1:1 .= b1.x+(b2+b3).x by Def5 .= (b1+(b2+b3)).x by Def5; end; hence (b1+b2)+b3 = b1+(b2+b3) by PBOOLE:3; end; theorem for X being set, b, c, d being natural-yielding ManySortedSet of X holds b-'c-'d = b-'(c+d) proof let X be set, b, c, d be natural-yielding ManySortedSet of X; now let x be set; assume x in X; thus (b-'c-'d).x = (b-'c).x -' d.x by Def6 .= b.x-'c.x-'d.x by Def6 .= b.x-'(c.x+d.x) by Th3 .= b.x-'(c+d).x by Def5; end; hence b-'c-'d = b-'(c+d) by Th38; end; begin :: The support of a function -------------------------------------------- definition let f be Function; func support f means :Def7: for x being set holds x in it iff f.x <> 0; existence proof defpred P[set] means f.$1 <> 0; consider A being set such that A1: for x being set holds x in A iff x in dom f & P[x] from Separation; take A; let x be set; thus x in A implies f.x <> 0 by A1; assume A2: f.x <> 0; then x in dom f by FUNCT_1:def 4; hence thesis by A1,A2; end; uniqueness proof let A,B be set such that A3: for x being set holds x in A iff f.x <> 0 and A4: for x being set holds x in B iff f.x <> 0; for x being set holds x in A iff x in B proof let x be set; x in A iff f.x <> 0 by A3; hence thesis by A4; end; hence thesis by TARSKI:2; end; end; theorem Th41: for f being Function holds support f c= dom f proof let f be Function, x be set; assume x in support f; then f.x <> 0 by Def7; hence x in dom f by FUNCT_1:def 4; end; definition let f be Function; attr f is finite-support means :Def8: support f is finite; synonym f has_finite-support; end; definition cluster {} -> finite-support; coherence proof dom {} = {}; then support {} c= {} by Th41; hence support {} is finite by FINSET_1:13; end; end; definition cluster finite -> finite-support Function; coherence proof let f be Function; assume f is finite; then A1: dom f is finite by AMI_1:21; support f c= dom f by Th41; hence support f is finite by A1,FINSET_1:13; end; end; definition cluster natural-yielding finite-support non empty Function; existence proof take f = 0 .--> 1; rng f = {1} by CQC_LANG:5; then rng f c= NAT by ZFMISC_1:37; hence f is natural-yielding by SEQM_3:def 8; dom f = {0} by CQC_LANG:5; then support f c= {0} by Th41; then support f is finite by FINSET_1:13; hence f is finite-support by Def8; f = {[0,1]} by AMI_1:19; hence f is non empty; end; end; definition let f be finite-support Function; cluster support f -> finite; coherence by Def8; end; definition let X be set; cluster finite-support Function of X, NAT; existence proof set f = X --> 0; A1: dom f = X by FUNCOP_1:19; A2: {0} c= NAT by ZFMISC_1:37; rng f c= {0} by FUNCOP_1:19; then rng f c= NAT by A2,XBOOLE_1:1; then reconsider f as Function of X, NAT by A1,FUNCT_2:def 1,RELSET_1:11; take f; now assume support f <> {}; then consider x being set such that A3: x in support f by XBOOLE_0:def 1; A4: f.x <> 0 by A3,Def7; support f c= dom f by Th41; hence contradiction by A1,A3,A4,FUNCOP_1:13; end; hence support f is finite; end; end; definition let f be finite-support Function, x, y be set; cluster f+*(x,y) -> finite-support; coherence proof set F = f+*(x,y); support F c= support f \/ {x} proof let a be set; assume a in support F; then A1: F.a <> 0 by Def7; per cases; suppose x in dom f & a = x; then a in {x} by TARSKI:def 1; hence a in support f \/ {x} by XBOOLE_0:def 2; suppose x in dom f & a <> x; then F.a = f.a by FUNCT_7:34; then a in support f by A1,Def7; hence a in support f \/ {x} by XBOOLE_0:def 2; suppose not x in dom f; then F.a = f.a by FUNCT_7:def 3; then a in support f by A1,Def7; hence a in support f \/ {x} by XBOOLE_0:def 2; end; hence support (f+*(x,y)) is finite by FINSET_1:13; end; end; definition let X be set; cluster natural-yielding finite-support ManySortedSet of X; existence proof set f = X --> 0; A1: dom f = X by FUNCOP_1:19; then reconsider f as ManySortedSet of X by PBOOLE:def 3; take f; A2: rng f c= {0} by FUNCOP_1:19; {0} c= NAT by ZFMISC_1:37; then rng f c= NAT by A2,XBOOLE_1:1; hence f is natural-yielding by SEQM_3:def 8; support f = {} proof assume not thesis; then consider x being set such that A3: x in support f by XBOOLE_0:def 1; support f c= dom f by Th41; then f.x = 0 by A1,A3,FUNCOP_1:13; hence contradiction by A3,Def7; end; hence f is finite-support by Def8; end; end; theorem Th42: for X being set, b1, b2 being natural-yielding ManySortedSet of X holds support (b1+b2) = support b1 \/ support b2 proof let X be set, b1, b2 be natural-yielding ManySortedSet of X; now let x be set; hereby assume x in support b1 \/ support b2; then x in support b1 or x in support b2 by XBOOLE_0:def 2; then b1.x <> 0 or b2.x <> 0 by Def7; then b1.x + b2.x <> 0 by NAT_1:23; hence (b1+b2).x <> 0 by Def5; end; assume A1: (b1+b2).x <> 0; assume not x in support b1 \/ support b2; then not x in support b1 & not x in support b2 by XBOOLE_0:def 2; then b1.x = 0 & b2.x = 0 by Def7; then b1.x+b2.x = 0; hence contradiction by A1,Def5; end; hence support (b1+b2) = support b1 \/ support b2 by Def7; end; theorem Th43: for X being set, b1, b2 being natural-yielding ManySortedSet of X holds support (b1-'b2) c= support b1 proof let X be set, b1, b2 be natural-yielding ManySortedSet of X; thus support (b1-'b2) c= support b1 proof let x be set; assume A1: x in support (b1-'b2); assume not x in support b1; then A2: b1.x = 0 by Def7; 0 <= b2.x by NAT_1:18; then b1.x-'b2.x = 0 by A2,NAT_2:10; then (b1-'b2).x = 0 by Def6; hence contradiction by A1,Def7; end; end; definition let X be non empty set, S be ZeroStr, f be Function of X, S; func Support f -> Subset of X means :Def9: for x being Element of X holds x in it iff f.x <> 0.S; existence proof defpred P[set] means f.$1 <> 0.S; consider B being Subset of X such that A1: for x being Element of X holds x in B iff P[x] from SubsetEx; take B; thus thesis by A1; end; uniqueness proof let A,B be Subset of X such that A2: for x being Element of X holds x in A iff f.x <> 0.S and A3: for x being Element of X holds x in B iff f.x <> 0.S; now let x be Element of X; x in A iff f.x <> 0.S by A2; hence x in A iff x in B by A3; end; hence A = B by SUBSET_1:8; end; end; definition let X be non empty set, S be ZeroStr, p be Function of X, S; attr p is finite-Support means :Def10: Support p is finite; synonym p has_finite-Support; end; begin :: Bags ----------------------------------------------------------------- definition let X be set; mode bag of X is natural-yielding finite-support ManySortedSet of X; end; definition let X be finite set; cluster -> finite-support ManySortedSet of X; coherence proof let f be ManySortedSet of X; support f c= dom f & dom f = X by Th41,PBOOLE:def 3; hence support f is finite by FINSET_1:13; end; end; definition let X be set, b1, b2 be bag of X; cluster b1+b2 -> finite-support; coherence proof support (b1+b2) = support b1 \/ support b2 by Th42; hence support (b1+b2) is finite; end; cluster b1-'b2 -> finite-support; coherence proof support (b1-'b2) c= support b1 by Th43; hence support (b1-'b2) is finite by FINSET_1:13; end; end; theorem Th44: for X being set holds X--> 0 is bag of X proof let X be set; set f = X --> 0; A1: dom f = X by FUNCOP_1:19; A2: rng f c= {0} by FUNCOP_1:19; {0} c= NAT by ZFMISC_1:37; then A3: rng f c= NAT by A2,XBOOLE_1:1; support f = {} proof assume not thesis; then consider x being set such that A4: x in support f by XBOOLE_0:def 1; support f c= dom f by Th41; then f.x = 0 by A1,A4,FUNCOP_1:13; hence contradiction by A4,Def7; end; hence X --> 0 is bag of X by A1,A3,Def8,PBOOLE:def 3,SEQM_3:def 8; end; definition let n be Ordinal, p, q be bag of n; pred p < q means :Def11: ex k being Ordinal st p.k < q.k & for l being Ordinal st l in k holds p.l = q.l; asymmetry proof let p, q be bag of n; given k being Ordinal such that A1: p.k < q.k and A2: for l being Ordinal st l in k holds p.l = q.l; given k1 being Ordinal such that A3: q.k1 < p.k1 and A4: for l being Ordinal st l in k1 holds q.l = p.l; per cases by ORDINAL1:24; suppose k in k1; hence contradiction by A1,A4; suppose k1 in k; hence contradiction by A2,A3; suppose k1 = k; hence contradiction by A1,A3; end; end; theorem Th45: for n being Ordinal, p, q, r being bag of n st p < q & q < r holds p < r proof let n be Ordinal, p, q, r be bag of n; assume A1: p < q & q < r; then consider k being Ordinal such that A2: p.k < q.k and A3: for l being Ordinal st l in k holds p.l = q.l by Def11; consider m being Ordinal such that A4: q.m < r.m and A5: for l being Ordinal st l in m holds q.l = r.l by A1,Def11; take n = k /\ m; A6: n c= k & n c= m by XBOOLE_1:17; A7: (n c= k & n <> k iff n c< k) & (n c= m & n <> m iff n c< m) by XBOOLE_0:def 8; now per cases by ORDINAL1:24; suppose k in m; hence p.n < r.n by A2,A5,A7,ORDINAL1:21,ORDINAL3:16,XBOOLE_1:17; suppose m in k; hence p.n < r.n by A3,A4,A7,ORDINAL1:21,ORDINAL3:16,XBOOLE_1:17; suppose m = k; hence p.n < r.n by A2,A4,AXIOMS:22; end; hence p.n < r.n; let l be Ordinal; assume A8: l in n; hence p.l = q.l by A3,A6 .= r.l by A5,A6,A8; end; definition let n be Ordinal, p, q be bag of n; pred p <=' q means :Def12: p < q or p = q; reflexivity; end; theorem Th46: for n being Ordinal, p, q, r being bag of n st p <=' q & q <=' r holds p <=' r proof let n be Ordinal, p, q, r be bag of n; assume p <=' q & q <=' r; then (p < q or p = q) & (q < r or q = r) by Def12; then p < r or p <=' r by Th45; hence p <=' r by Def12; end; theorem for n being Ordinal, p, q, r being bag of n st p < q & q <=' r holds p < r proof let n be Ordinal, p, q, r be bag of n such that A1: p < q and A2: q <=' r; q < r or q = r by A2,Def12; hence p < r by A1,Th45; end; theorem for n being Ordinal, p, q, r being bag of n st p <=' q & q < r holds p < r proof let n be Ordinal, p, q, r be bag of n such that A1: p <=' q and A2: q < r; p < q or p = q by A1,Def12; hence p < r by A2,Th45; end; theorem Th49: for n being Ordinal, p, q being bag of n holds p <=' q or q <=' p proof let n be Ordinal, p, q be bag of n; assume A1: not p <=' q; then A2: not p < q & not p = q by Def12; consider i being set such that A3: i in n and A4: p.i <> q.i by A1,PBOOLE:3; reconsider j = i as Ordinal by A3,ORDINAL1:23; defpred P[set] means p.$1 <> q.$1; j in n by A3; then A5: ex i being Ordinal st P[i] by A4; consider m being Ordinal such that A6: P[m] and A7: for n being Ordinal st P[n] holds m c= n from Ordinal_Min(A5); per cases by A6,AXIOMS:21; suppose A8: p.m < q.m; now let l be Ordinal; assume l in m; then not m c= l by ORDINAL1:7; hence q.l = p.l by A7; end; hence q <=' p by A2,A8,Def11; suppose A9: p.m > q.m; now let l be Ordinal; assume l in m; then not m c= l by ORDINAL1:7; hence p.l = q.l by A7; end; then q < p by A9,Def11; hence q <=' p by Def12; end; definition let X be set, d, b be bag of X; pred d divides b means :Def13: for k being set holds d.k <= b.k; reflexivity; end; theorem Th50: for n being set, d, b being bag of n st for k being set st k in n holds d.k <= b.k holds d divides b proof let n be set, d, b be bag of n; assume A1: for k being set st k in n holds d.k <= b.k; let k be set; per cases; suppose k in dom d; then k in n by PBOOLE:def 3; hence thesis by A1; suppose not k in dom d; then d.k = 0 by FUNCT_1:def 4; hence thesis by NAT_1:18; end; theorem Th51: for n being Ordinal, b1, b2 being bag of n st b1 divides b2 holds b2 -' b1 + b1 = b2 proof let n be Ordinal, b1, b2 be bag of n such that A1: b1 divides b2; now let k be set; assume k in n; then reconsider k' = k as Ordinal by ORDINAL1:23; A2: b1.k' <= b2.k' by A1,Def13; thus (b2 -' b1 + b1).k = (b2-'b1).k + b1.k by Def5 .= b2.k -' b1.k + b1.k by Def6 .= b2.k + b1.k -' b1.k by A2,JORDAN4:3 .= b2.k by BINARITH:39; end; hence b2 -' b1 + b1 = b2 by PBOOLE:3; end; theorem Th52: for X being set, b1, b2 being bag of X holds b2 + b1 -' b1 = b2 proof let X be set, b1, b2 be bag of X; now let k be set; assume k in X; thus (b2 + b1 -' b1).k = (b2+b1).k -' b1.k by Def6 .= b2.k+b1.k -' b1.k by Def5 .= b2.k by BINARITH:39; end; hence b2 + b1 -' b1 = b2 by PBOOLE:3; end; theorem Th53: for n being Ordinal, d, b being bag of n st d divides b holds d <=' b proof let n be Ordinal, d, b be bag of n; assume that A1: d divides b and A2: not (d < b); now let p be set; assume p in n; then reconsider p' = p as Ordinal by ORDINAL1:23; A3: d.p' <= b.p' by A1,Def13; defpred P[set] means d.$1 < b.$1; assume d.p <> b.p; then d.p' < b.p' by A3,AXIOMS:21; then A4: ex p being Ordinal st P[p]; consider k being Ordinal such that A5: P[k] and A6: for m being Ordinal st P[m] holds k c= m from Ordinal_Min(A4); now let l be Ordinal; assume l in k; then not k c= l by ORDINAL1:7; then A7: b.l <= d.l by A6; d.l <= b.l by A1,Def13; hence d.l = b.l by A7,AXIOMS:21; end; hence contradiction by A2,A5,Def11; end; hence d = b by PBOOLE:3; end; theorem Th54: for n being set, b,b1,b2 being bag of n st b = b1 + b2 holds b1 divides b proof let n be set, b,b1,b2 be bag of n; assume A1: b = b1 + b2; now let k be set; assume k in n; b.k = b1.k+b2.k by A1,Def5; hence b1.k <= b.k by NAT_1:29; end; hence b1 divides b by Th50; end; definition let X be set; func Bags X means :Def14: for x being set holds x in it iff x is bag of X; existence proof defpred P[set] means $1 is bag of X; consider A being set such that A1: for x being set holds x in A iff x in Funcs(X,NAT) & P[x] from Separation; take A; let x be set; thus x in A implies x is bag of X by A1; assume A2: x is bag of X; then reconsider b = x as bag of X; dom b = X & rng b c= NAT by PBOOLE:def 3,SEQM_3:def 8; then x in Funcs(X,NAT) by FUNCT_2:def 2; hence x in A by A1,A2; end; uniqueness proof let A,B be set such that A3: for x being set holds x in A iff x is bag of X and A4: for x being set holds x in B iff x is bag of X; now let x be set; x in A iff x is bag of X by A3; hence x in A iff x in B by A4; end; hence thesis by TARSKI:2; end; end; definition let X be set; redefine func Bags X -> Subset of Bags X; coherence proof Bags X c= Bags X; hence thesis; end; end; theorem Bags {} = {{}} proof now let x be set; hereby assume x in {{}}; then x = {} by TARSKI:def 1; hence x is bag of {} by PBOOLE:def 3,RELAT_1:60; end; assume x is bag of {}; then reconsider x' = x as ManySortedSet of {}; dom x' = {} by PBOOLE:def 3; then x' = {} by RELAT_1:64; hence x in {{}} by TARSKI:def 1; end; hence Bags {} = {{}} by Def14; end; definition let X be set; cluster Bags X -> non empty; coherence proof X --> 0 is bag of X by Th44; hence thesis by Def14; end; end; definition let X be set, B be non empty Subset of Bags X; redefine mode Element of B -> bag of X; coherence proof let b be Element of B; thus thesis by Def14; end; end; definition let n be set, L be non empty 1-sorted, p be Function of Bags n, L, x be bag of n; redefine func p.x -> Element of L; coherence proof reconsider f = p as Function of Bags n, the carrier of L; reconsider b = x as Element of Bags n by Def14; f.b is Element of L; hence p.x is Element of L; end; end; definition let X be set; func EmptyBag X -> Element of Bags X equals :Def15: X --> 0; coherence proof X --> 0 is bag of X by Th44; hence X --> 0 is Element of Bags X by Def14; end; end; theorem Th56: for X, x being set holds (EmptyBag X).x = 0 proof let X, x be set; A1: EmptyBag X = X --> 0 by Def15; A2: dom (X --> 0) = X by FUNCOP_1:19; per cases; suppose x in X; hence (EmptyBag X).x = 0 by A1,FUNCOP_1:13; suppose not x in X; hence (EmptyBag X).x = 0 by A1,A2,FUNCT_1:def 4; end; theorem for X be set, b being bag of X holds b+EmptyBag X = b proof let X be set, b be bag of X; now let x be set; assume A1: x in X; A2: (EmptyBag X).x = (X --> 0).x by Def15 .= 0 by A1,FUNCOP_1:13; thus (b+EmptyBag X).x = b.x+(EmptyBag X).x by Def5 .= b.x by A2; end; hence b+EmptyBag X = b by PBOOLE:3; end; theorem Th58: for X be set, b being bag of X holds b-'EmptyBag X = b proof let X be set, b be bag of X; now let x be set; assume A1: x in X; A2: (EmptyBag X).x = (X --> 0).x by Def15 .= 0 by A1,FUNCOP_1:13; thus (b-'EmptyBag X).x = b.x-'(EmptyBag X).x by Def6 .= b.x by A2,JORDAN3:2; end; hence b-'EmptyBag X = b by PBOOLE:3; end; theorem for X be set, b being bag of X holds (EmptyBag X) -' b = EmptyBag X proof let X be set, b be bag of X; now let x be set; assume A1: x in X; A2: (EmptyBag X).x = (X --> 0).x by Def15 .= 0 by A1,FUNCOP_1:13; A3: 0 <= b.x by NAT_1:18; thus ((EmptyBag X)-'b).x = (EmptyBag X).x-'b.x by Def6 .= (EmptyBag X).x by A2,A3,NAT_2:10; end; hence (EmptyBag X) -' b = EmptyBag X by PBOOLE:3; end; theorem Th60: for X being set, b being bag of X holds b-'b = EmptyBag X proof let X be set, b be bag of X; now let x be set; assume x in X; thus (b-'b).x = b.x -' b.x by Def6 .= 0 by GOBOARD9:1 .= (EmptyBag X).x by Th56; end; hence b-'b = EmptyBag X by PBOOLE:3; end; theorem Th61: for n being set, b1, b2 be bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds b2 = b1 proof let n be set, b1, b2 be bag of n such that A1: b1 divides b2 and A2: b2 -' b1 = EmptyBag n; now let k be set; assume k in n; A3: b1.k <= b2.k by A1,Def13; 0 = (b2-'b1).k by A2,Th56 .= b2.k -' b1.k by Def6; then b2.k <= b1.k by JORDAN4:1; hence b2.k = b1.k by A3,AXIOMS:21; end; hence b2 = b1 by PBOOLE:3; end; theorem Th62: for n being set, b being bag of n st b divides EmptyBag n holds EmptyBag n = b proof let n be set, b be bag of n; assume A1: b divides EmptyBag n; now let k be set; assume k in n; A2: (EmptyBag n).k = 0 by Th56; then b.k <= 0 by A1,Def13; hence (EmptyBag n).k = b.k by A2,NAT_1:18; end; hence EmptyBag n = b by PBOOLE:3; end; theorem Th63: for n being set, b being bag of n holds EmptyBag n divides b proof let n be set, b be bag of n; let k be set; (EmptyBag n).k = 0 by Th56; hence (EmptyBag n).k <= b.k by NAT_1:18; end; theorem Th64: for n being Ordinal, b being bag of n holds EmptyBag n <=' b proof let n be Ordinal, b be bag of n; EmptyBag n divides b by Th63; hence EmptyBag n <=' b by Th53; end; definition let n be Ordinal; func BagOrder n -> Order of Bags n means :Def16: for p, q being bag of n holds [p, q] in it iff p <=' q; existence proof defpred P[set,set] means ex b1,b2 be Element of Bags n st $1 = b1 & $2 = b2 & b1 <=' b2; consider BO being Relation of Bags n, Bags n such that A1: for x, y being set holds [x,y] in BO iff x in Bags n & y in Bags n & P[x,y] from Rel_On_Set_Ex; A2: BO is_reflexive_in Bags n proof let x be set; assume x in Bags n; hence thesis by A1; end; A3: BO is_antisymmetric_in Bags n proof let x, y be set; assume A4: x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO; then consider b1, b2 being Element of Bags n such that A5: x = b1 & y = b2 & b1 <=' b2 by A1; consider b1', b2' being Element of Bags n such that A6: y = b1' & x = b2' & b1' <=' b2' by A1,A4; (b1 < b2 or b1 = b2) & (b1' < b2' or b1' = b2') by A5,A6,Def12; hence x = y by A5,A6; end; A7: BO is_transitive_in Bags n proof let x, y, z be set such that x in Bags n & y in Bags n & z in Bags n and A8: [x,y] in BO & [y,z] in BO; consider b1, b2 being Element of Bags n such that A9: x = b1 & y = b2 & b1 <=' b2 by A1,A8; consider b1', b2' being Element of Bags n such that A10: y = b1' & z = b2' & b1' <=' b2' by A1,A8; reconsider B1 = b1, B2' = b2' as bag of n; B1 <=' B2' by A9,A10,Th46; hence [x,z] in BO by A1,A9,A10; end; dom BO = Bags n & field BO = Bags n by A2,ORDERS_1:98; then reconsider BO as Order of Bags n by A2,A3,A7,RELAT_2:def 9,def 12,def 16,PARTFUN1:def 4; take BO; let p, q be bag of n; A12: p in Bags n & q in Bags n by Def14; hereby assume [p, q] in BO; then consider b1, b2 being Element of Bags n such that A13: p = b1 & q = b2 & b1 <=' b2 by A1; thus p <=' q by A13; end; thus p <=' q implies [p,q] in BO by A1,A12; end; uniqueness proof let B1, B2 be Order of Bags n such that A14: for p, q being bag of n holds [p, q] in B1 iff p <=' q and A15: for p, q being bag of n holds [p, q] in B2 iff p <=' q; let a, b be set; hereby assume A16: [a,b] in B1; then consider b1, b2 being set such that A17: [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n by RELSET_1:6; reconsider b1, b2 as bag of n by A17,Def14; b1 <=' b2 by A14,A16,A17; hence [a,b] in B2 by A15,A17; end; assume A18: [a,b] in B2; then consider b1, b2 being set such that A19: [a,b] = [b1,b2] & b1 in Bags n & b2 in Bags n by RELSET_1:6; reconsider b1, b2 as bag of n by A19,Def14; b1 <=' b2 by A15,A18,A19; hence [a,b] in B1 by A14,A19; end; end; Lm1: for n being Ordinal holds BagOrder n is_reflexive_in Bags n proof let n be Ordinal; let x be set; assume x in Bags n; then reconsider x' = x as bag of n by Def14; x' <=' x'; hence thesis by Def16; end; Lm2: for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n proof let n be Ordinal; set BO = BagOrder n; let x, y be set; assume A1: x in Bags n & y in Bags n & [x,y] in BO & [y,x] in BO; then reconsider b1 = x, b2 = y as bag of n by Def14; A2: b1 <=' b2 by A1,Def16; reconsider b1' = y, b2' = x as bag of n by A1,Def14; b1' <=' b2' by A1,Def16; then (b1 < b2 or b1 = b2) & (b1' < b2' or b1' = b2') by A2,Def12; hence x = y; end; Lm3: for n being Ordinal holds BagOrder n is_transitive_in Bags n proof let n be Ordinal; set BO = BagOrder n; let x, y, z be set such that A1: x in Bags n & y in Bags n & z in Bags n and A2: [x,y] in BO & [y,z] in BO; reconsider b1 = x, b2 = y as bag of n by A1,Def14; A3: b1 <=' b2 by A2,Def16; reconsider b1'= y, b2' = z as bag of n by A1,Def14; A4: b1' <=' b2' by A2,Def16; reconsider B1 = b1, B2' = b2' as bag of n; B1 <=' B2' by A3,A4,Th46; hence [x,z] in BO by Def16; end; Lm4: for n being Ordinal holds BagOrder n linearly_orders Bags n proof let n be Ordinal; set BO = BagOrder n; A1: BO is_reflexive_in Bags n by Lm1; A2: BO is_antisymmetric_in Bags n by Lm2; A3: BO is_transitive_in Bags n by Lm3; BO is_connected_in Bags n proof let x, y be set; assume A4: x in Bags n & y in Bags n & x <> y & not [x,y] in BO; then reconsider p = x, q = y as bag of n by Def14; not p <=' q by A4,Def16; then q <=' p by Th49; hence [y,x] in BO by Def16; end; hence BagOrder n linearly_orders Bags n by A1,A2,A3,ORDERS_2:def 6; end; definition let n be Ordinal; cluster BagOrder n -> being_linear-order; coherence proof set BO = BagOrder n; A1: field BO = Bags n by ORDERS_2:2; BO linearly_orders Bags n by Lm4; then BO is_connected_in Bags n by ORDERS_2:def 6; then BO is connected by A1,RELAT_2:def 14; hence thesis by ORDERS_2:def 3; end; end; definition let X be set, f be Function of X, NAT; func NatMinor f -> Subset of Funcs(X, NAT) means :Def17: for g being natural-yielding ManySortedSet of X holds g in it iff for x being set st x in X holds g.x <= f.x; existence proof defpred P[set] means ex g being natural-yielding ManySortedSet of X st $1 = g & for x being set st x in X holds g.x <= f.x; consider IT being Subset of Funcs(X, NAT) such that A1: for h being set holds h in IT iff h in Funcs(X, NAT) & P[h] from Subset_Ex; take IT; let g be natural-yielding ManySortedSet of X; hereby assume g in IT; then consider g1 being natural-yielding ManySortedSet of X such that A2: g1 = g & for x being set st x in X holds g1.x <= f.x by A1; thus for x being set st x in X holds g.x <= f.x by A2; end; assume A3: for x being set st x in X holds g.x <= f.x; dom g = X & rng g c= NAT by PBOOLE:def 3,SEQM_3:def 8; then g is Function of X, NAT by FUNCT_2:def 1,RELSET_1:11; then g in Funcs(X, NAT) by FUNCT_2:11; hence g in IT by A1,A3; end; uniqueness proof let it1, it2 be Subset of Funcs(X, NAT) such that A4: for g being natural-yielding ManySortedSet of X holds g in it1 iff for x being set st x in X holds g.x <= f.x and A5: for g being natural-yielding ManySortedSet of X holds g in it2 iff for x being set st x in X holds g.x <= f.x; now let h be Element of Funcs(X, NAT); dom h = X & rng h c= NAT by ALTCAT_1:6; then A6: h is natural-yielding ManySortedSet of X by PBOOLE:def 3; hereby assume h in it1; then for x being set st x in X holds h.x <= f.x by A4,A6; hence h in it2 by A5,A6; end; assume h in it2; then for x being set st x in X holds h.x <= f.x by A5,A6; hence h in it1 by A4,A6; end; hence it1 = it2 by SUBSET_1:8; end; end; theorem Th65: for X being set, f being Function of X, NAT holds f in NatMinor f proof let X be set, f be Function of X, NAT; dom f = X by FUNCT_2:def 1; then A1: f is ManySortedSet of X by PBOOLE:def 3; for x being set st x in X holds f.x <= f.x; hence f in NatMinor f by A1,Def17; end; definition let X be set, f be Function of X, NAT; cluster NatMinor f -> non empty functional; coherence proof thus NatMinor f is non empty by Th65; let x be set; assume x in NatMinor f; hence x is Function by FUNCT_2:121; end; end; definition let X be set, f be Function of X, NAT; cluster -> natural-yielding Element of NatMinor f; coherence proof let x be Element of NatMinor f; rng x c= NAT by ALTCAT_1:6; hence x is natural-yielding by SEQM_3:def 8; end; end; theorem Th66: for X being set, f being finite-support Function of X, NAT holds NatMinor f c= Bags X proof let X be set, f be finite-support Function of X, NAT; let x be set; assume x in NatMinor f; then reconsider x' = x as Element of NatMinor f; A1: dom x' = X by ALTCAT_1:6; then A2: x' is ManySortedSet of X by PBOOLE:def 3; support x' c= support f proof let a be set; assume A3: a in support x'; then x'.a <> 0 by Def7; then A4: 0 < x'.a by NAT_1:19; support x' c= dom x' by Th41; then f.a <> 0 by A1,A2,A3,A4,Def17; hence a in support f by Def7; end; then support x' is finite by FINSET_1:13; then x is bag of X by A1,Def8,PBOOLE:def 3; hence x in Bags X by Def14; end; definition let X be set, f be finite-support Function of X, NAT; redefine func support f -> Element of Fin X; coherence proof dom f = X by FUNCT_2:def 1; then support f c= X by Th41; hence thesis by FINSUB_1:def 5; end; end; theorem Th67: for X being non empty set, f being finite-support Function of X, NAT holds Card NatMinor f = multnat $$ (support f, addnat[:](f,1)) proof let X be non empty set; defpred P[Element of Fin X] means for f being Function of X, NAT st for x being Element of X st not x in $1 holds f.x = 0 holds Card NatMinor f = multnat $$ ($1, addnat[:](f,1)); A1: P[{}.X] proof let f be Function of X, NAT such that A2: for x being Element of X st not x in {}.X holds f.x = 0; now let x be set; hereby assume A3: x in NatMinor f; then reconsider x' = x as Function of X, NAT by FUNCT_2:121; dom x' = X & rng x' c= NAT by FUNCT_2:def 1,RELSET_1:12; then reconsider x'' = x' as natural-yielding ManySortedSet of X by PBOOLE:def 3; now let c be Element of X; A4: x''.c <= f.c by A3,Def17; f.c = 0 by A2; hence x'.c = f.c by A4,NAT_1:19; end; hence x = f by FUNCT_2:113; end; thus x = f implies x in NatMinor f by Th65; end; then NatMinor f = {f} by TARSKI:def 1; hence Card NatMinor f = 1 by CARD_1:50,CARD_2:20 .= multnat $$ ({}.X, addnat[:](f,1)) by MONOID_0:67,SETWISEO:40; end; A5: for B being Element of Fin X, b being Element of X holds P[B] & not b in B implies P[B \/ {b}] proof let B be Element of Fin X, b be Element of X such that A6: P[B] & not b in B; let f be Function of X, NAT such that A7: for x being Element of X st not x in B \/ {b} holds f.x = 0; dom (addnat[:](f,1)) = X by Th2; then A8: addnat[:](f,1).b = addnat.(f.b,1) by FUNCOP_1:35 .= f.b+1 by BINARITH:1; set g = f+*(b,0); A9: dom f = X by FUNCT_2:def 1; for x being Element of X st not x in B holds g.x = 0 proof let x be Element of X such that A10: not x in B; per cases; suppose x = b; hence g.x = 0 by A9,FUNCT_7:33; suppose A11: x <> b; A12: now assume x in B \/ {b}; then x in B or x in {b} by XBOOLE_0:def 2; hence contradiction by A10,A11,TARSKI:def 1; end; thus g.x = f.x by A11,FUNCT_7:34 .= 0 by A7,A12; end; then A13: Card NatMinor g = (multnat $$ (B, addnat[:](g,1))) by A6; then reconsider ng = NatMinor g as functional finite non empty set by CARD_4:1; set cng = card ng; g|B = f|B by A6,SCMFSA6A:4; then addnat[:](g,1)|B = addnat[:](f,1)|B by FUNCOP_1:36; then A14: (multnat $$ (B, addnat[:](g,1))) = (multnat $$ (B, addnat[:](f,1))) by MONOID_0:67,SETWOP_2:9; A15: f.b < f.b+1 by REAL_1:69; then reconsider fb1 = f.b+1 as non empty Nat by EULER_1:1; [:ng,f.b+1 :],NatMinor f are_equipotent proof deffunc F(Element of ng,Element of fb1) = $1+*(b,$2); A16: for p being Element of ng, l being Element of fb1 holds F(p,l) in NatMinor f proof let p be Element of ng, l be Element of fb1; reconsider q = p as Element of NatMinor g; A17: fb1 c= NAT by ORDINAL1:def 2; l in fb1; then reconsider k = l as Nat by A17; p in NatMinor g; then A18: dom p = X by ALTCAT_1:6; then dom(p+*(b,l)) = X by FUNCT_7:32; then reconsider pbl = q+*(b,k) as natural-yielding ManySortedSet of X by PBOOLE:def 3; for x being set st x in X holds pbl.x <= f.x proof let x be set; assume A19: x in X; per cases; suppose A20: x = b; then A21: pbl.x = k by A18,FUNCT_7:33; k < fb1 by EULER_1:1; hence pbl.x <= f.x by A20,A21,NAT_1:38; suppose A22: x <> b; then A23: pbl.x = q.x by FUNCT_7:34; q is ManySortedSet of X by A18,PBOOLE:def 3; then q.x <= g.x by A19,Def17; hence pbl.x <= f.x by A22,A23,FUNCT_7:34; end; hence p+*(b,l) in NatMinor f by Def17; end; consider r being Function of [:ng,fb1:], NatMinor f such that A24: for p being Element of ng, l being Element of fb1 holds r.[p,l] = F(p,l) from Kappa2D(A16); take r; thus r is one-to-one proof let x1,x2 be set; assume A25: x1 in dom r & x2 in dom r & r.x1 = r.x2; then consider p1, l1 being set such that A26: x1 = [p1,l1] by ZFMISC_1:102; A27: p1 in ng & l1 in fb1 by A25,A26,ZFMISC_1:106; consider p2, l2 being set such that A28: x2 = [p2,l2] by A25,ZFMISC_1:102; A29: p2 in ng & l2 in fb1 by A25,A28,ZFMISC_1:106; reconsider p1 as Element of NatMinor g by A25,A26,ZFMISC_1:106; reconsider p2 as Element of NatMinor g by A25,A28,ZFMISC_1:106; A30: p1+*(b,l1) = r.[p1,l1] by A24,A27 .= p2+*(b,l2) by A24,A25,A26,A28,A29; A31: dom p1 = X by ALTCAT_1:6; A32: dom p2 = X by ALTCAT_1:6; then reconsider p1' = p1, p2' = p2 as natural-yielding ManySortedSet of X by A31,PBOOLE:def 3; A33: now let x be set; assume A34: x in X; per cases; suppose A35: x = b; A36: g.b = 0 by A9,FUNCT_7:33; A37: p1'.x <= g.x & p2'.x <= g.x by A34,Def17; hence p1'.x = 0 by A35,A36,NAT_1:19 .= p2'.x by A35,A36,A37,NAT_1:19; suppose A38: x <> b; hence p1'.x = (p1+*(b,l1)).x by FUNCT_7:34 .= p2'.x by A30,A38,FUNCT_7:34; end; l1 = (p1+*(b,l1)).b by A31,FUNCT_7:33 .= l2 by A30,A32,FUNCT_7:33; hence x1 = x2 by A26,A28,A33,PBOOLE:3; end; thus A39: dom r = [:ng,f.b+1 :] by FUNCT_2:def 1; thus rng r c= NatMinor f by RELSET_1:12; thus NatMinor f c= rng r proof let x be set; assume x in NatMinor f; then reconsider e = x as Element of NatMinor f; A40: dom e = X by ALTCAT_1:6; then A41: e is ManySortedSet of X by PBOOLE:def 3; dom (e+*(b,0)) = X by A40,FUNCT_7:32; then reconsider eb0 = e+*(b,0) as natural-yielding ManySortedSet of X by PBOOLE:def 3; now let x be set; assume A42: x in X; per cases; suppose A43: x = b; then eb0.x = 0 by A40,FUNCT_7:33; hence eb0.x <= g.x by A9,A43,FUNCT_7:33; suppose A44: x <> b; then A45: eb0.x = e.x by FUNCT_7:34; e.x <= f.x by A41,A42,Def17; hence eb0.x <= g.x by A44,A45,FUNCT_7:34; end; then reconsider eb0 as Element of NatMinor g by Def17; e.b <= f.b by A41,Def17; then e.b < fb1 by A15,AXIOMS:22; then A46: e.b in fb1 by EULER_1:1; then A47: [eb0,e.b] in dom r by A39,ZFMISC_1:106; e = e+*(b,e.b) by FUNCT_7:37 .= eb0+*(b,e.b) by FUNCT_7:36; then e = r.[eb0,e.b] by A24,A46; hence x in rng r by A47,FUNCT_1:def 5; end; end; hence Card NatMinor f = card [:ng,f.b+1 :] by CARD_1:21 .= cng * card(f.b+1) by CARD_2:65 .= cng * (f.b+1) by CARD_1:def 5 .= multnat.(multnat $$ (B, addnat[:](f,1)), f.b+1) by A13,A14,Th1 .= multnat $$ (B \/ {b}, addnat[:](f,1)) by A6,A8,MONOID_0:67,SETWOP_2:4; end; A48: for B being Element of Fin X holds P[B] from FinSubInd1(A1,A5); let f be finite-support Function of X, NAT; for x being Element of X holds not x in support f implies f.x = 0 by Def7; hence Card NatMinor f = multnat $$ (support f, addnat[:](f,1)) by A48; end; definition let X be set, f be finite-support Function of X, NAT; cluster NatMinor f -> finite; coherence proof per cases; suppose X is empty; then NatMinor f c= Funcs({},NAT); then NatMinor f c= {{}} by FUNCT_5:64; hence thesis by FINSET_1:13; suppose X is not empty; then reconsider X as non empty set; reconsider f as finite-support Function of X, NAT; Card NatMinor f = multnat $$ (support f, addnat[:](f,1)) by Th67; hence thesis by CARD_4:1; end; end; definition let n be Ordinal, b be bag of n; func divisors b -> FinSequence of Bags n means :Def18: 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; existence proof dom b = n & rng b c= NAT by PBOOLE:def 3,SEQM_3:def 8; then reconsider f = b as finite-support Function of n, NAT by FUNCT_2:def 1,RELSET_1:11; reconsider S = NatMinor f as non empty finite Subset of Bags n by Th66; take IT = SgmX(BagOrder n, S); take S; thus IT = SgmX(BagOrder n, S); let p be bag of n; thus p in S implies p divides b proof assume p in S; then for x being set st x in n holds p.x <= b.x by Def17; hence p divides b by Th50; end; assume p divides b; then for x being set st x in n holds p.x <= b.x by Def13; hence p in S by Def17; end; uniqueness proof let it1, it2 be FinSequence of Bags n; given S1 being non empty finite Subset of Bags n such that A1: it1 = SgmX(BagOrder n, S1) and A2: (for p being bag of n holds p in S1 iff p divides b); given S2 being non empty finite Subset of Bags n such that A3: it2 = SgmX(BagOrder n, S2) and A4: (for p being bag of n holds p in S2 iff p divides b); now let x be set; hereby assume A5: x in S1; then reconsider x' = x as Element of Bags n; x' divides b by A2,A5; hence x in S2 by A4; end; assume A6: x in S2; then reconsider x' = x as Element of Bags n; x' divides b by A4,A6; hence x in S1 by A2; end; hence it1 = it2 by A1,A3,TARSKI:2; end; end; definition let n be Ordinal, b be bag of n; cluster divisors b -> non empty one-to-one; coherence proof ex S being non empty finite Subset of Bags n st divisors b = SgmX(BagOrder n, S) & (for p being bag of n holds p in S iff p divides b) by Def18; hence thesis; end; end; theorem Th68: for n being Ordinal,i being Nat, b being bag of n st i in dom divisors b holds ((divisors b)/.i) qua Element of Bags n divides b proof let n be Ordinal,i be Nat, b be bag of n; assume A1: i in dom divisors b; consider S being non empty finite Subset of Bags n such that A2: divisors b = SgmX(BagOrder n, S) and A3: (for p being bag of n holds p in S iff p divides b) by Def18; BagOrder n linearly_orders Bags n by Lm4; then A4: BagOrder n linearly_orders S by ORDERS_2:36; A5: (divisors b)/.i = (divisors b).i by A1,FINSEQ_4:def 4; (divisors b)/.i is Element of Bags n; then reconsider pid = (divisors b)/.i as bag of n; (divisors b).i in rng divisors b by A1,FUNCT_1:def 5; then pid in S by A2,A4,A5,TRIANG_1:def 2; hence thesis by A3; end; theorem Th69: for n being Ordinal, b being bag of n holds (divisors b)/.1 = EmptyBag n & (divisors b)/.len divisors b = b proof let n be Ordinal, b be bag of n; consider S being non empty finite Subset of Bags n such that A1: divisors b = SgmX(BagOrder n, S) and A2: (for p being bag of n holds p in S iff p divides b) by Def18; EmptyBag n divides b by Th63; then A3: EmptyBag n in S by A2; BagOrder n linearly_orders Bags n by Lm4; then A4: BagOrder n linearly_orders S by ORDERS_2:36; now let y be Element of Bags n; assume y in S; EmptyBag n <=' y by Th64; hence [EmptyBag n, y] in BagOrder n by Def16; end; hence (divisors b)/.1 = EmptyBag n by A1,A3,A4,Th8; A5: b in S by A2; now let y be Element of Bags n; assume y in S; then y divides b by A2; then y <=' b by Th53; hence [y,b] in BagOrder n by Def16; end; hence thesis by A1,A4,A5,Th9; end; theorem Th70: 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 proof let n be Ordinal, i be Nat, b, b1, b2 be bag of n; A1: (divisors b)/.1 = EmptyBag n & (divisors b)/.len divisors b = b by Th69; A2: 1 in dom divisors b & len divisors b in dom divisors b by FINSEQ_5:6; assume A3: i > 1 & i < len divisors b; then i in dom divisors b by FINSEQ_3:27; hence thesis by A1,A2,A3,PARTFUN2:17; end; theorem Th71: for n being Ordinal holds divisors EmptyBag n = <* EmptyBag n *> proof let n be Ordinal; consider S being non empty finite Subset of Bags n such that A1: divisors EmptyBag n = SgmX(BagOrder n, S) and A2: for p being bag of n holds p in S iff p divides EmptyBag n by Def18; BagOrder n linearly_orders Bags n by Lm4; then A3: BagOrder n linearly_orders S by ORDERS_2:36; EmptyBag n in S by A2; then A4: { EmptyBag n } c= S by ZFMISC_1:37; S c= { EmptyBag n} proof let x be set; assume A5: x in S; then reconsider b = x as bag of n by Def14; b divides EmptyBag n by A2,A5; then b = EmptyBag n by Th62; hence x in {EmptyBag n} by TARSKI:def 1; end; then S = { EmptyBag n} by A4,XBOOLE_0:def 10; then A6: rng divisors EmptyBag n = {EmptyBag n} by A1,A3,TRIANG_1:def 2; len divisors EmptyBag n = card rng divisors EmptyBag n by Th7 .= 1 by A6,CARD_1:79; hence divisors EmptyBag n = <* EmptyBag n *> by A6,FINSEQ_1:56; end; definition let n be Ordinal, b be bag of n; func decomp b -> FinSequence of 2-tuples_on Bags n means :Def19: dom it = dom divisors b & for i being Nat, p being bag of n st i in dom it & p = (divisors b)/.i holds it/.i = <*p, b-'p*>; existence proof defpred P[Nat,set] means for p being bag of n st p = (divisors b)/.$1 holds $2 = <*p,b-'p*>; A1: for k being Nat st k in Seg len divisors b ex d being Element of 2-tuples_on Bags n st P[k,d] proof let k be Nat such that k in Seg len divisors b; reconsider p = (divisors b)/.k as bag of n by Def14; reconsider b1=p, b2=b-'p as Element of Bags n by Def14; len<*p,b-'p*> = 2 by FINSEQ_1:61; then reconsider d = <*b1,b2*> as Element of 2-tuples_on Bags n by FINSEQ_2:110; take d; thus P[k,d]; end; consider f being FinSequence of 2-tuples_on Bags n such that A2: len f = len divisors b and A3: for n being Nat st n in Seg len divisors b holds P[n,f/.n] from FinSeqDChoice(A1); take f; thus dom f = dom divisors b by A2,FINSEQ_3:31; let i be Nat, p be bag of n such that A4: i in dom f and A5: p = (divisors b)/.i; i in Seg len divisors b by A2,A4,FINSEQ_1:def 3; hence f/.i = <*p, b-'p*> by A3,A5; end; uniqueness proof let F,G be FinSequence of 2-tuples_on Bags n such that A6: dom F = dom divisors b and A7: for i being Nat, p being bag of n st i in dom F & p = (divisors b)/.i holds F/.i = <*p, b-'p*> and A8: dom G = dom divisors b and A9: for i being Nat, p being bag of n st i in dom G & p = (divisors b)/.i holds G/.i = <*p, b-'p*>; now let i be Nat; reconsider p = (divisors b)/.i as bag of n by Def14; assume A10: i in dom F; hence F/.i = <*p,b-'p*> by A7 .= G/.i by A6,A8,A9,A10; end; hence F = G by A6,A8,FINSEQ_5:13; end; end; theorem Th72: for n being Ordinal, i being 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 proof let n be Ordinal, i be Nat, b be bag of n; assume A1: i in dom decomp b; then A2: i in dom divisors b by Def19; reconsider p = (divisors b)/.i as bag of n by Def14; take p, b-'p; thus (decomp b)/.i = <*p,b-'p*> by A1,Def19; p divides b by A2,Th68; hence b = p + (b-'p) by Th51; end; theorem Th73: for n being Ordinal, b, b1, b2 being bag of n st b = b1+b2 ex i being Nat st i in dom decomp b & (decomp b)/.i = <*b1, b2*> proof let n be Ordinal, b, b1, b2 be bag of n; consider S being non empty finite Subset of Bags n such that A1: divisors b = SgmX(BagOrder n, S) and A2: for p being bag of n holds p in S iff p divides b by Def18; BagOrder n linearly_orders Bags n by Lm4; then A3: BagOrder n linearly_orders S by ORDERS_2:36; assume A4: b = b1+b2; then b1 divides b by Th54; then b1 in S by A2; then b1 in rng divisors b by A1,A3,TRIANG_1:def 2; then consider i being Nat such that A5: i in dom divisors b and A6: (divisors b)/.i= b1 by PARTFUN2:4; take i; thus i in dom decomp b by A5,Def19; then (decomp b)/.i = <*b1, b-'b1*> by A6,Def19; hence (decomp b)/.i = <*b1, b2*> by A4,Th52; end; theorem Th74: for n being Ordinal, i being Nat, b,b1,b2 being bag of n st i in dom decomp b & (decomp b)/.i = <*b1, b2*> holds b1 = (divisors b)/.i proof let n be Ordinal, i be Nat, b,b1,b2 be bag of n; reconsider p = (divisors b)/.i as bag of n by Def14; assume i in dom decomp b & (decomp b)/.i = <*b1, b2*>; then <*b1,b2*> = <*p,b-'p*> by Def19; hence b1 = (divisors b)/.i by GROUP_7:2; end; definition let n be Ordinal, b be bag of n; cluster decomp b -> non empty one-to-one FinSequence-yielding; coherence proof A1: dom divisors b = dom decomp b by Def19; hence decomp b is non empty by RELAT_1:60; now let k,m be Nat; assume A2: k in dom decomp b; assume A3: m in dom decomp b; then consider bm1, bm2 being bag of n such that A4: (decomp b)/.m = <*bm1, bm2*> and b = bm1+bm2 by Th72; assume (decomp b)/.k = (decomp b)/.m; then (divisors b)/.k = bm1 by A2,A4,Th74 .= (divisors b)/.m by A3,A4,Th74; hence k = m by A1,A2,A3,PARTFUN2:17; end; hence decomp b is one-to-one by PARTFUN2:16; let x be set; assume A5: x in dom decomp b; then reconsider k = x as Nat; reconsider p = (divisors b)/.k as bag of n by Def14; (decomp b)/.k = <*p,b-'p*> by A5,Def19; hence (decomp b).x is FinSequence by A5,FINSEQ_4:def 4; end; end; definition let n be Ordinal, b be Element of Bags n; cluster decomp b -> non empty one-to-one FinSequence-yielding; coherence; end; theorem Th75: for n being Ordinal, b being bag of n holds (decomp b)/.1 = <*EmptyBag n, b*> & (decomp b)/.len decomp b = <*b, EmptyBag n*> proof let n be Ordinal, b be bag of n; dom decomp b = dom divisors b by Def19; then A1: len decomp b = len divisors b by FINSEQ_3:31; reconsider p = (divisors b)/.1 as bag of n by Def14; A2: p = EmptyBag n by Th69; 1 in dom decomp b by FINSEQ_5:6; hence (decomp b)/.1 = <*EmptyBag n, b-'EmptyBag n*> by A2,Def19 .= <*EmptyBag n, b*> by Th58; reconsider p = (divisors b)/.len decomp b as bag of n by Def14; A3: p = b by A1,Th69; len decomp b in dom decomp b by FINSEQ_5:6; hence (decomp b)/.len decomp b = <*b,b-'b*> by A3,Def19 .= <*b, EmptyBag n*> by Th60; end; theorem Th76: 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 proof let n be Ordinal, i be Nat, b, b1, b2 be bag of n such that A1: i > 1 and A2: i < len decomp b and A3: (decomp b)/.i = <*b1, b2*>; A4: dom decomp b = dom divisors b by Def19; then A5: len decomp b = len divisors b by FINSEQ_3:31; reconsider p = (divisors b)/.i as bag of n by Def14; A6: i in dom decomp b by A1,A2,FINSEQ_3:27; then (decomp b)/.i = <*p,b-'p*> by Def19; then A7: b1 = p & b2 = b-'p by A3,GROUP_7:2; hence b1 <> EmptyBag n by A1,A2,A5,Th70; assume A8: b2 = EmptyBag n; p divides b by A4,A6,Th68; then p = b by A7,A8,Th61; hence contradiction by A1,A2,A5,Th70; end; theorem Th77: for n being Ordinal holds decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> proof let n be Ordinal; len<*EmptyBag n, EmptyBag n*> = 2 by FINSEQ_1:61; then reconsider E = <*EmptyBag n, EmptyBag n*> as Element of 2-tuples_on Bags n by FINSEQ_2:110; rng<* E *> c= 2-tuples_on Bags n proof let u be set; assume u in rng<* E *>; then u in {E} by FINSEQ_1:56; then u = E by TARSKI:def 1; hence u in 2-tuples_on Bags n; end; then reconsider e = <* E *> as FinSequence of 2-tuples_on Bags n by FINSEQ_1:def 4; A1: <* EmptyBag n *> = divisors EmptyBag n by Th71; A2: dom e = Seg 1 by FINSEQ_1:55; then A3: dom e = dom divisors EmptyBag n by A1,FINSEQ_1:55; for i being Nat, p being bag of n st i in dom e & p = (divisors EmptyBag n)/.i holds e/.i = <*p, (EmptyBag n)-'p*> proof let i be Nat, p be bag of n such that A4: i in dom e and A5: p = (divisors EmptyBag n)/.i; A6: i = 1 by A2,A4,FINSEQ_1:4,TARSKI:def 1; then A7: (divisors EmptyBag n)/.i = EmptyBag n by A1,FINSEQ_4:25; thus e/.i = E by A6,FINSEQ_4:25 .= <*p, (EmptyBag n)-'p*> by A5,A7,Th58; end; hence decomp EmptyBag n = <* <*EmptyBag n, EmptyBag n*> *> by A3,Def19; end; theorem Th78: 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)/.1) qua Element of Bags n))) ^^ ((len (decomp ((((decomp b)/.k)/.1) qua Element of Bags n))) |-> <*(((decomp b)/.k)/.2)*>)) & (for k being Nat st k in dom g holds g.k = ((len (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))) |-> <*((decomp b)/.k)/.1*>) ^^ (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))) ex p being Permutation of dom FlattenSeq f st FlattenSeq g = (FlattenSeq f)*p proof let n be Ordinal, b be bag of n, f, g be FinSequence of (3-tuples_on Bags n)* such that A1: dom f = dom decomp b and A2: dom g = dom decomp b and A3: (for k being Nat st k in dom f holds f.k = ((decomp ((((decomp b)/.k)/.1) qua Element of Bags n))) ^^ ((len (decomp ((((decomp b)/.k)/.1) qua Element of Bags n))) |-> <*(((decomp b)/.k)/.2)*>)) and A4: (for k being Nat st k in dom g holds g.k = ((len (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))) |-> <*(((decomp b)/.k)/.1)*>) ^^ (decomp ((((decomp b)/.k)/.2) qua Element of Bags n))); set Ff = FlattenSeq f, Fg = FlattenSeq g, db = decomp b; now let y be set; hereby assume y in rng Ff; then consider k being set such that A5: k in dom Ff & y = Ff.k by FUNCT_1:def 5; reconsider k as Nat by A5; consider i, j being Nat such that A6: i in dom f and A7: j in dom (f.i) and k = (Sum Card (f|(i-'1))) + j and A8: (f.i).j = Ff.k by A5,Th32; set ddbi1 = decomp (((db/.i)/.1) qua Element of Bags n); A9: f.i = ddbi1 ^^ ((len ddbi1) |-> <*(db/.i)/.2*>) by A3,A6; consider b1, b2 being bag of n such that A10: db/.i = <*b1,b2*> and A11: b = b1+b2 by A1,A6,Th72; reconsider b1' = b1, b2' = b2 as Element of Bags n by Def14; A12: b1' = b1 & b2' = b2; then A13: (db/.i)/.1 = b1 by A10,FINSEQ_4:26; A14: (db/.i)/.2 = b2 by A10,A12,FINSEQ_4:26; A15: dom (f.i) = dom ddbi1 /\ dom ((len ddbi1) |-> <*(db/.i)/.2*>) by A9,MATRLIN:def 2 .= dom ddbi1 /\ Seg len ddbi1 by FINSEQ_2:68 .= dom ddbi1 /\ dom ddbi1 by FINSEQ_1:def 3 .= dom ddbi1; then consider b11, b12 being bag of n such that A16: ddbi1/.j = <*b11, b12*> and A17: b1 = b11+b12 by A7,A13,Th72; A18: dom ddbi1 = Seg len ddbi1 by FINSEQ_1:def 3; A19: ddbi1/.j = ddbi1.j by A7,A15,FINSEQ_4:def 4; ((len ddbi1) |-> <*(db/.i)/.2*>).j = <*(db/.i)/.2*> by A7,A15,A18,FINSEQ_2:70; then A20: (f.i).j = <*b11,b12*>^<*b2*> by A7,A9,A14,A16,A19,MATRLIN:def 2 .= <*b11,b12,b2*> by FINSEQ_1:60; b = b11+(b12+b2) by A11,A17,Th39; then consider i' being Nat such that A21: i' in dom decomp b and A22: (decomp b)/.i' = <*b11, b12+b2*> by Th73; set b3 = b12+b2; consider j' being Nat such that A23: j' in dom decomp b3 and A24: (decomp b3)/.j' = <*b12, b2*> by Th73; set ddbi'2 = decomp ((((decomp b)/.i')/.2) qua Element of Bags n); A25: g.i' = ((len ddbi'2) |-> <*((decomp b)/.i')/.1*>) ^^ ddbi'2 by A2,A4, A21; reconsider b11' = b11, b3' = b3 as Element of Bags n by Def14; A26: (decomp b)/.i' = <*b11', b3'*> by A22; then A27: ((decomp b)/.i')/.1 = b11 by FINSEQ_4:26; A28: ddbi'2 = decomp b3 by A26,FINSEQ_4:26; A29: dom (g.i') = dom ((len ddbi'2) |-> <*((decomp b)/.i')/.1*>) /\ dom ddbi'2 by A25,MATRLIN:def 2 .= Seg len ddbi'2 /\ dom ddbi'2 by FINSEQ_2:68 .= dom ddbi'2 /\ dom ddbi'2 by FINSEQ_1:def 3 .= dom ddbi'2; then A30: j' in dom (g.i') by A23,A26,FINSEQ_4:26; then A31: j' in Seg len ddbi'2 by A29,FINSEQ_1:def 3; A32: (decomp b3)/.j' = (decomp b3).j' by A23,FINSEQ_4:def 4; A33: (g.i').j' = (((len ddbi'2) |-> <*((decomp b)/.i')/.1*>)).j' ^ (ddbi'2).j' by A25,A30,MATRLIN:def 2 .= <*b11*>^<*b12,b2*> by A24,A27,A28,A31,A32,FINSEQ_2:70 .= <*b11,b12,b2*> by FINSEQ_1:60; set m = (Sum Card (g|(i'-'1))) + j'; A34: m in dom Fg by A2,A21,A30,Th33; Fg.m = (g.i').j' by A2,A21,A30,Th33; hence y in rng Fg by A5,A8,A20,A33,A34,FUNCT_1:def 5; end; assume y in rng Fg; then consider k being set such that A35: k in dom Fg & y = Fg.k by FUNCT_1:def 5; reconsider k as Nat by A35; consider i, j being Nat such that A36: i in dom g and A37: j in dom (g.i) and k = (Sum Card (g|(i-'1))) + j and A38: (g.i).j = Fg.k by A35,Th32; set ddbi1 = decomp (((db/.i)/.2) qua Element of Bags n); A39: g.i = ((len ddbi1) |-> <*(db/.i)/.1*>) ^^ ddbi1 by A4,A36; consider b1, b2 being bag of n such that A40: db/.i = <*b1,b2*> and A41: b = b1+b2 by A2,A36,Th72; reconsider b1' = b1, b2' = b2 as Element of Bags n by Def14; A42: b1' = b1 & b2' = b2; then A43: (db/.i)/.1 = b1 by A40,FINSEQ_4:26; A44: (db/.i)/.2 = b2 by A40,A42,FINSEQ_4:26; A45: dom (g.i) = dom ddbi1 /\ dom ((len ddbi1) |-> <*(db/.i)/.1*>) by A39,MATRLIN:def 2 .= dom ddbi1 /\ Seg len ddbi1 by FINSEQ_2:68 .= dom ddbi1 /\ dom ddbi1 by FINSEQ_1:def 3 .= dom ddbi1; then consider b11, b12 being bag of n such that A46: ddbi1/.j = <*b11, b12*> and A47: b2 = b11+b12 by A37,A44,Th72; A48: ddbi1/.j = ddbi1.j by A37,A45,FINSEQ_4:def 4; dom ddbi1 = Seg len ddbi1 by FINSEQ_1:def 3; then ((len ddbi1) |-> <*(db/.i)/.1*>).j = <*(db/.i)/.1*> by A37,A45,FINSEQ_2:70; then A49: (g.i).j = <*b1*>^<*b11,b12*> by A37,A39,A43,A46,A48,MATRLIN:def 2 .= <*b1,b11,b12*> by FINSEQ_1:60; b = b1+b11+b12 by A41,A47,Th39; then consider i' being Nat such that A50: i' in dom decomp b and A51: (decomp b)/.i' = <*b1+b11, b12*> by Th73; set b3 = b1+b11; consider j' being Nat such that A52: j' in dom decomp b3 and A53: (decomp b3)/.j' = <*b1, b11*> by Th73; set ddbi'2 = decomp ((((decomp b)/.i')/.1) qua Element of Bags n); A54: f.i' = ddbi'2 ^^ ((len ddbi'2) |-> <*((decomp b)/.i')/.2*>) by A1,A3,A50; reconsider b3' = b3, b12' = b12 as Element of Bags n by Def14; A55: (decomp b)/.i' = <*b3', b12'*> by A51; then A56: ((decomp b)/.i')/.2 = b12 by FINSEQ_4:26; A57: ((decomp b)/.i')/.1 = b3 by A55,FINSEQ_4:26; A58: dom (f.i') = dom ((len ddbi'2) |-> <*((decomp b)/.i')/.2*>) /\ dom ddbi'2 by A54,MATRLIN:def 2 .= Seg len ddbi'2 /\ dom ddbi'2 by FINSEQ_2:68 .= dom ddbi'2 /\ dom ddbi'2 by FINSEQ_1:def 3 .= dom ddbi'2; A59: j' in Seg len ddbi'2 by A52,A57,FINSEQ_1:def 3; A60: (decomp b3)/.j' = (decomp b3).j' by A52,FINSEQ_4:def 4; A61: (f.i').j' = (ddbi'2).j' ^ (((len ddbi'2) |-> <*((decomp b)/.i')/.2*>)).j' by A52,A54,A57,A58,MATRLIN:def 2 .= <*b1,b11*>^<*b12*> by A53,A56,A57,A59,A60,FINSEQ_2:70 .= <*b1,b11,b12*> by FINSEQ_1:60; set m = (Sum Card (f|(i'-'1))) + j'; A62: m in dom Ff by A1,A50,A52,A57,A58,Th33; Ff.m = (f.i').j' by A1,A50,A52,A57,A58,Th33; hence y in rng Ff by A35,A38,A49,A61,A62,FUNCT_1:def 5; end; then A63: rng Ff = rng Fg by TARSKI:2; A64: Ff is one-to-one proof let k1, k2 be set such that A65: k1 in dom Ff and A66: k2 in dom Ff and A67: Ff.k1 = Ff.k2; consider i1, j1 being Nat such that A68: i1 in dom f and A69: j1 in dom (f.i1) and A70: k1 = (Sum Card (f|(i1-'1))) + j1 and A71: (f.i1).j1 = Ff.k1 by A65,Th32; consider i2, j2 being Nat such that A72: i2 in dom f and A73: j2 in dom (f.i2) and A74: k2 = (Sum Card (f|(i2-'1))) + j2 and A75: (f.i2).j2 = Ff.k2 by A66,Th32; set ddbi11 = decomp (((db/.i1)/.1) qua Element of Bags n); A76: f.i1 = ddbi11 ^^ ((len ddbi11) |-> <*(db/.i1)/.2*>) by A3,A68; A77: db/.i1 = db.i1 by A1,A68,FINSEQ_4:def 4; consider b11, b12 being bag of n such that A78: db/.i1 = <*b11,b12*> and b = b11+b12 by A1,A68,Th72; reconsider b11' = b11, b12' = b12 as Element of Bags n by Def14; A79: b11' = b11 & b12' = b12; then A80: (db/.i1)/.1 = b11 by A78,FINSEQ_4:26; A81: (db/.i1)/.2 = b12 by A78,A79,FINSEQ_4:26; A82: dom (f.i1) = dom ddbi11 /\ dom ((len ddbi11) |-> <*(db/.i1)/.2*>) by A76,MATRLIN:def 2 .= dom ddbi11 /\ Seg len ddbi11 by FINSEQ_2:68 .= dom ddbi11 /\ dom ddbi11 by FINSEQ_1:def 3 .= dom ddbi11; then consider b111, b112 being bag of n such that A83: ddbi11/.j1 = <*b111, b112*> and A84: b11 = b111+b112 by A69,A80,Th72; A85: ddbi11/.j1 = ddbi11.j1 by A69,A82,FINSEQ_4:def 4; dom ddbi11 = Seg len ddbi11 by FINSEQ_1:def 3; then ((len ddbi11) |-> <*(db/.i1)/.2*>).j1 = <*(db/.i1)/.2*> by A69,A82,FINSEQ_2:70; then A86: (f.i1).j1 = <*b111,b112*>^<*b12*> by A69,A76,A81,A83,A85,MATRLIN: def 2 .= <*b111,b112,b12*> by FINSEQ_1:60; set ddbi21 = decomp (((db/.i2)/.1) qua Element of Bags n); A87: f.i2 = ddbi21 ^^ ((len ddbi21) |-> <*(db/.i2)/.2*>) by A3,A72; A88: db/.i2 = db.i2 by A1,A72,FINSEQ_4:def 4; consider b21, b22 being bag of n such that A89: db/.i2 = <*b21,b22*> and b = b21+b22 by A1,A72,Th72; reconsider b21' = b21, b22' = b22 as Element of Bags n by Def14; A90: b21' = b21 & b22' = b22; then A91: (db/.i2)/.1 = b21 by A89,FINSEQ_4:26; A92: (db/.i2)/.2 = b22 by A89,A90,FINSEQ_4:26; A93: dom (f.i2) = dom ddbi21 /\ dom ((len ddbi21) |-> <*(db/.i2)/.2*>) by A87,MATRLIN:def 2 .= dom ddbi21 /\ Seg len ddbi21 by FINSEQ_2:68 .= dom ddbi21 /\ dom ddbi21 by FINSEQ_1:def 3 .= dom ddbi21; then consider b211, b212 being bag of n such that A94: ddbi21/.j2 = <*b211, b212*> and A95: b21 = b211+b212 by A73,A91,Th72; A96: dom ddbi21 = Seg len ddbi21 by FINSEQ_1:def 3; A97: ddbi21/.j2 = ddbi21.j2 by A73,A93,FINSEQ_4:def 4; ((len ddbi21) |-> <*(db/.i2)/.2*>).j2 = <*(db/.i2)/.2*> by A73,A93,A96,FINSEQ_2:70; then (f.i2).j2 = <*b211,b212*>^<*b22*> by A73,A87,A92,A94,A97,MATRLIN:def 2 .= <*b211,b212,b22*> by FINSEQ_1:60; then A98: b111 = b211 & b112 = b212 & b12 = b22 by A67,A71,A75,A86,GROUP_7:3; then i1 = i2 by A1,A68,A72,A77,A78,A84,A88,A89,A95,FUNCT_1:def 8; hence k1 = k2 by A69,A70,A73,A74,A83,A85,A93,A94,A97,A98,FUNCT_1:def 8; end; Fg is one-to-one proof let k1, k2 be set such that A99: k1 in dom Fg and A100: k2 in dom Fg and A101: Fg.k1 = Fg.k2; consider i1, j1 being Nat such that A102: i1 in dom g and A103: j1 in dom (g.i1) and A104: k1 = (Sum Card (g|(i1-'1))) + j1 and A105: (g.i1).j1 = Fg.k1 by A99,Th32; consider i2, j2 being Nat such that A106: i2 in dom g and A107: j2 in dom (g.i2) and A108: k2 = (Sum Card (g|(i2-'1))) + j2 and A109: (g.i2).j2 = Fg.k2 by A100,Th32; set ddbi11 = decomp (((db/.i1)/.2) qua Element of Bags n); A110: g.i1 = ((len ddbi11) |-> <*(db/.i1)/.1*>)^^ddbi11 by A4,A102; A111: db/.i1 = db.i1 by A2,A102,FINSEQ_4:def 4; consider b11, b12 being bag of n such that A112: db/.i1 = <*b11,b12*> and b = b11+b12 by A2,A102,Th72; reconsider b11' = b11, b12' = b12 as Element of Bags n by Def14; A113: b11' = b11 & b12' = b12; then A114: (db/.i1)/.1 = b11 by A112,FINSEQ_4:26; A115: (db/.i1)/.2 = b12 by A112,A113,FINSEQ_4:26; A116: dom (g.i1) = dom ddbi11 /\ dom ((len ddbi11) |-> <*(db/.i1)/.1*>) by A110,MATRLIN:def 2 .= dom ddbi11 /\ Seg len ddbi11 by FINSEQ_2:68 .= dom ddbi11 /\ dom ddbi11 by FINSEQ_1:def 3 .= dom ddbi11; then consider b111, b112 being bag of n such that A117: ddbi11/.j1 = <*b111, b112*> and A118: b12 = b111+b112 by A103,A115,Th72; A119: dom ddbi11 = Seg len ddbi11 by FINSEQ_1:def 3; A120: ddbi11/.j1 = ddbi11.j1 by A103,A116,FINSEQ_4:def 4; ((len ddbi11) |-> <*(db/.i1)/.1*>).j1 = <*(db/.i1)/.1*> by A103,A116,A119,FINSEQ_2:70; then A121: (g.i1).j1 = <*b11*>^<*b111,b112*> by A103,A110,A114,A117,A120, MATRLIN:def 2 .= <*b11,b111,b112*> by FINSEQ_1:60; set ddbi21 = decomp (((db/.i2)/.2) qua Element of Bags n); A122: g.i2 = ((len ddbi21) |-> <*(db/.i2)/.1*>) ^^ ddbi21 by A4,A106; A123: db/.i2 = db.i2 by A2,A106,FINSEQ_4:def 4; consider b21, b22 being bag of n such that A124: db/.i2 = <*b21,b22*> and b = b21+b22 by A2,A106,Th72; reconsider b21' = b21, b22' = b22 as Element of Bags n by Def14; A125: b21' = b21 & b22' = b22; then A126: (db/.i2)/.1 = b21 by A124,FINSEQ_4:26; A127: (db/.i2)/.2 = b22 by A124,A125,FINSEQ_4:26; A128: dom (g.i2) = dom ddbi21 /\ dom ((len ddbi21) |-> <*(db/.i2)/.1*>) by A122,MATRLIN:def 2 .= dom ddbi21 /\ Seg len ddbi21 by FINSEQ_2:68 .= dom ddbi21 /\ dom ddbi21 by FINSEQ_1:def 3 .= dom ddbi21; then consider b211, b212 being bag of n such that A129: ddbi21/.j2 = <*b211, b212*> and A130: b22 = b211+b212 by A107,A127,Th72; A131: ddbi21/.j2 = ddbi21.j2 by A107,A128,FINSEQ_4:def 4; dom ddbi21 = Seg len ddbi21 by FINSEQ_1:def 3; then ((len ddbi21) |-> <*(db/.i2)/.1*>).j2 = <*(db/.i2)/.1*> by A107,A128,FINSEQ_2:70; then (g.i2).j2 = <*b21*>^<*b211,b212*> by A107,A122,A126,A129,A131,MATRLIN: def 2 .= <*b21,b211, b212*> by FINSEQ_1:60; then A132: b111 = b211 & b112 = b212 & b11 = b21 by A101,A105,A109,A121,GROUP_7:3; then i1 = i2 by A2,A102,A106,A111,A112,A118,A123,A124,A130,FUNCT_1:def 8; hence k1 = k2 by A103,A104,A107,A108,A117,A120,A128,A129,A131,A132,FUNCT_1:def 8; end; then Ff, Fg are_fiberwise_equipotent by A63,A64,VECTSP_9:4; hence ex p being Permutation of dom FlattenSeq f st FlattenSeq g = (FlattenSeq f)*p by RFINSEQ:17; end; begin :: Formal power series -------------------------------------------------- definition let X be set, S be 1-sorted; mode Series of X, S is Function of Bags X, S; canceled; end; definition let n be set, L be non empty LoopStr, p, q be Series of n, L; func p+q -> Series of n, L means :Def21: for x being bag of n holds it.x = p.x+q.x; existence proof deffunc F(Element of Bags n) = p.$1+q.$1; consider f being Function of Bags n, the carrier of L such that A1: for x being Element of Bags n holds f.x = F(x) from LambdaD; reconsider f as Function of Bags n, L; reconsider f as Series of n, L; take f; let x be bag of n; x in Bags n by Def14; hence thesis by A1; end; uniqueness proof let it1, it2 be Series of n, L such that A2: for x being bag of n holds it1.x = p.x+q.x and A3: for x being bag of n holds it2.x = p.x+q.x; now let x be Element of Bags n; reconsider x' = x as bag of n; thus it1.x = p.x'+q.x' by A2 .= it2.x by A3; end; hence it1 = it2 by FUNCT_2:113; end; end; theorem Th79: for n being set, L being right_zeroed (non empty LoopStr), p, q being Series of n, L holds Support (p+q) c= Support p \/ Support q proof let n be set, L be right_zeroed (non empty LoopStr), p, q be Series of n, L; set f = p+q, Sp = Support p, Sq = Support q; let x be set; assume A1: x in Support f; then reconsider x' = x as Element of Bags n; f.x' <> 0.L by A1,Def9; then p.x'+q.x' <> 0.L by Def21; then not(p.x' = 0.L & q.x' = 0.L) by RLVECT_1:def 7; then x' in Sp or x' in Sq by Def9; hence x in Sp \/ Sq by XBOOLE_0:def 2; end; definition let n be set, L be Abelian right_zeroed (non empty LoopStr), p, q be Series of n, L; redefine func p+q; commutativity proof let p, q be Series of n, L; now let b be Element of Bags n; thus (p + q).b = q.b + p.b by Def21 .= (q + p).b by Def21; end; hence p+q = q+p by FUNCT_2:113; end; end; theorem Th80: for n being set, L being add-associative right_zeroed (non empty doubleLoopStr), p, q, r being Series of n, L holds (p+q)+r = p+(q+r) proof let n be set, L be add-associative right_zeroed (non empty doubleLoopStr), p, q, r be Series of n, L; now let b be Element of Bags n; thus ((p+q)+r).b = (p+q).b+r.b by Def21 .= p.b+q.b+r.b by Def21 .= p.b+(q.b+r.b) by RLVECT_1:def 6 .= p.b+(q+r).b by Def21 .= (p+(q+r)).b by Def21; end; hence (p+q)+r = p+(q+r) by FUNCT_2:113; end; definition let n be set, L be add-associative right_zeroed right_complementable (non empty LoopStr), p be Series of n, L; func -p -> Series of n, L means :Def22: for x being bag of n holds it.x = -(p.x); existence proof deffunc F(Element of Bags n) = -(p.$1); consider f being Function of Bags n, the carrier of L such that A1: for x being Element of Bags n holds f.x = F(x) from LambdaD; reconsider f as Function of Bags n, L; reconsider f as Series of n, L; take f; let x be bag of n; x in Bags n by Def14; hence thesis by A1; end; uniqueness proof let it1, it2 be Series of n, L such that A2: for x being bag of n holds it1.x = -(p.x) and A3: for x being bag of n holds it2.x = -(p.x); now let b be Element of Bags n; thus it1.b = -(p.b) by A2 .= it2.b by A3; end; hence it1 = it2 by FUNCT_2:113; end; involutiveness proof let p,q be Series of n, L such that A4: for x being bag of n holds p.x = -(q.x); let x be bag of n; thus q.x = --(q.x) by RLVECT_1:30 .= -(p.x) by A4; end; end; definition let n be set, L be add-associative right_zeroed right_complementable (non empty LoopStr), p, q be Series of n, L; func p-q -> Series of n, L equals :Def23: p+-q; coherence; end; definition let n be set, S be non empty ZeroStr; func 0_(n, S) -> Series of n, S equals :Def24: (Bags n) --> 0.S; coherence by FUNCOP_1:57; end; theorem Th81: for n being set, S being non empty ZeroStr, b be bag of n holds (0_(n, S)).b = 0.S proof let n be set, S be non empty ZeroStr, b be bag of n; A1: 0_(n, S) = (Bags n) --> 0.S by Def24; b in Bags n by Def14; hence (0_(n, S)).b = 0.S by A1,FUNCOP_1:13; end; theorem Th82: for n being set, L be right_zeroed (non empty LoopStr), p be Series of n, L holds p+0_(n,L) = p proof let n be set, L be right_zeroed (non empty LoopStr), p be Series of n, L; reconsider ls = p+0_(n,L), p' = p as Function of (Bags n), the carrier of L; now let b be Element of Bags n; thus ls.b = p.b + 0_(n,L).b by Def21 .= p'.b+0.L by Th81 .= p'.b by RLVECT_1:def 7; end; hence p+0_(n,L) = p by FUNCT_2:113; end; definition let n be set, L be unital (non empty multLoopStr_0); func 1_(n,L) -> Series of n, L equals :Def25: 0_(n,L)+*(EmptyBag n,1.L); coherence; end; theorem Th83: for n being set, L being add-associative right_zeroed right_complementable (non empty LoopStr), p being Series of n, L holds p-p = 0_(n,L) proof let n be set, L be add-associative right_zeroed right_complementable (non empty LoopStr), p be Series of n, L; reconsider pp = p-p, Z = 0_(n,L) as Function of Bags n, the carrier of L; now let b be Element of Bags n; thus pp.b = (p+-p).b by Def23 .= p.b+(-p).b by Def21 .= p.b + -p.b by Def22 .= 0.L by RLVECT_1:def 10 .= Z.b by Th81; end; hence p-p = 0_(n,L) by FUNCT_2:113; end; theorem Th84: for n being set, L being unital (non empty multLoopStr_0) holds (1_(n,L)).EmptyBag n = 1.L & for b being bag of n st b <> EmptyBag n holds (1_(n,L)).b = 0.L proof let n be set, L be unital (non empty multLoopStr_0); set Z = 0_(n,L); A1: Z = (Bags n --> 0.L) by Def24; then A2: dom Z = Bags n by FUNCOP_1:19; A3: Z+*(EmptyBag n,1.L) = 1_(n,L) by Def25; hence (1_(n,L)).EmptyBag n = 1.L by A2,FUNCT_7:33; let b be bag of n; assume A4: b <> EmptyBag n; A5: b in Bags n by Def14; thus (1_(n,L)).b = Z.b by A3,A4,FUNCT_7:34 .= 0.L by A1,A5,FUNCOP_1:13; end; definition let n be Ordinal, L be add-associative right_complementable right_zeroed (non empty doubleLoopStr), p, q be Series of n, L; func p*'q -> Series of n, L means :Def26: for b being bag of n ex s being FinSequence of the carrier of L st it.b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2; existence proof defpred P[Element of Bags n, Element of L] means ex b being bag of n st b = $1 & ex s being FinSequence of the carrier of L st $2 = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2; A1: now let bb be Element of Bags n; reconsider b = bb as bag of n; defpred Q[Nat, set] means ex b1, b2 being bag of n st (decomp b)/.$1 = <*b1, b2*> & $2 = p.b1*q.b2; A2: now let k be Nat; assume k in Seg len decomp b; then k in dom decomp b by FINSEQ_1:def 3; then consider b1, b2 being bag of n such that A3: (decomp b)/.k = <*b1,b2*> and b = b1+b2 by Th72; reconsider x = p.b1*q.b2 as Element of L; take x; thus Q[k,x] by A3; end; consider s being FinSequence of the carrier of L such that A4: len s = len decomp b and A5: for k being Nat st k in Seg len decomp b holds Q[k, s/.k] from FinSeqDChoice (A2); reconsider y = Sum s as Element of L; take y; thus P[bb,y] proof take b; thus b = bb; take s; thus y = Sum s; thus len s = len decomp b by A4; let k be Nat; assume k in dom s; then k in Seg len decomp b by A4,FINSEQ_1:def 3; hence ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by A5; end; end; consider P being Function of (Bags n), the carrier of L such that A6: for b being Element of Bags n holds P[b, P.b] from FuncExD(A1); reconsider P as Function of (Bags n), L; reconsider P as Series of n, L; take P; let b be bag of n; reconsider bb = b as Element of Bags n by Def14; P[bb, P.bb] by A6; hence thesis; end; uniqueness proof let it1, it2 be Series of n, L such that A7: for b being bag of n ex s being FinSequence of the carrier of L st it1.b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 and A8: for b being bag of n ex s being FinSequence of the carrier of L st it2.b = Sum s & len s = len decomp b & for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2; reconsider ita = it1, itb = it2 as Function of (Bags n), the carrier of L; now let b be Element of Bags n; consider sa being FinSequence of the carrier of L such that A9: ita.b = Sum sa and A10: len sa = len decomp b and A11: for k being Nat st k in dom sa ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & sa/.k = p.b1*q.b2 by A7; consider sb being FinSequence of the carrier of L such that A12: itb.b = Sum sb and A13: len sb = len decomp b and A14: for k being Nat st k in dom sb ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & sb/.k = p.b1*q.b2 by A8; now let k be Nat; assume A15: 1 <= k & k <= len sa; then A16: k in dom sa by FINSEQ_3:27; then consider ab1, ab2 being bag of n such that A17: (decomp b)/.k = <*ab1, ab2*> and A18: sa/.k = p.ab1*q.ab2 by A11; A19: k in dom sb by A10,A13,A15,FINSEQ_3:27; then consider bb1, bb2 being bag of n such that A20: (decomp b)/.k = <*bb1, bb2*> and A21: sb/.k = p.bb1*q.bb2 by A14; A22: sa/.k = sa.k & sb/.k = sb.k by A16,A19,FINSEQ_4:def 4; ab1 = bb1 & ab2 = bb2 by A17,A20,GROUP_7:2; hence sa.k = sb.k by A18,A21,A22; end; hence ita.b = itb.b by A9,A10,A12,A13,FINSEQ_1:18; end; hence it1 = it2 by FUNCT_2:113; end; end; theorem Th85: for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable distributive associative (non empty doubleLoopStr), p, q, r being Series of n, L holds p*'(q+r) = p*'q+p*'r proof let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable distributive associative (non empty doubleLoopStr), p, q, r be Series of n, L; set cL = the carrier of L; now let b be Element of Bags n; consider s being FinSequence of cL such that A1: (p*'(q+r)).b = Sum s and A2: len s = len decomp b and A3: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*(q+r).b2 by Def26; consider t being FinSequence of cL such that A4: (p*'q).b = Sum t and A5: len t = len decomp b and A6: for k being Nat st k in dom t ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & t/.k = p.b1*q.b2 by Def26; consider u being FinSequence of cL such that A7: (p*'r).b = Sum u and A8: len u = len decomp b and A9: for k being Nat st k in dom u ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & u/.k = p.b1*r.b2 by Def26; reconsider S = s, t, u as Element of (len s)-tuples_on cL by A2,A5,A8,FINSEQ_2:110; A10: dom t = dom s & dom u = dom s by A2,A5,A8,FINSEQ_3:31; then A11: dom (t+u) = dom s by Th5; then A12: len (t+u) = len s by FINSEQ_3:31; now let i be Nat; assume i in Seg len S; then 1 <= i & i <= len s by FINSEQ_1:3; then A13: i in dom s by FINSEQ_3:27; then consider sb1, sb2 being bag of n such that A14: (decomp b)/.i = <*sb1, sb2*> & s/.i = p.sb1*(q+r).sb2 by A3; consider tb1, tb2 being bag of n such that A15: (decomp b)/.i = <*tb1, tb2*> & t/.i = p.tb1*q.tb2 by A6,A10,A13; consider ub1, ub2 being bag of n such that A16: (decomp b)/.i = <*ub1, ub2*> & u/.i = p.ub1*r.ub2 by A9,A10,A13; A17: sb1 = tb1 & sb1 = ub1 & sb2 = tb2 & sb2 = ub2 by A14,A15,A16,GROUP_7:2; A18: s/.i = s.i & t/.i = t.i & u/.i = u.i by A10,A13,FINSEQ_4:def 4; hence s.i = p.sb1*(q.sb2+r.sb2) by A14,Def21 .= p.sb1*q.sb2+p.sb1*r.sb2 by VECTSP_1:def 18 .= (t + u).i by A11,A13,A15,A16,A17,A18,FVSUM_1:21; end; then s = t + u by A12,FINSEQ_2:10; hence (p*'(q+r)).b = Sum t + Sum u by A1,FVSUM_1:95 .= (p*'q+p*'r).b by A4,A7,Def21; end; hence p*'(q+r) = p*'q+p*'r by FUNCT_2:113; end; theorem Th86: for n being Ordinal, L being Abelian add-associative right_zeroed right_complementable unital distributive associative (non empty doubleLoopStr), p, q, r being Series of n, L holds (p*'q)*'r = p*'(q*'r) proof let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable unital distributive associative (non empty doubleLoopStr), p, q, r be Series of n, L; set cL = the carrier of L; reconsider pq_r = (p*'q)*'r, p_qr = p*'(q*'r) as Function of Bags n, cL; set pq = p*'q, qr = q*'r; now let b be Element of Bags n; set db = decomp b; consider ls being FinSequence of cL such that A1: pq_r.b = Sum ls and A2: len ls = len decomp b and A3: for k being Nat st k in dom ls ex b1,b2 being bag of n st db/.k = <*b1,b2*> & ls/.k = pq.b1*r.b2 by Def26; consider rs being FinSequence of cL such that A4: p_qr.b = Sum rs and A5: len rs = len decomp b and A6: for k being Nat st k in dom rs ex b1,b2 being bag of n st db/.k = <*b1,b2*> & rs/.k = p.b1*qr.b2 by Def26; deffunc F(Nat) = ((decomp (((db/.$1)/.1) qua Element of Bags n))) ^^ ((len (decomp (((db/.$1)/.1) qua Element of Bags n)))|-> <*(db/.$1)/.2*>); consider dbl being FinSequence such that A7: len dbl = len db and A8: for k being Nat st k in dom dbl holds dbl.k = F(k) from domSeqLambda; deffunc G(Nat) = ((len (decomp (((db/.$1)/.2) qua Element of Bags n))) |-> <*(db/.$1)/.1*>) ^^ ((decomp (((db/.$1)/.2) qua Element of Bags n))); consider dbr being FinSequence such that A9: len dbr = len db and A10: for k being Nat st k in dom dbr holds dbr.k = G(k) from domSeqLambda; A11: rng dbl c= (3-tuples_on Bags n)* proof let y be set; assume y in rng dbl; then consider k being set such that A12: k in dom dbl & y = dbl.k by FUNCT_1:def 5; set ddbk1 = decomp (((db/.k)/.1) qua Element of Bags n); set dbk2 = (db/.k)/.2; set dblk = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>); A13: dbl.k = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>) by A8,A12; A14: dom dblk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by MATRLIN:def 2 .= dom ddbk1 /\ Seg len ddbk1 by FINSEQ_2:68 .= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3 .= dom ddbk1; A15: rng ddbk1 c= 2-tuples_on Bags n by FINSEQ_1:def 4; A16: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3; rng dblk c= 3-tuples_on Bags n proof let y be set; assume y in rng dblk; then consider i being set such that A17: i in dom dblk & dblk.i = y by FUNCT_1:def 5; ddbk1.i in rng ddbk1 by A14,A17,FUNCT_1:def 5; then reconsider Fi = ddbk1.i as Element of 2-tuples_on Bags n by A15; reconsider i' = i as Nat by A17; A18: ((len ddbk1) |-> <*dbk2*>).i' = <*dbk2*> by A14,A16,A17,FINSEQ_2:70; reconsider Gi = <*dbk2*> as Element of 1-tuples_on Bags n; y = Fi^Gi by A17,A18,MATRLIN:def 2; hence y in 3-tuples_on Bags n; end; then dblk is FinSequence of 3-tuples_on Bags n by FINSEQ_1:def 4; hence y in (3-tuples_on Bags n)* by A12,A13,FINSEQ_1:def 11; end; rng dbr c= (3-tuples_on Bags n)* proof let y be set; assume y in rng dbr; then consider k being set such that A19: k in dom dbr & y = dbr.k by FUNCT_1:def 5; set ddbk1 = decomp (((db/.k)/.2) qua Element of Bags n); set dbk2 = (db/.k)/.1; set dbrk = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1; A20: dbr.k = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1 by A10,A19; A21: dom dbrk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by MATRLIN:def 2 .= dom ddbk1 /\ Seg len ddbk1 by FINSEQ_2:68 .= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3 .= dom ddbk1; A22: rng ddbk1 c= 2-tuples_on Bags n by FINSEQ_1:def 4; A23: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3; rng dbrk c= 3-tuples_on Bags n proof let y be set; assume y in rng dbrk; then consider i being set such that A24: i in dom dbrk & dbrk.i = y by FUNCT_1:def 5; ddbk1.i in rng ddbk1 by A21,A24,FUNCT_1:def 5; then reconsider Fi = ddbk1.i as Element of 2-tuples_on Bags n by A22; reconsider i' = i as Nat by A24; A25: ((len ddbk1) |-> <*dbk2*>).i' = <*dbk2*> by A21,A23,A24,FINSEQ_2:70; reconsider Gi = <*dbk2*> as Element of 1-tuples_on Bags n; y = Gi^Fi by A24,A25,MATRLIN:def 2; hence y in 3-tuples_on Bags n; end; then dbrk is FinSequence of 3-tuples_on Bags n by FINSEQ_1:def 4; hence y in (3-tuples_on Bags n)* by A19,A20,FINSEQ_1:def 11; end; then reconsider dbl, dbr as FinSequence of (3-tuples_on Bags n)* by A11, FINSEQ_1:def 4; deffunc F(Element of 3-tuples_on Bags n) = p.($1/.1)*q.($1/.2)*r.($1/.3); consider v being Function of (3-tuples_on Bags n), cL such that A26: for b being Element of 3-tuples_on Bags n holds v.b = F(b) from LambdaD; A27: dom v = 3-tuples_on Bags n by FUNCT_2:def 1; set fdbl = FlattenSeq dbl, fdbr = FlattenSeq dbr; reconsider vfdbl = v*fdbl,vfdbr = v*fdbr as FinSequence of cL by FINSEQ_2:36; consider vdbl being FinSequence of cL* such that A28: vdbl = ((dom dbl --> v)**dbl) and A29: vfdbl = FlattenSeq vdbl by Th36; A30: Sum vfdbl = Sum Sum vdbl by A29,Th34; now set f = Sum vdbl; A31: dom f = dom vdbl by Th15; A32: dom vdbl = dom (dom dbl --> v) /\ dom dbl by A28,MSUALG_3:def 4 .= dom dbl /\ dom dbl by FUNCOP_1:19 .= dom dbl; hence len Sum vdbl = len ls by A2,A7,A31,FINSEQ_3:31; let k be Nat such that A33: 1 <= k & k <= len ls; A34: dom ls = dom f by A2,A7,A31,A32,FINSEQ_3:31; A35: k in dom f by A2,A7,A31,A32,A33,FINSEQ_3:27; then consider b1,b2 being bag of n such that A36: db/.k = <*b1,b2*> and A37: ls/.k = pq.b1*r.b2 by A3,A34; reconsider b2' = b2 as Element of Bags n by Def14; consider pqs being FinSequence of the carrier of L such that A38: pq.b1 = Sum pqs and A39: len pqs = len decomp b1 and A40: for i being Nat st i in dom pqs ex b11, b12 being bag of n st (decomp b1)/.i = <*b11, b12*> & pqs/.i = p.b11*q.b12 by Def26; A41: Sum (pqs*r.b2) = (Sum pqs)*r.b2 by Th29; A42: k in dom vdbl by A2,A7,A32,A33,FINSEQ_3:27; set vdblk = v*(dbl.k); set ddbk1 = decomp (((db/.k)/.1) qua Element of Bags n); set dbk2 = (db/.k)/.2; len <*b1,b2*> = 2 by FINSEQ_1:61; then A43: 1 in dom <*b1,b2*> & 2 in dom <*b1,b2*> by FINSEQ_3:27; then A44: dbk2 = <*b1,b2*>.2 by A36,FINSEQ_4:def 4 .= b2 by FINSEQ_1:61; A45: (db/.k)/.1 = <*b1,b2*>.1 by A36,A43,FINSEQ_4:def 4 .= b1 by FINSEQ_1:61; A46: dbl.k = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>) by A8,A32,A42; set dblk = dbl.k; A47: dom dblk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by A46,MATRLIN:def 2 .= dom ddbk1 /\ Seg len ddbk1 by FINSEQ_2:68 .= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3 .= dom ddbk1; k in dom dbl by A2,A7,A33,FINSEQ_3:27; then A48: dblk in rng dbl by FUNCT_1:def 5; rng dbl c= (3-tuples_on Bags n)* by FINSEQ_1:def 4; then dblk is Element of (3-tuples_on Bags n)* by A48; then reconsider dblk as FinSequence of 3-tuples_on Bags n; A49: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3; rng dblk c= 3-tuples_on Bags n by FINSEQ_1:def 4; then A50: dom vdblk = dom dblk by A27,RELAT_1:46; then dom vdblk = Seg len ddbk1 by A47,FINSEQ_1:def 3; then reconsider vdblk as FinSequence by FINSEQ_1:def 2; A51: dom pqs = dom (pqs*r.b2) by Def3; now thus len vdblk = len pqs by A39,A45,A47,A50,FINSEQ_3:31 .= len (pqs*r.b2) by A51,FINSEQ_3:31; then A52: dom vdblk = dom (pqs*r.b2) by FINSEQ_3:31; let i be Nat; assume A53: 1 <= i & i <= len (pqs*r.b2); then A54: i in dom (pqs*r.b2) by FINSEQ_3:27; then consider b11, b12 being bag of n such that A55: (decomp b1)/.i = <*b11, b12*> and A56: pqs/.i = p.b11*q.b12 by A40,A51; reconsider i' = i as Nat; A57: ((len ddbk1) |-> <*dbk2*>).i' = <*dbk2*> by A47,A49,A50,A52,A54,FINSEQ_2:70; (decomp b1)/.i = (decomp b1).i by A45,A47,A50,A52,A54,FINSEQ_4:def 4; then A58: dblk.i = <*b11,b12*>^<*b2*> by A44,A45,A46,A50,A52,A54,A55,A57,MATRLIN:def 2 .= <*b11,b12,b2*> by FINSEQ_1:60; reconsider b11' = b11, b12' = b12 as Element of Bags n by Def14; reconsider B = <*b11',b12',b2'*> as Element of 3-tuples_on Bags n by FINSEQ_2:124; A59: i in dom pqs by A51,A53,FINSEQ_3:27; A60: dom pqs = dom (pqs*r.b2) by Def3; thus (v*(dbl.k)).i = v.(dblk.i) by A52,A54,FUNCT_1:22 .= p.(B/.1)*q.(B/.2)*r.(B/.3) by A26,A58 .= p.b11'*q.(B/.2)*r.(B/.3) by FINSEQ_4:27 .= p.b11*q.b12*r.(B/.3) by FINSEQ_4:27 .= (pqs/.i)*r.b2 by A56,FINSEQ_4:27 .= (pqs*r.b2)/.i by A59,Def3 .= (pqs*r.b2).i by A59,A60,FINSEQ_4:def 4; end; then A61: vdblk = pqs*r.b2 by FINSEQ_1:18; A62: vdbl/.k = vdbl.k by A42,FINSEQ_4:def 4 .= ((dom dbl --> v).k)*(dbl.k) by A28,A42,MSUALG_3:def 4 .= pqs*r.b2 by A32,A42,A61,FUNCOP_1:13; A63: ls/.k = ls.k by A34,A35,FINSEQ_4:def 4; f/.k = f.k by A35,FINSEQ_4:def 4; hence (Sum vdbl).k = ls.k by A35,A37,A38,A41,A62,A63,MATRLIN:def 8; end; then A64: Sum vdbl = ls by FINSEQ_1:18; consider vdbr being FinSequence of cL* such that A65: vdbr = ((dom dbr --> v)**dbr) and A66: vfdbr = FlattenSeq vdbr by Th36; A67: Sum vfdbr = Sum Sum vdbr by A66,Th34; now set f = Sum vdbr; A68: dom f = dom vdbr by Th15; A69: dom vdbr = dom (dom dbr --> v) /\ dom dbr by A65,MSUALG_3:def 4 .= dom dbr /\ dom dbr by FUNCOP_1:19 .= dom dbr; hence len Sum vdbr = len rs by A5,A9,A68,FINSEQ_3:31; let k be Nat such that A70: 1 <= k & k <= len rs; A71: dom rs = dom f by A5,A9,A68,A69,FINSEQ_3:31; A72: k in dom f by A5,A9,A68,A69,A70,FINSEQ_3:27; then consider b1,b2 being bag of n such that A73: db/.k = <*b1,b2*> and A74: rs/.k = p.b1*qr.b2 by A6,A71; reconsider b1' = b1 as Element of Bags n by Def14; consider qrs being FinSequence of the carrier of L such that A75: qr.b2 = Sum qrs and A76: len qrs = len decomp b2 and A77: for i being Nat st i in dom qrs ex b11, b12 being bag of n st (decomp b2)/.i = <*b11, b12*> & qrs/.i = q.b11*r.b12 by Def26; A78: Sum (p.b1*qrs) = p.b1*(Sum qrs) by Th28; A79: k in dom vdbr by A5,A9,A69,A70,FINSEQ_3:27; set vdbrk = v*(dbr.k); set ddbk1 = decomp (((db/.k)/.2) qua Element of Bags n); set dbk2 = (db/.k)/.1; len <*b1,b2*> = 2 by FINSEQ_1:61; then A80: 1 in dom <*b1,b2*> & 2 in dom <*b1,b2*> by FINSEQ_3:27; then A81: dbk2 = <*b1,b2*>.1 by A73,FINSEQ_4:def 4 .= b1 by FINSEQ_1:61; A82: (db/.k)/.2 = <*b1,b2*>.2 by A73,A80,FINSEQ_4:def 4 .= b2 by FINSEQ_1:61; A83: dbr.k = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1 by A10,A69,A79; set dbrk = dbr.k; A84: dom dbrk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by A83,MATRLIN:def 2 .= dom ddbk1 /\ Seg len ddbk1 by FINSEQ_2:68 .= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3 .= dom ddbk1; k in dom dbr by A5,A9,A70,FINSEQ_3:27; then A85: dbrk in rng dbr by FUNCT_1:def 5; rng dbr c= (3-tuples_on Bags n)* by FINSEQ_1:def 4; then dbrk is Element of (3-tuples_on Bags n)* by A85; then reconsider dbrk as FinSequence of 3-tuples_on Bags n; A86: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3; rng dbrk c= 3-tuples_on Bags n by FINSEQ_1:def 4; then A87: dom vdbrk = dom dbrk by A27,RELAT_1:46; then dom vdbrk = Seg len ddbk1 by A84,FINSEQ_1:def 3; then reconsider vdbrk as FinSequence by FINSEQ_1:def 2; A88: dom qrs = dom (p.b1*qrs) by Def2; then A89: len qrs = len (p.b1*qrs) by FINSEQ_3:31; then A90: len vdbrk = len (p.b1*qrs) by A76,A82,A84,A87,FINSEQ_3:31; A91: dom vdbrk = dom (p.b1*qrs) by A76,A82,A84,A87,A88,FINSEQ_3:31; now let i be Nat; assume A92: 1 <= i & i <= len (p.b1*qrs); then A93: i in dom dbrk by A76,A82,A84,A89,FINSEQ_3:27; then consider b11, b12 being bag of n such that A94: (decomp b2)/.i = <*b11, b12*> and A95: qrs/.i = q.b11*r.b12 by A77,A87,A88,A91; reconsider i' = i as Nat; A96: ((len ddbk1) |-> <*dbk2*>).i' = <*dbk2*> by A84,A86,A93,FINSEQ_2:70; (decomp b2)/.i = (decomp b2).i by A82,A84,A93,FINSEQ_4:def 4; then A97: dbrk.i = <*b1*>^<*b11,b12*> by A81,A82,A83,A93,A94,A96, MATRLIN:def 2 .= <*b1,b11,b12*> by FINSEQ_1:60; reconsider b11' = b11, b12' = b12 as Element of Bags n by Def14; reconsider B = <*b1',b11',b12'*> as Element of 3-tuples_on Bags n by FINSEQ_2:124; A98: i in dom qrs by A88,A92,FINSEQ_3:27; thus (v*(dbr.k)).i = v.(dbrk.i) by A87,A93,FUNCT_1:22 .= p.(B/.1)*q.(B/.2)*r.(B/.3) by A26,A97 .= p.b1*q.(B/.2)*r.(B/.3) by FINSEQ_4:27 .= p.b1*q.b11*r.(B/.3) by FINSEQ_4:27 .= p.b1*q.b11*r.b12 by FINSEQ_4:27 .= p.b1*(qrs/.i) by A95,VECTSP_1:def 16 .= (p.b1*qrs)/.i by A98,Def2 .= (p.b1*qrs).i by A88,A98,FINSEQ_4:def 4; end; then A99: vdbrk = p.b1*qrs by A90,FINSEQ_1:18; A100: vdbr/.k = vdbr.k by A79,FINSEQ_4:def 4 .= ((dom dbr --> v).k)*(dbr.k) by A65,A79,MSUALG_3:def 4 .= p.b1*qrs by A69,A79,A99,FUNCOP_1:13; A101: rs/.k = rs.k by A71,A72,FINSEQ_4:def 4; f/.k = f.k by A72,FINSEQ_4:def 4; hence (Sum vdbr).k = rs.k by A72,A74,A75,A78,A100,A101,MATRLIN:def 8; end; then A102: Sum vdbr = rs by FINSEQ_1:18; dom dbl = dom db & dom dbr = dom db by A7,A9,FINSEQ_3:31; then consider P being Permutation of dom fdbl such that A103: fdbr = fdbl*P by A8,A10,Th78; rng fdbl c= 3-tuples_on Bags n by FINSEQ_1:def 4; then dom vfdbl = dom fdbl by A27,RELAT_1:46; then reconsider P as Permutation of dom (vfdbl); vfdbr = vfdbl*P by A103,RELAT_1:55; hence pq_r.b = p_qr.b by A1,A4,A30,A64,A67,A102,RLVECT_2:9; end; hence (p*'q)*'r = p*'(q*'r) by FUNCT_2:113; end; definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative (non empty doubleLoopStr), p, q be Series of n, L; redefine func p*'q; commutativity proof let p, q be Series of n, L; reconsider pq = p*'q, qp = q*'p as Function of Bags n, the carrier of L; now let b be Element of Bags n; consider s being FinSequence of the carrier of L such that A1: pq.b = Sum s and A2: len s = len decomp b and A3: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by Def26; consider t being FinSequence of the carrier of L such that A4: qp.b = Sum t and A5: len t = len decomp b and A6: for k being Nat st k in dom t ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & t/.k = q.b1*p.b2 by Def26; A7: dom s = dom decomp b & dom t = dom decomp b by A2,A5,FINSEQ_3:31; then reconsider ds = dom s as non empty set; defpred P[set, set] means ex b1, b2 being bag of n st (decomp b).$1 = <*b1, b2*> & (decomp b).$2 = <*b2, b1*>; A8: now let e be set; assume A9: e in ds; then consider b1, b2 being bag of n such that A10: (decomp b)/.e = <*b1, b2*> and A11: b = b1+b2 by A7,Th72; consider d being Nat such that A12: d in dom decomp b and A13: (decomp b)/.d = <*b2,b1*> by A11,Th73; reconsider d as set; take d; thus d in ds by A2,A12,FINSEQ_3:31; thus P[e,d] proof take b1, b2; thus (decomp b).e = <*b1, b2*> & (decomp b).d = <*b2, b1*> by A7,A9,A10,A12,A13,FINSEQ_4:def 4; end; end; consider f being Function of ds, ds such that A14: for e being set st e in ds holds P[e,f.e] from FuncEx1(A8); A15: dom f = ds & rng f c= ds by FUNCT_2:def 1,RELSET_1:12; A16: f is one-to-one proof let x1, x2 be set such that A17: x1 in dom f and A18: x2 in dom f and A19: f.x1 = f.x2; consider b1, b2 being bag of n such that A20: (decomp b).x1 = <*b1, b2*> & (decomp b).(f.x1) = <*b2, b1*> by A14,A17; consider b3, b4 being bag of n such that A21: (decomp b).x2 = <*b3, b4*> & (decomp b).(f.x2) = <*b4, b3*> by A14,A18 ; b2 = b4 & b1 = b3 by A19,A20,A21,GROUP_7:2; hence x1 = x2 by A7,A17,A18,A20,A21,FUNCT_1:def 8; end; ds c= rng f proof let x be set; assume A22: x in ds; then A23: f.x in rng f by A15,FUNCT_1:def 5; then A24: f.(f.x) in rng f by A15,FUNCT_1:def 5; consider b1, b2 being bag of n such that A25: (decomp b).x = <*b1, b2*> & (decomp b).(f.x) = <*b2, b1*> by A14,A22; consider b3, b4 being bag of n such that A26: (decomp b).(f.x) = <*b3, b4*> & (decomp b).(f.(f.x)) = <*b4, b3*> by A14,A15,A23; b3 = b2 & b4 = b1 by A25,A26,GROUP_7:2; hence x in rng f by A7,A15,A22,A24,A25,A26,FUNCT_1:def 8; end; then rng f = ds by A15,XBOOLE_0:def 10; then reconsider f as Permutation of dom s by A16,FUNCT_2:83; now let i be Nat; assume A27: i in dom t; then A28: f.i in rng f by A7,A15,FUNCT_1:def 5; then f.i in ds by A15; then reconsider fi = f.i as Nat; consider b1, b2 being bag of n such that A29: (decomp b)/.i = <*b1, b2*> & t/.i = q.b1*p.b2 by A6,A27; consider b3, b4 being bag of n such that A30: (decomp b)/.fi = <*b3, b4*> & s/.fi = p.b3*q.b4 by A3,A15,A28; consider b5, b6 being bag of n such that A31: (decomp b).i = <*b5, b6*> & (decomp b).(f.i) = <*b6, b5*> by A7,A14, A27; A32: dom s = dom t by A2,A5,FINSEQ_3:31; A33: t/.i = t.i & s/.fi = s.fi by A15,A27,A28,FINSEQ_4:def 4; dom s = dom decomp b by A2,FINSEQ_3:31; then (decomp b)/.i = (decomp b).i & (decomp b)/.fi = (decomp b).fi by A15,A27,A28,A32,FINSEQ_4:def 4; then b1 = b5 & b2 = b6 & b3 = b6 & b4 = b5 by A29,A30,A31,GROUP_7:2; hence t.i = s.(f.i) by A29,A30,A33,VECTSP_1:def 17; end; hence pq.b = qp.b by A1,A2,A4,A5,RLVECT_2:8; end; hence p*'q = q*'p by FUNCT_2:113; end; end; theorem for n being Ordinal, L being add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p being Series of n, L holds p*'0_(n,L) = 0_(n,L) proof let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p be Series of n, L; set Z = 0_(n,L); now let b be Element of Bags n; consider s being FinSequence of the carrier of L such that A1: (p*'Z).b = Sum s and len s = len decomp b and A2: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*Z.b2 by Def26; now let k be Nat; assume k in dom s; then consider b1, b2 being bag of n such that (decomp b)/.k = <*b1, b2*> and A3: s/.k = p.b1*Z.b2 by A2; thus s/.k = p.b1*0.L by A3,Th81 .= 0.L by VECTSP_1:36; end; then Sum s = 0.L by MATRLIN:15; hence (p*'Z).b = Z.b by A1,Th81; end; hence p*'0_(n,L) = 0_(n,L) by FUNCT_2:113; end; theorem Th88: for n being Ordinal, L being add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p being Series of n, L holds p*'1_(n,L) = p proof let n be Ordinal, L be add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p be Series of n, L; set O = 1_(n,L), cL = the carrier of L; now let b be Element of Bags n; consider s being FinSequence of cL such that A1: (p*'O).b = Sum s and A2: len s = len decomp b and A3: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*O.b2 by Def26; A4: len s <> 0 by A2,FINSEQ_1:25; then consider t being FinSequence of cL, s1 being Element of cL such that A5: s = t^<*s1*> by FINSEQ_2:22; A6: Sum s = (Sum t) + (Sum <*s1*>) by A5,RLVECT_1:58; s is non empty by A4,FINSEQ_1:25; then A7: len s in dom s by FINSEQ_5:6; then consider b1, b2 being bag of n such that A8: (decomp b)/.len s = <*b1, b2*> and A9: s/.len s = p.b1*O.b2 by A3; (decomp b)/.len s = <*b, EmptyBag n*> by A2,Th75; then A10: b1 = b & b2 = EmptyBag n by A8,GROUP_7:2; A11: s.len s = (t^<*s1*>).(len t +1) by A5,FINSEQ_2:19 .= s1 by FINSEQ_1:59; A12: s/.len s = s.len s by A7,FINSEQ_4:def 4; A13: Sum <*s1*> = s1 by RLVECT_1:61 .= p.b*1.L by A9,A10,A11,A12,Th84 .= p.b by GROUP_1:def 4; now per cases; suppose t = <*>(cL); hence (Sum t) = 0.L by RLVECT_1:60; suppose A14: t <> <*>(cL); now let k be Nat; assume A15: k in dom t; then A16: t/.k = t.k by FINSEQ_4:def 4 .= s.k by A5,A15,FINSEQ_1:def 7; A17: 1 <= k by A15,FINSEQ_3:27; A18: dom s = dom decomp b by A2,FINSEQ_3:31; A19: len s = len t + len <*s1*> by A5,FINSEQ_1:35 .= len t +1 by FINSEQ_1:56; k <= len t by A15,FINSEQ_3:27; then A20: k < len s by A19,NAT_1:38; then A21: k in dom decomp b by A2,A17,FINSEQ_3:27; then A22: s/.k = s.k by A18,FINSEQ_4:def 4; per cases by A17,AXIOMS:21; suppose A23: 1 < k; consider b1, b2 being bag of n such that A24: (decomp b)/.k = <*b1, b2*> and A25: s/.k = p.b1*O.b2 by A3,A18,A21; b2 <> EmptyBag n by A2,A20,A23,A24,Th76; hence t/.k = p.b1*0.L by A16,A22,A25,Th84 .= 0.L by VECTSP_1:36; suppose A26: k = 1; consider b1, b2 being bag of n such that A27: (decomp b)/.k = <*b1, b2*> and A28: s/.k = p.b1*O.b2 by A3,A18,A21; (decomp b)/.1 = <*EmptyBag n, b*> by Th75; then A29: b1 = EmptyBag n & b2 = b by A26,A27,GROUP_7:2; now assume b = EmptyBag n; then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by Th77; then len t +1 = 0+1 by A2,A19,FINSEQ_1:56; then len t = 0 by XCMPLX_1:2; hence contradiction by A14,FINSEQ_1:25; end; then s.k = (p.EmptyBag n)*0.L by A22,A28,A29,Th84 .= 0.L by VECTSP_1:36; hence t/.k = 0.L by A16; end; hence (Sum t) = 0.L by MATRLIN:15; end; hence (p*'O).b = p.b by A1,A6,A13,RLVECT_1:10; end; hence p*'1_(n,L) = p by FUNCT_2:113; end; theorem Th89: for n being Ordinal, L being add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p being Series of n, L holds 1_(n,L)*'p = p proof let n be Ordinal, L be add-associative right_complementable right_zeroed distributive unital non trivial (non empty doubleLoopStr), p be Series of n, L; set O = 1_(n,L), cL = the carrier of L; now let b be Element of Bags n; consider s being FinSequence of cL such that A1: (O*'p).b = Sum s and A2: len s = len decomp b and A3: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = O.b1*p.b2 by Def26; A4: len s <> 0 by A2,FINSEQ_1:25; then s is non empty by FINSEQ_1:25; then consider s1 being Element of cL, t being FinSequence of cL such that A5: s1 = s.1 and A6: s = <*s1*>^t by FSM_1:5; A7: Sum s = (Sum <*s1*>) + (Sum t) by A6,RLVECT_1:58; s is non empty by A4,FINSEQ_1:25; then A8: 1 in dom s by FINSEQ_5:6; then consider b1, b2 being bag of n such that A9: (decomp b)/.1 = <*b1, b2*> and A10: s/.1 = O.b1*p.b2 by A3; (decomp b)/.1 = <*EmptyBag n, b*> by Th75; then A11: b2 = b & b1 = EmptyBag n by A9,GROUP_7:2; A12: s/.1 = s.1 by A8,FINSEQ_4:def 4; A13: Sum <*s1*> = s1 by RLVECT_1:61 .= 1.L*p.b by A5,A10,A11,A12,Th84 .= p.b by GROUP_1:def 4; now per cases; suppose t = <*>(cL); hence (Sum t) = 0.L by RLVECT_1:60; suppose A14: t <> <*>(cL); now let k be Nat; assume A15: k in dom t; then A16: t/.k = t.k by FINSEQ_4:def 4 .= s.(k+1) by A6,A15,FSM_1:6; 1 <= k by A15,FINSEQ_3:27; then A17: 1 < k+1 by NAT_1:38; A18: dom s = dom decomp b by A2,FINSEQ_3:31; A19: len s = len t + len <*s1*> by A6,FINSEQ_1:35 .= len t +1 by FINSEQ_1:56; k <= len t by A15,FINSEQ_3:27; then A20: k+1 <= len s by A19,AXIOMS:24; then A21: k+1 in dom decomp b by A2,A17,FINSEQ_3:27; then A22: s/.(k+1) = s.(k+1) by A18,FINSEQ_4:def 4; per cases by A20,AXIOMS:21; suppose A23: k+1 < len s; consider b1, b2 being bag of n such that A24: (decomp b)/.(k+1) = <*b1, b2*> and A25: s/.(k+1) = O.b1*p.b2 by A3,A18,A21; b1 <> EmptyBag n by A2,A17,A23,A24,Th76; hence t/.k = 0.L*p.b2 by A16,A22,A25,Th84 .= 0.L by VECTSP_1:39; suppose A26: k+1 = len s; consider b1, b2 being bag of n such that A27: (decomp b)/.(k+1) = <*b1, b2*> and A28: s/.(k+1) = O.b1*p.b2 by A3,A18,A21; (decomp b)/.len s = <*b,EmptyBag n*> by A2,Th75; then A29: b2 = EmptyBag n & b1 = b by A26,A27,GROUP_7:2; now assume b = EmptyBag n; then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by Th77; then len t +1 = 0+1 by A2,A19,FINSEQ_1:56; then len t = 0 by XCMPLX_1:2; hence contradiction by A14,FINSEQ_1:25; end; then s.(k+1) = 0.L*(p.EmptyBag n) by A22,A28,A29,Th84 .= 0.L by VECTSP_1:39; hence t/.k = 0.L by A16; end; hence (Sum t) = 0.L by MATRLIN:15; end; hence (O*'p).b = p.b by A1,A7,A13,RLVECT_1:10; end; hence 1_(n,L)*'p = p by FUNCT_2:113; end; begin :: Polynomials ---------------------------------------------------------- definition let n be set, S be non empty ZeroStr; cluster finite-Support Series of n, S; existence proof reconsider P = Bags n --> 0.S as Function of Bags n, the carrier of S by FUNCOP_1:57; reconsider P as Function of Bags n, S; reconsider P as Series of n, S; take P; for x being Element of Bags n holds x in {} iff P.x <> 0.S by FUNCOP_1:13 ; then Support P = {}Bags n by Def9; hence Support P is finite; end; end; definition let n be Ordinal, S be non empty ZeroStr; mode Polynomial of n, S is finite-Support Series of n, S; end; definition let n be Ordinal, L be right_zeroed (non empty LoopStr), p, q be Polynomial of n, L; cluster p+q -> finite-Support; coherence proof A1: Support p is finite by Def10; A2: Support q is finite by Def10; set Sp = Support p, Sq = Support q; A3: Sp \/ Sq is finite by A1,A2,FINSET_1:14; Support (p+q) c= Sp \/ Sq by Th79; then Support (p+q) is finite by A3,FINSET_1:13; hence thesis by Def10; end; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable (non empty LoopStr), p be Polynomial of n, L; cluster -p -> finite-Support; coherence proof set f = -p; A1: Support p is finite by Def10; Support f c= Support p proof let x be set; assume A2: x in Support f; then reconsider x' = x as Element of Bags n; f.x' <> 0.L by A2,Def9; then -(p.x') <> 0.L by Def22; then p.x' <> 0.L by RLVECT_1:25; hence x in Support p by Def9; end; then Support f is finite by A1,FINSET_1:13; hence f is finite-Support by Def10; end; end; definition let n be Nat, L be add-associative right_zeroed right_complementable (non empty LoopStr), p, q be Polynomial of n, L; cluster p-q -> finite-Support; coherence proof p-q = p+-q by Def23; hence thesis; end; end; definition let n be Ordinal, S be non empty ZeroStr; cluster 0_(n, S) -> finite-Support; coherence proof set Z = 0_(n, S); now given x being set such that A1: x in Support Z; reconsider x as Element of Bags n by A1; Z = (Bags n) --> 0.S by Def24; then Z.x = 0.S by FUNCOP_1:13; hence contradiction by A1,Def9; end; then Support Z = {} by XBOOLE_0:def 1; hence Z is finite-Support by Def10; end; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable unital right-distributive non trivial (non empty doubleLoopStr); cluster 1_(n,L) -> finite-Support; coherence proof reconsider O = 0_(n,L)+*(EmptyBag n,1.L) as Function of Bags n, the carrier of L; reconsider O' = O as Function of Bags n, L; reconsider O' as Series of n, L; A1: 0_(n, L) = (Bags n) --> 0.L by Def24; A2: 1_(n,L) = 0_(n,L)+*(EmptyBag n,1.L) by Def25; now let x be set; hereby assume A3: x in Support O'; then reconsider x' = x as Element of Bags n; assume x <> EmptyBag n; then O'.x = 0_(n,L).x' by FUNCT_7:34 .= 0.L by A1,FUNCOP_1:13; hence contradiction by A3,Def9; end; assume A4: x = EmptyBag n; dom 0_(n,L) = Bags n by A1,FUNCOP_1:19; then O'.x = 1.L by A4,FUNCT_7:33; then O'.x <> 0.L by Th27; hence x in Support O' by A4,Def9; end; then Support O' = {EmptyBag n} by TARSKI:def 1; hence thesis by A2,Def10; end; end; definition let n be Ordinal, L be add-associative right_complementable right_zeroed unital distributive (non empty doubleLoopStr), p, q be Polynomial of n, L; cluster p*'q -> finite-Support; coherence proof deffunc F(Element of Bags n,Element of Bags n) = $1+$2; set D = { F(b1,b2) where b1, b2 is Element of Bags n : b1 in Support p & b2 in Support q }; A1: Support p is finite by Def10; A2: Support q is finite by Def10; A3: D is finite from CartFin(A1, A2); Support (p*'q) c= D proof let x' be set; assume A4: x' in Support (p*'q); then reconsider b = x' as Element of Bags n; A5: (p*'q).b <> 0.L by A4,Def9; consider s being FinSequence of the carrier of L such that A6: (p*'q).b = Sum s and A7: len s = len decomp b and A8: for k being Nat st k in dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by Def26; consider k being Nat such that A9: k in dom s and A10: s/.k <> 0.L by A5,A6,MATRLIN:15; consider b1, b2 being bag of n such that A11: (decomp b)/.k = <*b1, b2*> and A12: s/.k = p.b1*q.b2 by A8,A9; A13: b1 in Bags n & b2 in Bags n by Def14; p.b1 <> 0.L & q.b2 <> 0.L by A10,A12,VECTSP_1:36,39; then A14: b1 in Support p & b2 in Support q by A13,Def9; k in dom decomp b by A7,A9,FINSEQ_3:31; then consider b1', b2' being bag of n such that A15: (decomp b)/.k = <*b1', b2'*> and A16: b = b1'+b2' by Th72; b1' = b1 & b2' = b2 by A11,A15,GROUP_7:2; hence x' in D by A14,A16; end; then Support (p*'q) is finite by A3,FINSET_1:13; hence p*'q is finite-Support by Def10; end; end; begin :: The ring of polynomials --------------------------------------------- definition let n be Ordinal, L be right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); func Polynom-Ring (n, L) -> strict non empty doubleLoopStr means :Def27: (for x being set holds x in the carrier of it iff x is Polynomial of n, L) & (for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x+y = p+q) & (for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q holds x*y = p*'q) & 0.it = 0_(n,L) & 1_ it = 1_(n,L); existence proof defpred Q[set] means ex x' being Series of n, L st x' = $1 & x' is finite-Support; consider P being Subset of Funcs(Bags n, the carrier of L) such that A1: for x being Element of Funcs(Bags n, the carrier of L)holds x in P iff Q[x] from SubsetEx; consider x' being finite-Support Series of n, L; x' in Funcs(Bags n, the carrier of L) by FUNCT_2:11; then reconsider P as non empty Subset of Funcs(Bags n, the carrier of L) by A1; defpred A[set, set, set] means ex p, q, r being Polynomial of n, L st p = $1 & q = $2 & r = $3 & p+q=r; A2: now let x be Element of P, y be Element of P; reconsider p = x, q = y as Element of Funcs(Bags n, the carrier of L); consider p' being Series of n, L such that A3: p' = p & p' is finite-Support by A1; consider q' being Series of n, L such that A4: q' = q & q' is finite-Support by A1; reconsider p', q' as Polynomial of n, L by A3,A4; set r = p'+q'; r in Funcs(Bags n, the carrier of L) by FUNCT_2:11; then reconsider u = r as Element of P by A1; take u; thus A[x,y,u] by A3,A4; end; consider fadd being Function of [:P,P:],P such that A5: for x being Element of P, y being Element of P holds A[x,y,fadd.[x,y]] from FuncEx2D(A2); defpred M[set, set, set] means ex p, q, r being Polynomial of n, L st p = $1 & q = $2 & r = $3 & p*'q=r; A6: now let x be Element of P, y be Element of P; reconsider p = x, q = y as Element of Funcs(Bags n, the carrier of L); consider p' being Series of n, L such that A7: p' = p & p' is finite-Support by A1; consider q' being Series of n, L such that A8: q' = q & q' is finite-Support by A1; reconsider p', q' as Polynomial of n, L by A7,A8; set r = p'*'q'; r in Funcs(Bags n, the carrier of L) by FUNCT_2:11; then reconsider u = r as Element of P by A1; take u; thus M[x,y,u] by A7,A8; end; consider fmult being Function of [:P,P:],P such that A9: for x being Element of P, y being Element of P holds M[x,y,fmult.[x,y]] from FuncEx2D(A6); reconsider Z = ((Bags n) --> 0.L) as Function of Bags n, the carrier of L by FUNCOP_1:57; reconsider Z' = Z as Function of Bags n, L; reconsider Z' as Series of n, L; reconsider ZZ = Z as Element of Funcs(Bags n, the carrier of L) by FUNCT_2:11; now given x being set such that A10: x in Support Z'; reconsider x as Element of Bags n by A10; Z'.x = 0.L by FUNCOP_1:13; hence contradiction by A10,Def9; end; then Support Z' = {} by XBOOLE_0:def 1; then Z' is finite-Support by Def10; then ZZ in P by A1; then reconsider Ze = Z as Element of P; reconsider O = Z+*(EmptyBag n,1.L) as Function of Bags n, the carrier of L; reconsider O' = O as Function of Bags n, L; reconsider O' as Series of n, L; reconsider O as Element of Funcs(Bags n, the carrier of L) by FUNCT_2:11; now let x be set; hereby assume A11: x in Support O'; then reconsider x' = x as Element of Bags n; assume x <> EmptyBag n; then O'.x = Z.x' by FUNCT_7:34 .= 0.L by FUNCOP_1:13; hence contradiction by A11,Def9; end; assume A12: x = EmptyBag n; dom Z = Bags n by FUNCOP_1:19; then O'.x = 1.L by A12,FUNCT_7:33; then O'.x <> 0.L by Th27; hence x in Support O' by A12,Def9; end; then Support O' = {EmptyBag n} by TARSKI:def 1; then O' is finite-Support by Def10; then reconsider O as Element of P by A1; reconsider R = doubleLoopStr(# P, fadd, fmult, O, Ze #) as strict non empty doubleLoopStr; take R; thus for x being set holds x in the carrier of R iff x is Polynomial of n, L proof let x be set; hereby assume A13: x in the carrier of R; then reconsider xx = x as Element of Funcs(Bags n, the carrier of L); consider x' being Series of n, L such that A14: x' = xx & x' is finite-Support by A1,A13; thus x is Polynomial of n, L by A14; end; assume A15: x is Polynomial of n, L; then x is Element of Funcs(Bags n, the carrier of L) by FUNCT_2:11; hence x in the carrier of R by A1,A15; end; hereby let x, y be Element of R, p, q be Polynomial of n, L such that A16: x = p & y = q; consider p', q', r' being Polynomial of n, L such that A17: p' = x & q' = y & r' = fadd.[x,y] and A18: p'+q'= r' by A5; thus x+y = p+q by A16,A17,A18,RLVECT_1:def 3; end; hereby let x, y be Element of R, p, q be Polynomial of n, L such that A19: x = p & y = q; consider p', q', r' being Polynomial of n, L such that A20: p' = x & q' = y & r' = fmult.[x,y] and A21: p'*'q'= r' by A9; thus x*y = fmult.(x,y) by VECTSP_1:def 10 .= p*'q by A19,A20,A21,BINOP_1:def 1; end; thus 0.R = (Bags n) --> 0.L by RLVECT_1:def 2 .= 0_(n,L) by Def24; thus 1_ R = ((Bags n) --> 0.L)+*(EmptyBag n,1.L) by VECTSP_1:def 9 .= (0_(n,L))+*(EmptyBag n,1.L) by Def24 .= 1_(n,L) by Def25; end; uniqueness proof let it1, it2 be strict non empty doubleLoopStr such that A22: (for x being set holds x in the carrier of it1 iff x is Polynomial of n, L) and A23: (for x, y being Element of it1, p, q being Polynomial of n, L st x = p & y = q holds x+y = p+q) and A24: (for x, y being Element of it1, p, q being Polynomial of n, L st x = p & y = q holds x*y = p*'q) and A25: 0.it1 = 0_(n,L) and A26: 1_ it1 = 1_(n,L) and A27: (for x being set holds x in the carrier of it2 iff x is Polynomial of n, L) and A28: (for x, y being Element of it2, p, q being Polynomial of n, L st x = p & y = q holds x+y = p+q) and A29: (for x, y being Element of it2, p, q being Polynomial of n, L st x = p & y = q holds x*y = p*'q) and A30: 0.it2 = 0_(n,L) and A31: 1_ it2 = 1_(n,L); A32: now let x be set; hereby assume x in the carrier of it1; then x is Polynomial of n, L by A22; hence x in the carrier of it2 by A27; end; assume x in the carrier of it2; then x is Polynomial of n, L by A27; hence x in the carrier of it1 by A22; end; then A33: the carrier of it1 = the carrier of it2 by TARSKI:2; now let a, b be Element of it1; reconsider a1 = a, b1 = b as Element of it1; reconsider p = a, q = b as Polynomial of n, L by A22; reconsider a' = a, b' = b as Element of it2 by A32; reconsider a1' = a', b1' = b' as Element of it2; thus (the add of it1).(a, b) = (the add of it1).[a, b] by BINOP_1:def 1 .= a1+b1 by RLVECT_1:def 3 .= p+q by A23 .= a1'+b1' by A28 .= (the add of it2).[a', b'] by RLVECT_1:def 3 .= (the add of it2).(a, b) by BINOP_1:def 1; end; then A34: the add of it1 = the add of it2 by A33,BINOP_1:2; A35: now let a, b be Element of it1; reconsider a1 = a, b1 = b as Element of it1; reconsider p = a, q = b as Polynomial of n, L by A22; reconsider a' = a, b' = b as Element of it2 by A32; reconsider a1' = a', b1' = b' as Element of it2; thus (the mult of it1).(a, b) = a1*b1 by VECTSP_1:def 10 .= p*'q by A24 .= a1'*b1' by A29 .= (the mult of it2).(a, b) by VECTSP_1:def 10; end; A36: the Zero of it1 = 0.it2 by A25,A30,RLVECT_1:def 2 .= the Zero of it2 by RLVECT_1:def 2; the unity of it1 = 1_ it2 by A26,A31,VECTSP_1:def 9 .= the unity of it2 by VECTSP_1:def 9; hence thesis by A33,A34,A35,A36,BINOP_1:2; end; end; definition let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> Abelian; coherence proof set Pm = Polynom-Ring (n, L); let v, w be Element of Pm; reconsider p = v, q = w as Polynomial of n, L by Def27; thus v + w = q+p by Def27 .= w + v by Def27; end; end; definition let n be Ordinal, L be add-associative right_zeroed right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> add-associative; coherence proof set Pm = Polynom-Ring (n, L); let u, v, w be Element of Pm; reconsider o = u, p = v, q = w as Polynomial of n, L by Def27; A1: v+w = p+q by Def27; u+v = o+p by Def27; hence (u+v)+w = (o+p)+q by Def27 .= o+(p+q) by Th80 .= u+(v+w) by A1,Def27; end; end; definition let n be Ordinal, L be right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> right_zeroed; coherence proof let v be Element of Polynom-Ring (n, L); reconsider p = v as Polynomial of n, L by Def27; 0.Polynom-Ring (n, L) = 0_(n,L) by Def27; hence v + 0.Polynom-Ring (n, L) = p+0_(n,L) by Def27 .= v by Th82; end; end; definition let n be Ordinal, L be right_complementable right_zeroed add-associative unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> right_complementable; coherence proof let v be Element of Polynom-Ring (n,L); reconsider p = v as Polynomial of n, L by Def27; reconsider w = -p as Element of Polynom-Ring(n,L) by Def27; take w; thus v + w = p+-p by Def27 .= p-p by Def23 .= 0_(n,L) by Th83 .= 0.Polynom-Ring(n,L) by Def27; end; end; definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative unital distributive non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> commutative; coherence proof set Pm = Polynom-Ring (n, L); let v, w be Element of Pm; reconsider p = v, q = w as Polynomial of n, L by Def27; thus v*w = q*'p by Def27 .= w*v by Def27; end; end; definition let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable unital distributive associative non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> associative; coherence proof set Pm = Polynom-Ring (n, L); let x,y,z be Element of Pm; reconsider p = x, q = y, r = z as Polynomial of n, L by Def27; A1: y*z = q*'r by Def27; x*y = p*'q by Def27; hence (x*y)*z = (p*'q)*'r by Def27 .= p*'(q*'r) by Th86 .= x*(y*z) by A1,Def27; end; end; definition let n be Ordinal, L be right_zeroed Abelian add-associative right_complementable unital distributive associative non trivial (non empty doubleLoopStr); cluster Polynom-Ring (n, L) -> unital right-distributive; coherence proof set Pm = Polynom-Ring (n, L); thus Polynom-Ring (n, L) is unital proof take e = 1_ Pm; let x be Element of Pm; reconsider p = x as Polynomial of n, L by Def27; A1: 1_ Pm = 1_(n,L) by Def27; hence x*e = p*'1_(n,L) by Def27 .= x by Th88; thus e*x = 1_(n,L)*'p by A1,Def27 .= x by Th89; end; let x, y, z be Element of Pm; reconsider p = x, q = y, r = z as Polynomial of n, L by Def27; A2: x*y = p*'q by Def27; A3: x*z = p*'r by Def27; y+z = q+r by Def27; hence x*(y+z) = p*'(q+r) by Def27 .= p*'q+p*'r by Th85 .= x*y + x*z by A2,A3,Def27; end; end;

Back to top