:: Monoid of Multisets and Subsets :: by Grzegorz Bancerek :: :: Received December 29, 1992 :: Copyright (c) 1992-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SUBSET_1, NUMBERS, ALGSTR_0, MESFUNC1, XBOOLE_0, FUNCT_1, ZFMISC_1, FINSEQ_4, FUNCT_2, RELAT_1, PARTFUN1, TARSKI, FUNCOP_1, FINSEQ_2, FINSEQ_1, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0, LATTICE2, MCART_1, STRUCT_0, GROUP_1, VECTSP_1, BINOP_2, CARD_1, ARYTM_3, FUNCT_3, FINSET_1, ORDINAL4, COMPLEX1, ARYTM_1, MONOID_1, NAT_1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, REAL_1, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, MONOID_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, RECDEF_1, SETWISEO, FINSET_1, FUNCT_3, FINSEQ_2, LATTICE2, FUNCT_6, DOMAIN_1, ALGSTR_0; constructors BINOP_1, DOMAIN_1, FUNCT_3, SETWISEO, REAL_1, BINOP_2, RECDEF_1, FUNCT_5, FUNCT_6, LATTICE2, MONOID_0, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, MONOID_0, CARD_1, RELSET_1, XTUPLE_0, VALUED_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, BINOP_1, LATTICE2, SETWISEO, MONOID_0, STRUCT_0, XBOOLE_0; equalities BINOP_1, STRUCT_0, FUNCT_6, ALGSTR_0; expansions TARSKI, BINOP_1, SETWISEO, MONOID_0, XBOOLE_0, RELAT_1; theorems TARSKI, NAT_1, FINSEQ_1, BINOP_1, MCART_1, FUNCOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3, CARD_1, CARD_2, FINSEQ_2, FINSEQ_3, FUNCT_5, MONOID_0, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, GROUP_1; schemes NAT_1, FUNCT_2, MONOID_0, PARTFUN1, FUNCT_1, BINOP_1; begin :: Updating reserve x,y,z, X,Y,Z for set, n for Element of NAT; deffunc op(multMagma) = the multF of \$1; deffunc un(multLoopStr) = 1.\$1; definition let f be Function, x1,x2,y be set; func f..(x1,x2,y) -> set equals f..([x1,x2],y); correctness; end; definition let A,D1,D2,D be non empty set; let f be Function of [:D1, D2:], Funcs(A,D); let x1 be Element of D1; let x2 be Element of D2; let x be Element of A; redefine func f..(x1,x2,x) -> Element of D; coherence proof reconsider g = f.(x1,x2) as Element of Funcs(A,D); A1: [x1,x2] in [:D1,D2:]; dom f = [:D1,D2:] & dom g = A by FUNCT_2:def 1; then f..(x1,x2,x) = g.x by A1,FUNCT_5:38; hence thesis; end; end; definition let A be set; let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let g1 be Function of A,D1; let g2 be Function of A,D2; redefine func f.:(g1,g2) -> Element of Funcs(A,D); coherence proof f.:(g1,g2) = f*<:g1,g2:> by FUNCOP_1:def 3; then dom (f.:(g1,g2)) = A & rng (f.:(g1,g2)) c= D by FUNCT_2:def 1 ,RELAT_1:def 19; hence thesis by FUNCT_2:def 2; end; end; notation let A be non empty set; let n be Element of NAT, x be Element of A; synonym n .--> x for n |-> x; end; definition let A be non empty set; let n be Element of NAT, x be Element of A; redefine func n .--> x -> FinSequence of A; coherence by FINSEQ_2:63; end; definition let D be non empty set, A be set, d be Element of D; redefine func A --> d -> Element of Funcs(A,D); coherence proof dom (A --> d) = A & rng (A --> d) c= {d} by FUNCOP_1:13; hence thesis by FUNCT_2:def 2; end; end; definition let A be set; let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let d be Element of D1; let g be Function of A,D2; redefine func f[;](d,g) -> Element of Funcs(A,D); coherence proof dom g = A by FUNCT_2:def 1; then f[;](d,g) = f*<:A --> d, g:> by FUNCOP_1:def 5; then dom (f[;](d,g)) = A & rng (f[;](d,g)) c= D by FUNCT_2:def 1 ,RELAT_1:def 19; hence thesis by FUNCT_2:def 2; end; end; definition let A be set; let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let g be Function of A,D1; let d be Element of D2; redefine func f[:](g,d) -> Element of Funcs(A,D); coherence proof dom g = A by FUNCT_2:def 1; then f[:](g,d) = f*<:g, A --> d:> by FUNCOP_1:def 4; then dom (f[:](g,d)) = A & rng (f[:](g,d)) c= D by FUNCT_2:def 1 ,RELAT_1:def 19; hence thesis by FUNCT_2:def 2; end; end; theorem for f,g being Function, X being set holds (f|X)*g = f*(X|`g) proof let f,g be Function, X be set; A1: dom (f|X) = dom f /\ X by RELAT_1:61; A2: dom ((f|X)*g) = dom (f*(X|`g)) proof thus dom ((f|X)*g) c= dom (f*(X|`g)) proof let x be object; assume A3: x in dom ((f|X)*g); then A4: x in dom g by FUNCT_1:11; A5: g.x in dom (f|X) by A3,FUNCT_1:11; then A6: g.x in dom f by A1,XBOOLE_0:def 4; g.x in X by A1,A5,XBOOLE_0:def 4; then A7: x in dom (X|`g) by A4,FUNCT_1:53; then g.x = (X|`g).x by FUNCT_1:53; hence thesis by A6,A7,FUNCT_1:11; end; let x be object; assume A8: x in dom (f*(X|`g)); then A9: x in dom (X|`g) by FUNCT_1:11; then A10: x in dom g by FUNCT_1:53; (X|`g).x in dom f by A8,FUNCT_1:11; then A11: g.x in dom f by A9,FUNCT_1:53; g.x in X by A9,FUNCT_1:53; then g.x in dom (f|X) by A1,A11,XBOOLE_0:def 4; hence thesis by A10,FUNCT_1:11; end; now let x be object; assume A12: x in dom ((f|X)*g); then ((f|X)*g).x = (f|X).(g.x) & g.x in dom (f|X) by FUNCT_1:11,12; then A13: ((f|X)*g).x = f.(g.x) by FUNCT_1:47; (f*(X|`g)).x = f.((X|`g).x) & x in dom (X|`g) by A2,A12,FUNCT_1:11,12; hence ((f|X)*g).x = (f*(X|`g)).x by A13,FUNCT_1:53; end; hence thesis by A2,FUNCT_1:2; end; scheme NonUniqFuncDEx { X() -> set, Y() -> non empty set, P[object,object] }: ex f being Function of X(), Y() st for x being object st x in X() holds P[x,f.x] provided A1: for x being object st x in X() ex y being Element of Y() st P[x,y] proof A2: for x being object st x in X() ex y being object st y in Y() & P[x,y] proof let x be object; assume x in X(); then consider y being Element of Y() such that A3: P[x,y] by A1; take y; thus thesis by A3; end; consider f being Function such that A4: dom f = X() & rng f c= Y() & for x being object st x in X() holds P[x,f.x] from FUNCT_1:sch 6(A2); reconsider f as Function of X(), Y() by A4,FUNCT_2:def 1,RELSET_1:4; take f; thus thesis by A4; end; begin :: Monoid of functions into a semigroup definition let D1,D2,D be non empty set; let f be Function of [:D1,D2:],D; let A be set; func (f,D).:A -> Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D) means : Def2: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(A,D2) holds it.(f1,f2) = f.:(f1,f2); existence proof deffunc G(Element of Funcs(A,D1),Element of Funcs(A,D2)) = f.:(\$1,\$2); consider b being Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D) such that A1: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs( A,D2) holds b.(f1,f2) = G(f1,f2) from BINOP_1:sch 4; take b; let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2); thus thesis by A1; end; uniqueness proof let o1,o2 be Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D) such that A2: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs( A,D2) holds o1.(f1,f2) = f.:(f1,f2) and A3: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs( A,D2) holds o2.(f1,f2) = f.:(f1,f2); now let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2); thus o1.(f1,f2) = f.:(f1,f2) by A2 .= o2.(f1,f2) by A3; end; hence thesis; end; end; theorem for D1,D2,D being non empty set for f being Function of [:D1,D2:],D for A being set, f1 being (Function of A,D1), f2 being Function of A,D2 for x st x in A holds ((f,D).:A)..(f1,f2,x) = f.(f1.x,f2.x) proof let D1,D2,D be non empty set; let f be Function of [:D1,D2:],D; let A be set, f1 be (Function of A,D1), f2 be Function of A,D2; dom f2 = A & rng f2 c= D2 by FUNCT_2:def 1; then reconsider f2 as Element of Funcs(A,D2) by FUNCT_2:def 2; dom f1 = A & rng f1 c= D1 by FUNCT_2:def 1; then reconsider f1 as Element of Funcs(A,D1) by FUNCT_2:def 2; A1: dom (f.: (f1,f2)) = A by FUNCT_2:def 1; A2: ((f,D).:A).(f1,f2) = f.:(f1,f2) & [f1,f2] = [f1,f2] by Def2; let x such that A3: x in A; dom ((f,D).:A) = [:Funcs(A,D1), Funcs(A,D2):] & (f.:(f1,f2)).x = f.(f1.x ,f2. x) by A3,A1,FUNCOP_1:22,FUNCT_2:def 1; hence thesis by A3,A1,A2,FUNCT_5:38; end; reserve A for set, D for non empty set, a,b,c,l,r for Element of D, o,o9 for BinOp of D, f,g,h for Function of A,D; theorem Th3: o is commutative implies o.:(f,g) = o.:(g,f) proof A1: dom (o.:(f,g)) = A by FUNCT_2:def 1; A2: dom f = A & dom g = A by FUNCT_2:def 1; A3: dom (o.:(g,f)) = A by FUNCT_2:def 1; assume A4: o.(a,b) = o.(b,a); now let x be object; assume A5: x in A; then f.x in rng f & g.x in rng g by A2,FUNCT_1:def 3; then reconsider a = f.x, b = g.x as Element of D; thus (o.:(f,g)).x = o.(a,b) by A1,A5,FUNCOP_1:22 .= o.(b,a) by A4 .= (o.:(g,f)).x by A3,A5,FUNCOP_1:22; end; hence thesis by A1,A3,FUNCT_1:2; end; theorem Th4: o is associative implies o.:(o.:(f,g),h) = o.:(f,o.:(g,h)) proof A1: dom (o.:(f,g)) = A by FUNCT_2:def 1; A2: dom (o.:(g,h)) = A by FUNCT_2:def 1; A3: dom f = A & dom g = A by FUNCT_2:def 1; A4: dom (o.:(o.:(f,g),h)) = A by FUNCT_2:def 1; A5: dom h = A by FUNCT_2:def 1; A6: dom (o.:(f,o.:(g,h))) = A by FUNCT_2:def 1; assume A7: o.(o.(a,b),c) = o.(a,o.(b,c)); now let x be object; assume A8: x in A; then A9: h.x in rng h by A5,FUNCT_1:def 3; f.x in rng f & g.x in rng g by A3,A8,FUNCT_1:def 3; then reconsider a = f.x, b = g.x, c = h.x as Element of D by A9; thus (o.:(o.:(f,g),h)).x = o.((o.:(f,g)).x,c) by A4,A8,FUNCOP_1:22 .= o.(o.(a,b),c) by A1,A8,FUNCOP_1:22 .= o.(a,o.(b,c)) by A7 .= o.(a,(o.:(g,h)).x) by A2,A8,FUNCOP_1:22 .= (o.:(f,o.:(g,h))).x by A6,A8,FUNCOP_1:22; end; hence thesis by A4,A6,FUNCT_1:2; end; theorem Th5: a is_a_unity_wrt o implies o[;](a,f) = f & o[:](f,a) = f proof assume A1: a is_a_unity_wrt o; A2: dom f = A by FUNCT_2:def 1; A3: dom (o[;](a,f)) = A by FUNCT_2:def 1; now let x be object; assume A4: x in A; then f.x in rng f by A2,FUNCT_1:def 3; then reconsider b = f.x as Element of D; thus (o[;](a,f)).x = o.(a,b) by A3,A4,FUNCOP_1:32 .= f.x by A1,BINOP_1:3; end; hence o[;](a,f) = f by A3,A2,FUNCT_1:2; A5: dom (o[:](f,a)) = A by FUNCT_2:def 1; now let x be object; assume A6: x in A; then f.x in rng f by A2,FUNCT_1:def 3; then reconsider b = f.x as Element of D; thus (o[:](f,a)).x = o.(b,a) by A5,A6,FUNCOP_1:27 .= f.x by A1,BINOP_1:3; end; hence thesis by A5,A2,FUNCT_1:2; end; theorem Th6: o is idempotent implies o.:(f,f) = f proof A1: dom (o.:(f,f)) = A by FUNCT_2:def 1; assume A2: o.(a,a) = a; A3: now let x be object; assume A4: x in A; then reconsider a = f.x as Element of D by FUNCT_2:5; thus o.:(f,f).x = o.(a,a) by A1,A4,FUNCOP_1:22 .= f.x by A2; end; dom f = A by FUNCT_2:def 1; hence thesis by A1,A3,FUNCT_1:2; end; theorem Th7: o is commutative implies (o,D).:A is commutative proof assume A1: o is commutative; set h = (o,D).:A; let f,g be Element of Funcs(A,D); thus h.(f,g) = o.:(f, g) by Def2 .= o.:(g, f) by A1,Th3 .= h.(g,f) by Def2; end; theorem Th8: o is associative implies (o,D).:A is associative proof assume A1: o is associative; set F = (o,D).:A; let f,g,h be Element of Funcs(A,D); thus F.(F.(f,g),h) = F.(o.:(f,g),h) by Def2 .= o.:(o.:(f,g),h) by Def2 .= o.:(f,o.:(g,h)) by A1,Th4 .= F.(f,o.:(g,h)) by Def2 .= F.(f,F.(g,h)) by Def2; end; theorem Th9: a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D).:A proof set e = A --> a; set F = (o,D).:A; assume A1: a is_a_unity_wrt o; now let f be Element of Funcs(A,D); A2: dom f = A by FUNCT_2:def 1; thus F.(e,f) = o.:(e,f) by Def2 .= o[;](a,f) by A2,FUNCOP_1:31 .= f by A1,Th5; thus F.(f,e) = o.:(f,e) by Def2 .= o[:](f,a) by A2,FUNCOP_1:26 .= f by A1,Th5; end; hence thesis by BINOP_1:3; end; theorem Th10: o is having_a_unity implies the_unity_wrt (o,D).:A = A --> the_unity_wrt o & (o,D).:A is having_a_unity proof given a such that A1: a is_a_unity_wrt o; a = the_unity_wrt o & A --> a is_a_unity_wrt (o,D).:A by A1,Th9,BINOP_1:def 8 ; hence the_unity_wrt (o,D).:A = A --> the_unity_wrt o by BINOP_1:def 8; take A --> a; thus thesis by A1,Th9; end; theorem Th11: o is idempotent implies (o,D).:A is idempotent proof assume A1: o is idempotent; let f be Element of Funcs(A,D); thus ((o,D).:A).(f,f) = o.:(f,f) by Def2 .= f by A1,Th6; end; theorem Th12: o is invertible implies (o,D).:A is invertible proof assume A1: for a,b ex r,l st o.(a,r) = b & o.(l,a) = b; let f,g be Element of Funcs(A,D); defpred P[object,object] means o.(f.\$1,\$2) = g.\$1; A2: for x being object st x in A ex c st P[x,c] proof let x be object; assume x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5; consider r,l such that A3: o.(a,r) = b and o.(l,a) = b by A1; take r; thus thesis by A3; end; consider h1 being Function of A,D such that A4: for x being object st x in A holds P[x,h1.x] from NonUniqFuncDEx(A2); defpred Q[object,object] means o.(\$2,f.\$1) = g.\$1; A5: for x being object st x in A ex c st Q[x,c] proof let x be object; assume x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5; consider r,l such that o.(a,r) = b and A6: o.(l,a) = b by A1; take l; thus thesis by A6; end; consider h2 being Function of A,D such that A7: for x being object st x in A holds Q[x,h2.x] from NonUniqFuncDEx(A5); A8: dom h1 = A & dom h2 = A by FUNCT_2:def 1; rng h1 c= D & rng h2 c= D; then reconsider h1, h2 as Element of Funcs(A,D) by A8,FUNCT_2:def 2; take h1, h2; A9: dom g = A by FUNCT_2:def 1; A10: dom (o.:(f,h1)) = A by FUNCT_2:def 1; A11: now let x be object; assume A12: x in A; hence o.:(f,h1).x = o.(f.x,h1.x) by A10,FUNCOP_1:22 .= g.x by A4,A12; end; o.:(f,h1) = ((o,D).:A).(f,h1) by Def2; hence ((o,D).:A).(f,h1) = g by A10,A9,A11,FUNCT_1:2; A13: dom (o.:(h2,f)) = A by FUNCT_2:def 1; A14: now let x be object; assume A15: x in A; hence o.:(h2,f).x = o.(h2.x,f.x) by A13,FUNCOP_1:22 .= g.x by A7,A15; end; o.:(h2,f) = ((o,D).:A).(h2,f) by Def2; hence thesis by A13,A9,A14,FUNCT_1:2; end; theorem Th13: o is cancelable implies (o,D).:A is cancelable proof assume A1: o.(a,b) = o.(a,c) or o.(b,a) = o.(c,a) implies b = c; let f,g,h be Element of Funcs(A,D) such that A2: (o,D).:A.(f,g) = (o,D).:A.(f,h) or (o,D).:A.(g,f) = (o,D).:A.(h,f); A3: A = dom (o.:(g,f)) & A = dom (o.:(h,f)) by FUNCT_2:def 1; A4: (o,D).:A.(f,h) = o.:(f,h) & (o,D).:A.(h,f) = o.:(h,f) by Def2; A5: A = dom (o.:(f,g)) & A = dom (o.:(f,h)) by FUNCT_2:def 1; A6: (o,D).:A.(f,g) = o.:(f,g) & (o,D).:A.(g,f) = o.:(g,f) by Def2; A7: now let x be object; assume A8: x in A; then reconsider a = f.x, b = g.x, c = h.x as Element of D by FUNCT_2:5; A9: o.:(g,f).x = o.(b,a) & o.:(h,f).x = o.(c,a) by A3,A8,FUNCOP_1:22; o.:(f,g).x = o.(a,b) & o.:(f,h).x = o.(a,c) by A5,A8,FUNCOP_1:22; hence g.x = h.x by A1,A2,A6,A4,A9; end; dom g = A & dom h = A by FUNCT_2:def 1; hence thesis by A7,FUNCT_1:2; end; theorem Th14: o is uniquely-decomposable implies (o,D).:A is uniquely-decomposable proof assume that A1: o is having_a_unity and A2: for a,b st o.(a,b) = the_unity_wrt o holds a = b & b = the_unity_wrt o; A3: the_unity_wrt (o,D).:A = A --> the_unity_wrt o by A1,Th10; thus (o,D).:A is having_a_unity by A1,Th10; let f,g be Element of Funcs(A,D) such that A4: (o,D).:A.(f,g) = the_unity_wrt (o,D).:A; A5: dom (o.:(f,g)) = A by FUNCT_2:def 1; A6: (o,D).:A.(f,g) = o.:(f,g) by Def2; A7: now let x be object; assume A8: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5; (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o by A5,A8,FUNCOP_1:7,22; hence f.x = g.x by A2,A4,A6,A3; end; A9: now let x be object; assume A10: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5; (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o by A5,A10,FUNCOP_1:7,22; hence g.x = (A --> the_unity_wrt o).x by A2,A4,A6,A3; end; A11: dom g = A by FUNCT_2:def 1; dom f = A by FUNCT_2:def 1; hence f = g by A11,A7,FUNCT_1:2; dom (A --> the_unity_wrt o) = A by FUNCT_2:def 1; hence thesis by A3,A11,A9,FUNCT_1:2; end; theorem o absorbs o9 implies (o,D).:A absorbs (o9,D).:A proof assume A1: o.(a,o9.(a,b)) = a; let f,g be Element of Funcs(A,D); A2: dom (o.:(f,o9.:(f,g))) = A by FUNCT_2:def 1; A3: dom (o9.:(f,g)) = A by FUNCT_2:def 1; A4: now let x be object; assume A5: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5; (o.:(f,o9.:(f,g))).x = o.(a,(o9.:(f,g)).x) & (o9.:(f,g)).x = o9.(a,b ) by A3,A2,A5,FUNCOP_1:22; hence f.x = (o.:(f,o9.:(f,g))).x by A1; end; A6: dom f = A by FUNCT_2:def 1; ((o9,D).:A).(f,g) = o9.:(f,g) & ((o,D).:A).(f,o9.:(f,g)) = o.:(f,o9.: (f ,g)) by Def2; hence thesis by A6,A2,A4,FUNCT_1:2; end; theorem Th16: for D1, D2, D, E1, E2, E being non empty set, o1 being Function of [:D1, D2:], D, o2 being Function of [:E1, E2:], E st o1 c= o2 holds (o1,D).:A c= (o2,E).:A proof let D1, D2, D, E1, E2, E be non empty set, o1 be Function of [:D1, D2:], D, o2 be Function of [:E1, E2:], E; A1: dom o1 = [:D1,D2:] by FUNCT_2:def 1; assume A2: o1 c= o2; then A3: dom o1 c= dom o2 by GRFUNC_1:2; A4: dom o2 = [:E1,E2:] by FUNCT_2:def 1; then D2 c= E2 by A3,A1,ZFMISC_1:114; then A5: Funcs(A,D2) c= Funcs(A,E2) by FUNCT_5:56; D1 c= E1 by A3,A1,A4,ZFMISC_1:114; then A6: Funcs(A,D1) c= Funcs(A,E1) by FUNCT_5:56; A7: now let x be object; assume x in dom (o1,D).:A; then reconsider y = x as Element of [:Funcs(A,D1),Funcs(A,D2):]; reconsider g2 = y`2 as Element of Funcs(A,E2) by A5; reconsider f2 = y`2 as Element of Funcs(A,D2); reconsider g1 = y`1 as Element of Funcs(A,E1) by A6; reconsider f1 = y`1 as Element of Funcs(A,D1); A8: dom (o2.:(g1,g2)) = A & dom (o1.:(f1,f2)) = A by FUNCT_2:def 1; A9: dom f1 = A & dom f2 = A by FUNCT_2:def 1; A10: now let z be object; assume A11: z in A; then f1.z in rng f1 & f2.z in rng f2 by A9,FUNCT_1:def 3; then A12: [f1.z,f2.z] in dom o1 by A1,ZFMISC_1:87; (o2.:(g1,g2)).z = o2.(g1.z,g2.z) & (o1.:(f1,f2)).z = o1.(f1.z, f2. z) by A8,A11,FUNCOP_1:22; hence (o2.:(g1,g2)).z = (o1.:(f1,f2)).z by A2,A12,GRFUNC_1:2; end; A13: [f1,f2] = x by MCART_1:21; ((o1,D).:A).(f1,f2) = o1.:(f1,f2) & ((o2,E).:A).(g1,g2) = o2.:(g1,g2) by Def2; hence ((o1,D).:A).x = ((o2,E).:A).x by A8,A10,A13,FUNCT_1:2; end; dom (o1,D).:A = [:Funcs(A,D1),Funcs(A,D2):] & dom (o2,E).:A = [:Funcs(A, E1), Funcs(A,E2):] by FUNCT_2:def 1; then dom (o1,D).:A c= dom (o2,E).:A by A6,A5,ZFMISC_1:96; hence thesis by A7,GRFUNC_1:2; end; definition let G be non empty multMagma; let A be set; func .:(G,A) -> multMagma equals : Def3: multLoopStr (# Funcs(A, the carrier of G), (the multF of G,the carrier of G).:A, A --> the_unity_wrt the multF of G #) if G is unital otherwise multMagma (# Funcs(A, the carrier of G), (the multF of G,the carrier of G).:A #); correctness; end; registration let G be non empty multMagma; let A be set; cluster .:(G,A) -> non empty; coherence proof per cases; suppose G is unital; then .:(G,A) = multLoopStr (# Funcs(A, the carrier of G), (the multF of G ,the carrier of G).:A, (A --> the_unity_wrt the multF of G)#) by Def3; hence the carrier of .:(G,A) is non empty; end; suppose G is not unital; then .:(G,A) = multMagma (# Funcs(A, the carrier of G), (the multF of G, the carrier of G).:A #) by Def3; hence the carrier of .:(G,A) is non empty; end; end; end; reserve G for non empty multMagma; deffunc carr(non empty multMagma) = the carrier of \$1; theorem Th17: the carrier of .:(G,X) = Funcs(X, the carrier of G) & the multF of .:(G,X) = (the multF of G, the carrier of G).:X proof A1: not G is unital implies .:(G,X) = multMagma(#Funcs(X, carr(G)), (op(G), carr(G)).:X#) by Def3; G is unital implies .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G), carr(G)).:X, (X --> the_unity_wrt op(G))#) by Def3; hence thesis by A1; end; theorem x is Element of .: (G,X) iff x is Function of X, the carrier of G proof x is Element of .:(G,X) implies x is Element of Funcs(X, carr(G)) by Th17; hence x is Element of .:(G,X) implies x is Function of X, carr(G); assume x is Function of X, carr(G); then reconsider f = x as Function of X, carr(G); A1: rng f c= carr(G); carr(.:(G,X)) = Funcs(X, carr(G)) & dom f = X by Th17,FUNCT_2:def 1; hence thesis by A1,FUNCT_2:def 2; end; Lm1: .:(G,X) is constituted-Functions proof let a be Element of .:(G,X); a is Element of Funcs(X,carr(G)) by Th17; hence thesis; end; registration let G be non empty multMagma, A be set; cluster .:(G,A) -> constituted-Functions; coherence by Lm1; end; theorem Th19: for f being Element of .:(G,X) holds dom f = X & rng f c= the carrier of G proof let f be Element of .:(G,X); reconsider f as Element of Funcs(X, carr(G)) by Th17; f = f; hence thesis by FUNCT_2:def 1,RELAT_1:def 19; end; theorem Th20: for f,g being Element of .:(G,X) st for x being object st x in X holds f.x = g.x holds f = g proof let f,g be Element of .:(G,X); dom f = X & dom g = X by Th19; hence thesis by FUNCT_1:2; end; definition let G be non empty multMagma, A be non empty set; let f be Element of .:(G,A); let a be Element of A; redefine func f.a -> Element of G; coherence proof dom f = A by Th19; then A1: f.a in rng f by FUNCT_1:def 3; rng f c= carr(G) by Th19; hence thesis by A1; end; end; registration let G be non empty multMagma, A be non empty set; let f be Element of .:(G,A); cluster rng f -> non empty; coherence proof set a = the Element of A; dom f = A by Th19; then f.a in rng f by FUNCT_1:def 3; hence thesis; end; end; theorem Th21: for f1,f2 being Element of .:(G,D), a being Element of D holds ( f1*f2).a = (f1.a)*(f2.a) proof let f1,f2 be Element of .:(G,D), a be Element of D; reconsider g1 = f1, g2 = f2 as Element of Funcs(D, carr(G)) by Th17; op(.:(G,D)) = (op(G),carr(G)).:D by Th17; then dom (op(G).:(g1,g2)) = D & f1*f2 = op(G).:(g1,g2) by Def2,FUNCT_2:def 1; hence thesis by FUNCOP_1:22; end; definition let G be unital non empty multMagma; let A be set; redefine func .:(G,A) -> well-unital constituted-Functions strict non empty multLoopStr; coherence proof set M = multLoopStr(#Funcs(A, carr(G)), (op(G),carr(G)).:A, (A --> the_unity_wrt op(G))#); op(G) is having_a_unity by MONOID_0:def 10; then consider a being Element of G such that A1: a is_a_unity_wrt op(G); A2: 1.M = A --> the_unity_wrt the multF of G & .:(G,A) = M by Def3; a = the_unity_wrt op(G) & A --> a is_a_unity_wrt (op(G),carr(G)).:A by A1 ,Th9,BINOP_1:def 8; hence thesis by A2,MONOID_0:def 21; end; end; theorem Th22: for G being unital non empty multMagma holds 1..:(G,X) = X --> the_unity_wrt the multF of G proof let G be unital non empty multMagma; .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G), carr(G)).:X, (X --> the_unity_wrt op(G))#) by Def3; hence thesis; end; theorem Th23: for G being non empty multMagma, A being set holds (G is commutative implies .:(G,A) is commutative) & (G is associative implies .:(G,A) is associative) & (G is idempotent implies .:(G,A) is idempotent) & (G is invertible implies .:(G,A) is invertible) & (G is cancelable implies .:(G,A) is cancelable) & (G is uniquely-decomposable implies .:(G,A) is uniquely-decomposable) proof let G; let A be set; A1: op(.:(G,A)) = (op(G), carr(G)).:A & carr(.:(G,A)) = Funcs(A, carr(G)) by Th17; thus G is commutative implies .:(G,A) is commutative by A1,Th7; thus G is associative implies .:(G,A) is associative by A1,Th8; thus G is idempotent implies .:(G,A) is idempotent by A1,Th11; thus G is invertible implies .:(G,A) is invertible by A1,Th12; thus G is cancelable implies .:(G,A) is cancelable by A1,Th13; assume op(G) is uniquely-decomposable; hence op(.:(G,A)) is uniquely-decomposable by A1,Th14; end; theorem for H being non empty SubStr of G holds .:(H,X) is SubStr of .:(G,X) proof let H be non empty SubStr of G; A1: op(.:(H,X)) = (op(H), carr(H)).:X by Th17; op(H) c= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X by Th17,MONOID_0:def 23; hence op(.:(H,X)) c= op(.:(G,X)) by A1,Th16; end; theorem for G being unital non empty multMagma, H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds .:(H,X) is MonoidalSubStr of .:(G,X) proof let G be unital non empty multMagma, H be non empty SubStr of G; assume A1: the_unity_wrt the multF of G in carr(H); then reconsider G9 = G, H9 = H as unital non empty multMagma by MONOID_0:30; A2: the_unity_wrt op(H9) = the_unity_wrt op(G9) by A1,MONOID_0:30; A3: op(.:(H,X)) = (op(H), carr(H)).:X by Th17; op(H) c= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X by Th17,MONOID_0:def 23; then A4: op(.:(H,X)) c= op(.:(G,X)) by A3,Th16; 1..:(G9,X) = X --> the_unity_wrt op(G) & 1..:(H9,X) = X --> the_unity_wrt op (H) by Th22; hence thesis by A2,A4,MONOID_0:def 25; end; definition let G be unital associative commutative cancelable uniquely-decomposable non empty multMagma; let A be set; redefine func .:(G,A) -> commutative cancelable uniquely-decomposable constituted-Functions strict Monoid; coherence proof .:(G,A) is commutative cancelable by Th23; hence thesis by Th23; end; end; begin :: Monoid of multisets over a set definition let A be set; func MultiSet_over A -> commutative cancelable uniquely-decomposable constituted-Functions strict Monoid equals .:(, A); correctness; end; theorem Th26: the carrier of MultiSet_over X = Funcs(X,NAT) & the multF of MultiSet_over X = (addnat,NAT).:X & 1.MultiSet_over X = X --> 0 proof the multMagma of = & the_unity_wrt op() = 0 by MONOID_0:40,def 22; hence thesis by Th17,Th22,MONOID_0:46; end; definition let A be set; mode Multiset of A is Element of MultiSet_over A; end; theorem Th27: x is Multiset of X iff x is Function of X,NAT proof A1: now let x be Function of X,NAT; dom x = X & rng x c= NAT by FUNCT_2:def 1; hence x is Element of Funcs(X,NAT) by FUNCT_2:def 2; end; x is Multiset of X iff x is Element of Funcs(X,NAT) by Th26; hence thesis by A1; end; theorem Th28: for m being Multiset of X holds dom m = X & rng m c= NAT proof let m be Multiset of X; m is Function of X,NAT by Th27; hence thesis by FUNCT_2:def 1,RELAT_1:def 19; end; registration let X; cluster -> NAT-valued for Multiset of X; coherence by Th28; end; theorem Th29: for m1,m2 being Multiset of D, a being Element of D holds (m1 [*] m2).a = (m1.a)+(m2.a) proof reconsider N = as non empty multMagma; let m1,m2 be Multiset of D, a be Element of D; reconsider f1 = m1, f2 = m2 as Element of .:(N,D); thus (m1 [*] m2).a = (f1.a)*(f2.a) by Th21 .= (m1.a)+(m2.a) by MONOID_0:45; end; theorem Th30: chi(Y,X) is Multiset of X proof rng chi(Y,X) c= {0,1}; then A1: rng chi(Y,X) c= NAT by XBOOLE_1:1; dom chi(Y,X) = X & carr(MultiSet_over X) = Funcs(X,NAT) by Th26,FUNCT_3:def 3; hence thesis by A1,FUNCT_2:def 2; end; definition let Y,X; redefine func chi(Y,X) -> Multiset of X; coherence by Th30; end; definition let X; let n be Element of NAT; redefine func X --> n -> Multiset of X; coherence proof thus X --> n is Multiset of X by Th27; end; end; definition let A be non empty set, a be Element of A; func chi a -> Multiset of A equals chi({a},A); coherence; end; theorem Th31: for A being non empty set, a,b being Element of A holds (chi a).a = 1 & (b <> a implies (chi a).b = 0) proof let A be non empty set, a,b be Element of A; A1: b <> a implies not b in {a} by TARSKI:def 1; a in {a} by TARSKI:def 1; hence thesis by A1,FUNCT_3:def 3; end; reserve A for non empty set, a for Element of A, p for FinSequence of A, m1,m2 for Multiset of A; theorem Th32: (for a holds m1.a = m2.a) implies m1 = m2 proof assume for a holds m1.a = m2.a; then for x being object st x in A holds m1.x = m2.x; hence thesis by Th20; end; definition let A be set; func finite-MultiSet_over A -> strict non empty MonoidalSubStr of MultiSet_over A means : Def6: for f being Multiset of A holds f in the carrier of it iff f"(NAT\{0}) is finite; existence proof reconsider e = A --> 0 as Function of A,NAT by Th27; defpred P[set] means ex f being Function of A,NAT st \$1 = f & f"(NAT\{0}) is finite; A1: for a,b being Multiset of A holds P[a] & P[b] implies P[a [*] b] proof let a,b be Multiset of A; reconsider h = a [*] b as Function of A,NAT by Th27; given f being Function of A,NAT such that A2: a = f and A3: f"(NAT\{0}) is finite; given g being Function of A,NAT such that A4: b = g and A5: g"(NAT\{0}) is finite; take h; A6: dom f = A & dom g = A by FUNCT_2:def 1; h"(NAT\{0}) c= (f"(NAT\{0})) \/ (g"(NAT\{0})) proof let x be object; assume A7: x in h"(NAT\{0}); then h.x in NAT\{0} by FUNCT_1:def 7; then A8: not h.x in {0} by XBOOLE_0:def 5; f.x in rng f & g.x in rng g by A6,A7,FUNCT_1:def 3; then reconsider n = f.x, m = g.x as Element of NAT; h.x = n+m by A2,A4,A7,Th29; then n <> 0 or m <> 0 by A8,TARSKI:def 1; then not n in {0} or not m in {0} by TARSKI:def 1; then n in NAT\{0} or m in NAT\{0} by XBOOLE_0:def 5; then x in f"(NAT\{0}) or x in g"(NAT\{0}) by A6,A7,FUNCT_1:def 7; hence thesis by XBOOLE_0:def 3; end; hence thesis by A3,A5; end; A9: dom e = A by FUNCOP_1:13; now set x = the Element of e"(NAT\{0}); assume A10: e"(NAT\{0}) <> {}; then e.x in NAT\{0} by FUNCT_1:def 7; then A11: not e.x in {0} by XBOOLE_0:def 5; x in A by A9,A10,FUNCT_1:def 7; then e.x = 0 by FUNCOP_1:7; hence contradiction by A11,TARSKI:def 1; end; then A12: P[1.MultiSet_over A] by Th26; consider M being strict non empty MonoidalSubStr of MultiSet_over A such that A13: for a being Multiset of A holds a in the carrier of M iff P[a] from MONOID_0:sch 2(A1,A12); reconsider M as strict non empty MonoidalSubStr of MultiSet_over A; take M; let f be Multiset of A; thus f in carr(M) implies f"(NAT\{0}) is finite proof assume f in carr(M); then ex g being Function of A,NAT st f = g & g"(NAT\{0}) is finite by A13 ; hence thesis; end; reconsider g = f as Function of A,NAT by Th27; assume f"(NAT\{0}) is finite; then g"(NAT\{0}) is finite; hence thesis by A13; end; uniqueness proof set M = MultiSet_over A; let M1,M2 be strict non empty MonoidalSubStr of MultiSet_over A such that A14: for f being Multiset of A holds f in carr(M1) iff f"(NAT\{0}) is finite and A15: for f being Multiset of A holds f in carr(M2) iff f"(NAT\{0}) is finite; A16: carr(M2) c= carr(M) by MONOID_0:23; A17: carr(M1) c= carr(M) by MONOID_0:23; carr(M1) = carr(M2) proof thus carr(M1) c= carr(M2) proof let x be object; assume A18: x in carr(M1); then reconsider f = x as Multiset of A by A17; f"(NAT\{0}) is finite by A14,A18; hence thesis by A15; end; let x be object; assume A19: x in carr(M2); then reconsider f = x as Multiset of A by A16; f"(NAT\{0}) is finite by A15,A19; hence thesis by A14; end; hence thesis by MONOID_0:27; end; end; theorem Th33: chi a is Element of finite-MultiSet_over A proof (chi a)"(NAT\{0}) c= {a} proof let x be object; assume A1: x in (chi a)"(NAT\{0}); then x in dom chi a by FUNCT_1:def 7; then reconsider y = x as Element of A by Th28; (chi a).x in NAT\{0} by A1,FUNCT_1:def 7; then not (chi a).y in {0} by XBOOLE_0:def 5; then (chi a).y <> 0 by TARSKI:def 1; then y = a by Th31; hence thesis by TARSKI:def 1; end; hence thesis by Def6; end; theorem Th34: dom ({x}|`(p^<*x*>)) = dom ({x}|`p) \/ {len p+1} proof thus dom ({x}|`(p^<*x*>)) c= dom ({x}|`p) \/ {len p+1} proof let a be object; A1: len <*x*> = 1 by FINSEQ_1:40; A2: Seg len p = dom p by FINSEQ_1:def 3; assume A3: a in dom ({x}|`(p^<*x*>)); then A4: a in dom (p^<*x*>) by FUNCT_1:54; then a in Seg (len p+len <*x*>) by FINSEQ_1:def 7; then a in Seg len p \/ {len p+1} by A1,FINSEQ_1:9; then A5: a in dom p or a in {len p+1} by A2,XBOOLE_0:def 3; A6: (p^<*x*>).a in {x} by A3,FUNCT_1:54; reconsider a as Element of NAT by A4; a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7; then a in dom p implies a in dom ({x}|`p) by A6,FUNCT_1:54; hence thesis by A5,XBOOLE_0:def 3; end; let a be object; len <*x*> = 1 by FINSEQ_1:40; then A7: dom (p^<*x*>) = Seg (len p+1) by FINSEQ_1:def 7; assume A8: a in dom ({x}|`p) \/ {len p+1}; then a in dom ({x}|`p) or a in {len p+1} by XBOOLE_0:def 3; then A9: a in dom p & p.a in {x} or a in {len p+1} & a = len p+1 & x in {x} by FUNCT_1:54,TARSKI:def 1; Seg len p = dom p & Seg (len p+1) = Seg len p \/ {len p+1} by FINSEQ_1:9 ,def 3; then A10: (p^<*x*>).(len p+1) = x & a in dom (p^<*x*>) by A9,A7,FINSEQ_1:42 ,XBOOLE_0:def 3; reconsider a as Element of NAT by A8; a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7; hence thesis by A9,A10,FUNCT_1:54; end; theorem Th35: x <> y implies dom ({x}|`(p^<*y*>)) = dom ({x}|`p) proof assume A1: x <> y; thus dom ({x}|`(p^<*y*>)) c= dom ({x}|`p) proof let a be object; A2: len <*y*> = 1 by FINSEQ_1:40; A3: Seg len p = dom p by FINSEQ_1:def 3; assume A4: a in dom ({x}|`(p^<*y*>)); then A5: a in dom (p^<*y*>) by FUNCT_1:54; then a in Seg (len p+len <*y*>) by FINSEQ_1:def 7; then a in Seg len p \/ {len p+1} by A2,FINSEQ_1:9; then A6: a in dom p or a in {len p+1} by A3,XBOOLE_0:def 3; A7: (p^<*y*>).a in {x} by A4,FUNCT_1:54; reconsider a as Element of NAT by A5; A8: (p^<*y*>).(len p+1) = y & not y in {x} by A1,FINSEQ_1:42,TARSKI:def 1; then (p^<*y*>).a = p.a by A7,A6,FINSEQ_1:def 7,TARSKI:def 1; hence thesis by A7,A6,A8,FUNCT_1:54,TARSKI:def 1; end; let a be object; assume A9: a in dom ({x}|`p); then A10: a in dom p by FUNCT_1:54; len <*y*> = 1 by FINSEQ_1:40; then A11: dom (p^<*y*>) = Seg (len p+1) by FINSEQ_1:def 7; Seg len p = dom p & Seg (len p+1) = Seg len p \/ {len p+1} by FINSEQ_1:9 ,def 3; then A12: a in dom (p^<*y*>) by A10,A11,XBOOLE_0:def 3; A13: p.a in {x} by A9,FUNCT_1:54; reconsider a as Element of NAT by A9; (p^<*y*>).a = p.a by A10,FINSEQ_1:def 7; hence thesis by A13,A12,FUNCT_1:54; end; definition let A be non empty set, p be FinSequence of A; func |.p.| -> Multiset of A means : Def7: for a being Element of A holds it. a = card dom ({a}|`p); existence proof deffunc F(Element of A)=card dom ({\$1}|`p); consider m being Function of A,NAT such that A1: for a being Element of A holds m.a = F(a) from FUNCT_2:sch 4; m is Multiset of A by Th27; hence thesis by A1; end; uniqueness proof let m1, m2 be Multiset of A such that A2: for a being Element of A holds m1.a = card dom ({a}|`p) and A3: for a being Element of A holds m2.a = card dom ({a}|`p); now let a be Element of A; thus m1.a = card dom ({a}|`p) by A2 .= m2.a by A3; end; hence thesis by Th32; end; end; theorem |.<*> A.|.a = 0 proof dom ({a}|`{}) c= dom {} by FUNCT_1:56; then dom ({a}|`<*> A) = {}; hence thesis by Def7,CARD_1:27; end; theorem Th37: |.<*> A.| = A --> 0 proof A1: now let x be object; assume x in A; then reconsider a = x as Element of A; thus |.<*>A.|.x = card dom ({a}|`{}) by Def7 .= 0 by CARD_1:27,RELAT_1:38,107; end; dom |.<*>A.| = A by Th28; hence thesis by A1,FUNCOP_1:11; end; theorem |.<*a*>.| = chi a proof A1: rng <*a*> = {a} by FINSEQ_1:39; now let b be Element of A; set x = b; A2: dom <*a*> = Seg 1 & card Seg 1 = 1 by FINSEQ_1:38,57; a <> x implies {x} misses {a} by ZFMISC_1:11; then A3: a <> x implies {x}/\{a} = {}; A4: (chi a).a = 1 & {a}|`<*a*> = <*a*> by A1,Th31; <*a*> = (rng<*a*>)|`<*a*>; then {x}|`<*a*> = ({x}/\rng<*a*>)|`<*a*> by RELAT_1:96; then x <> a implies {x}|`<*a*> = {} & (chi a).b = 0 by A1,A3,Th31; hence |.<*a*>.|.x = (chi a).x by A2,A4,Def7,CARD_1:27,RELAT_1:38; end; hence thesis by Th32; end; reserve p,q for FinSequence of A; theorem Th39: |.p^<*a*>.| = |.p.| [*] chi a proof now reconsider pa = p^<*a*> as FinSequence of A; let b be Element of A; len p < len p+1 & dom ({b}|`p) c= dom p by FUNCT_1:56,NAT_1:13; then A1: not len p+1 in dom ({b}|`p) by FINSEQ_3:25; A2: |.p^<*a*>.|.b = card dom ({b}|`pa) & |.p.|.b = card dom ({b}|`p) by Def7; A3: a <> b implies dom ({b}|`(p^<*a*>)) = dom ({b}|`p) & (chi a).b = 0 by Th31 ,Th35; A4: (|.p.| [*] chi a).b = (|.p.|.b) + ((chi a).b) by Th29; dom ({a}|`(p^<*a*>)) = dom ({a}|`p) \/ {len p+1} & (chi a).a = 1 by Th31,Th34; hence |.p^<*a*>.|.b = (|.p.| [*] chi a).b by A1,A2,A3,A4,CARD_2:41; end; hence thesis by Th32; end; theorem Th40: |.p^q.| = |.p.|[*]|.q.| proof defpred P[Nat] means for q st len q = \$1 holds |.p^q.| = |.p.|[*] |.q.|; A1: len q = len q; A2: for n being Nat st P[n] holds P[n+1] proof let n be Nat such that A3: for q st len q = n holds |.p^q.| = |.p.|[*]|.q.|; let q; assume A4: len q = n+1; then q <> {}; then consider r being FinSequence, x being object such that A5: q = r^<*x*> by FINSEQ_1:46; rng <*x*> = {x} by FINSEQ_1:39; then {x} c= rng q by A5,FINSEQ_1:30; then A6: {x} c= A by XBOOLE_1:1; reconsider r as FinSequence of A by A5,FINSEQ_1:36; len <*x*> = 1 by FINSEQ_1:40; then A7: n+1 = len r+1 by A4,A5,FINSEQ_1:22; reconsider x as Element of A by A6,ZFMISC_1:31; thus |.p^q.| = |.p^r^<*x*>.| by A5,FINSEQ_1:32 .= |.p^r.|[*] chi x by Th39 .= |.p.|[*]|.r.|[*] chi x by A3,A7 .= |.p.|[*](|.r.|[*] chi x) by GROUP_1:def 3 .= |.p.|[*]|.q.| by A5,Th39; end; A8: P[0] proof let q; A9: |.<*>A.| = A-->0 & A-->0 = un(MultiSet_over A) by Th26,Th37; assume len q = 0; then A10: q = {}; then p^q = p by FINSEQ_1:34; hence thesis by A10,A9,MONOID_0:16; end; for n being Nat holds P[n] from NAT_1:sch 2(A8,A2); hence thesis by A1; end; theorem Th41: |.n .--> a.|.a = n & for b being Element of A st b <> a holds |. n .--> a.|.b = 0 proof defpred P[Nat] means |.In(\$1,NAT) .--> a.|.a = \$1; A1: 0.-->a = {} & {} = <*>A by FINSEQ_2:58; A2: for n being Nat st P[n] holds P[n+1] proof let n be Nat such that A3: |.In(n,NAT) .--> a.|.a = n; thus |.In(n+1,NAT) .--> a.|.a = |.(In(n,NAT) .--> a)^<*a*>.|.a by FINSEQ_2:60 .= (|.In(n,NAT) .--> a.|[*]chi a).a by Th39 .= n+(chi a).a by A3,Th29 .= n+1 by Th31; end; (A-->0).a = 0 by FUNCOP_1:7; then A4: P[0] by A1,Th37; for n being Nat holds P[n] from NAT_1:sch 2(A4,A2); then |.In(n,NAT) .--> a.|.a = n; hence |.n .--> a.|.a = n; let b be Element of A such that A5: b <> a; defpred P[Nat] means |.In(\$1,NAT) .--> a.|.b = 0; A6: for n being Nat st P[n] holds P[(n+1)] proof let n be Nat such that A7: |.In(n,NAT) .--> a.|.b = 0; thus |.In(n+1,NAT) .--> a.|.b = |.(In(n,NAT) .--> a)^<*a*>.|.b by FINSEQ_2:60 .= (|.In(n,NAT) .--> a.|[*]chi a).b by Th39 .= 0+(chi a).b by A7,Th29 .= 0 by A5,Th31; end; (A-->0).b = 0 by FUNCOP_1:7; then A8: P[0] by A1,Th37; for n being Nat holds P[n] from NAT_1:sch 2(A8,A6); then P[n]; hence thesis; end; reserve fm for Element of finite-MultiSet_over A; theorem |.p.| is Element of finite-MultiSet_over A proof defpred P[FinSequence of A] means |.\$1.| is Element of finite-MultiSet_over A; defpred Q[Nat] means for p st len p = \$1 holds P[p]; A1: len p = len p; A2: for n being Nat st Q[n] holds Q[n+1] proof set M = finite-MultiSet_over A; let n be Nat such that A3: for p st len p = n holds P[p]; let p; assume A4: len p = n+1; then p <> {}; then consider r being FinSequence, x being object such that A5: p = r^<*x*> by FINSEQ_1:46; rng <*x*> = {x} by FINSEQ_1:39; then {x} c= rng p by A5,FINSEQ_1:30; then A6: {x} c= A by XBOOLE_1:1; reconsider r as FinSequence of A by A5,FINSEQ_1:36; A7: len <*x*> = 1 by FINSEQ_1:40; reconsider x as Element of A by A6,ZFMISC_1:31; n+1 = len r+1 by A4,A5,A7,FINSEQ_1:22; then reconsider r9 = |.r.|, a = chi x as Element of M by A3,Th33; M is SubStr of MultiSet_over A by MONOID_0:21; then r9[*]a = |.r.|[*]chi x by MONOID_0:25 .= |.p.| by A5,Th39; hence thesis; end; A8: Q[0] proof let p; assume len p = 0; then p = <*> A; then |.p.| = A --> 0 by Th37 .= un(MultiSet_over A) by Th26 .= un(finite-MultiSet_over A) by MONOID_0:def 24; hence thesis; end; for n being Nat holds Q[n] from NAT_1:sch 2(A8,A2); hence thesis by A1; end; theorem x is Element of finite-MultiSet_over A implies ex p st x = |.p.| proof defpred Z[Nat] means for fm st for V being finite set st V = fm"( NAT\{0}) holds card V = \$1 ex p st fm = |.p.|; assume x is Element of finite-MultiSet_over A; then reconsider m = x as Element of finite-MultiSet_over A; carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23; then m is Multiset of A; then reconsider V = m"(NAT\{0}) as finite set by Def6; A1: for V9 being finite set st V9 = m"(NAT\{0}) holds card V9 = card V; A2: for n being Nat st Z[n] holds Z[n+1] proof deffunc F(object) = 0; let n be Nat such that A3: for fm st for V being finite set st V = fm"(NAT\{0}) holds card V = n ex p st fm = |.p.|; let fm such that A4: for V being finite set st V = fm"(NAT\{0}) holds card V = n+1; deffunc G(object) = fm.\$1; set x = the Element of fm"(NAT\{0}); carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23; then reconsider m = fm as Multiset of A; reconsider V = m"(NAT\{0}) as finite set by Def6; A5: card V = n+1 by A4; A6: dom m = A by Th28; then reconsider x as Element of A by A5,CARD_1:27,FUNCT_1:def 7; defpred C[object] means x = \$1; consider f being Function such that A7: dom f = A & for a being object st a in A holds (C[a] implies f.a = F (a)) & (not C[a] implies f.a = G(a)) from PARTFUN1:sch 1; rng f c= NAT proof let y be object; assume y in rng f; then consider z being object such that A8: z in dom f and A9: y = f.z by FUNCT_1:def 3; reconsider z as Element of A by A7,A8; y = 0 or y = m.z by A7,A9; hence thesis; end; then reconsider f as Function of A,NAT by A7,FUNCT_2:def 1,RELSET_1:4; reconsider f as Multiset of A by Th27; A10: f"(NAT\{0}) = (fm"(NAT\{0}))\{x} proof thus f"(NAT\{0}) c= (fm"(NAT\{0}))\{x} proof let y be object; assume A11: y in f"(NAT\{0}); then reconsider a = y as Element of A by A7,FUNCT_1:def 7; A12: f.y in NAT\{0} by A11,FUNCT_1:def 7; then not f.a in {0} by XBOOLE_0:def 5; then A13: f.a <> 0 by TARSKI:def 1; then a <> x by A7; then A14: not a in {x} by TARSKI:def 1; f.a = fm.a by A7,A13; then a in fm"(NAT\{0}) by A6,A12,FUNCT_1:def 7; hence thesis by A14,XBOOLE_0:def 5; end; let y be object; assume A15: y in (fm"(NAT\{0}))\{x}; then A16: y in dom fm by FUNCT_1:def 7; A17: fm.y in NAT\{0} by A15,FUNCT_1:def 7; not y in {x} by A15,XBOOLE_0:def 5; then y <> x by TARSKI:def 1; then fm.y = f.y by A6,A7,A16; hence thesis by A6,A7,A16,A17,FUNCT_1:def 7; end; then reconsider f9 = f as Element of finite-MultiSet_over A by A5,Def6; set g = |.(m.x) .--> x.|; A18: card {x} = 1 by CARD_1:30; reconsider V9 = f9"(NAT\{0}) as finite set by Def6; {x} c= fm"(NAT\{0}) by A5,CARD_1:27,ZFMISC_1:31; then card V9 = n+1-1 by A5,A10,A18,CARD_2:44 .= n; then for V being finite set st V = f9"(NAT\{0}) holds card V = n; then consider p such that A19: f = |.p.| by A3; take q = p^((m.x) .--> x); now let a; A20: 0 + m.a = m.a; A21: a <> x implies f.a = m.a & g.a = 0 by A7,Th41; f.x = 0 & g.x = m.x by A7,Th41; hence (f[*]g).a = m.a by A20,A21,Th29; end; hence fm = f[*]g by Th32 .= |.q.| by A19,Th40; end; A22: Z[0] proof set a = the Element of A; let fm such that A23: for V being finite set st V = fm"(NAT\{0}) holds card V = 0; carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23; then reconsider m = fm as Multiset of A; reconsider V = m"(NAT\{0}) as finite set by Def6; card V = 0 by A23; then fm"(NAT\{0}) = {}; then rng fm misses (NAT\{0}) by RELAT_1:138; then A24: {} = rng fm /\ (NAT\{0}) .= (rng fm /\ NAT)\{0} by XBOOLE_1:49; take p = <*> A; rng m c= NAT; then rng fm /\ NAT = rng fm by XBOOLE_1:28; then A25: rng fm c= {0} by A24,XBOOLE_1:37; A26: dom m = A by Th28; then A27: fm.a in rng fm by FUNCT_1:def 3; then fm.a = 0 by A25,TARSKI:def 1; then {0} c= rng fm by A27,ZFMISC_1:31; then rng fm = {0} by A25; hence fm = A --> 0 by A26,FUNCOP_1:9 .= |.p.| by Th37; end; for n being Nat holds Z[n] from NAT_1:sch 2(A22,A2); hence thesis by A1; end; begin :: Monoid of subsets of a semigroup reserve a,b,c for Element of D; definition let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; func f.:^2 -> Function of [:bool D1, bool D2:], bool D means : Def8: for x being Element of [:bool D1, bool D2:] holds it.x = f.:[:x`1,x`2:]; existence proof deffunc F(Element of [:bool D1, bool D2:]) = f.:[:\$1`1,\$1`2:]; ex f being Function of [:bool D1,bool D2:],bool D st for x being Element of [:bool D1, bool D2:] holds f.x = F(x) from FUNCT_2:sch 4; hence thesis; end; uniqueness proof let F1,F2 be Function of [:bool D1, bool D2:], bool D such that A1: for x being Element of [:bool D1, bool D2:] holds F1.x = f.:[:x`1, x`2:] and A2: for x being Element of [:bool D1, bool D2:] holds F2.x = f.:[:x`1, x`2:]; now let x be Element of [:bool D1, bool D2:]; thus F1.x = f.:[:x`1,x`2:] by A1 .= F2.x by A2; end; hence thesis by FUNCT_2:63; end; end; theorem Th44: for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for X1 being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = f.:[:X1,X2 :] proof let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let X1 be Subset of D1, X2 be Subset of D2; [X1,X2]`1 = X1 & [X1,X2]`2 = X2; hence thesis by Def8; end; theorem Th45: for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for X1 being Subset of D1, X2 being Subset of D2, x1,x2 being set st x1 in X1 & x2 in X2 holds f.(x1,x2) in (f.:^2).(X1,X2) proof let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let X1 be Subset of D1, X2 be Subset of D2, x1,x2 be set; assume that A1: x1 in X1 and A2: x2 in X2; reconsider b = x2 as Element of D2 by A2; reconsider a = x1 as Element of D1 by A1; A3: (f.:^2).(X1,X2) = f.:[:X1,X2:] & dom f = [:D1,D2:] by Th44,FUNCT_2:def 1; [a,b] in [:X1,X2:] by A1,A2,ZFMISC_1:87; hence thesis by A3,FUNCT_1:def 6; end; theorem for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for X1 being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = {f.(a,b) where a is Element of D1, b is Element of D2: a in X1 & b in X2} proof let D1,D2,D be non empty set, f be Function of [:D1,D2:],D; let X1 be Subset of D1, X2 be Subset of D2; set A = {f.(a,b) where a is Element of D1, b is Element of D2: a in X1 & b in X2}; A1: (f.:^2).(X1,X2) = f.:[:X1,X2:] by Th44; thus (f.:^2).(X1,X2) c= A proof let x be object; assume x in f.:^2.(X1,X2); then consider y being object such that y in dom f and A2: y in [:X1,X2:] and A3: x = f.y by A1,FUNCT_1:def 6; consider y1,y2 being object such that A4: y1 in X1 and A5: y2 in X2 and A6: y = [y1,y2] by A2,ZFMISC_1:84; reconsider y2 as Element of D2 by A5; reconsider y1 as Element of D1 by A4; x = f.(y1,y2) by A3,A6; hence thesis by A4,A5; end; let x be object; assume x in A; then ex a being Element of D1, b being Element of D2 st x = f.(a,b) & a in X1 & b in X2; hence thesis by Th45; end; theorem Th47: o is commutative implies o.:[:X,Y:] = o.:[:Y,X:] proof assume A1: o.(a,b) = o.(b,a); now let X,Y; thus o.:[:X,Y:] c= o.:[:Y,X:] proof let x be object; assume x in o.:[:X,Y:]; then consider y being object such that A2: y in dom o and A3: y in [:X,Y:] and A4: x = o.y by FUNCT_1:def 6; reconsider y as Element of [:D,D:] by A2; y = [y`1,y`2] by MCART_1:21; then y`1 in X & y`2 in Y by A3,ZFMISC_1:87; then A5: [y`2,y`1] in [:Y,X:] by ZFMISC_1:87; A6: dom o = [:D,D:] & o.(y`1,y`2) = o.(y`2,y`1 ) by A1,FUNCT_2:def 1; x = o.(y`1,y`2) by A4,MCART_1:21; hence thesis by A6,A5,FUNCT_1:def 6; end; end; hence o.:[:X,Y:] c= o.:[:Y,X:] & o.:[:Y,X:] c= o.:[:X,Y:]; end; theorem Th48: o is associative implies o.:[:o.:[:X,Y:],Z:] = o.:[:X,o.:[:Y,Z:] :] proof A1: dom o = [:D,D:] by FUNCT_2:def 1; assume A2: o.(o.(a,b),c) = o.(a,o.(b,c)); thus o.:[:o.:[:X,Y:],Z:] c= o.:[:X,o.:[:Y,Z:]:] proof let x be object; assume x in o.:[:o.:[:X,Y:],Z:]; then consider y being object such that A3: y in dom o and A4: y in [:o.:[:X,Y:],Z:] and A5: x = o.y by FUNCT_1:def 6; reconsider y as Element of [:D,D:] by A3; A6: y = [y`1,y`2] by MCART_1:21; then A7: y`2 in Z by A4,ZFMISC_1:87; y`1 in o.:[:X,Y:] by A4,A6,ZFMISC_1:87; then consider z being object such that A8: z in dom o and A9: z in [:X,Y:] and A10: y`1 = o.z by FUNCT_1:def 6; reconsider z as Element of [:D,D:] by A8; A11: y`1 = o.(z`1,z`2) by A10,MCART_1:21; A12: z = [z`1,z`2] by MCART_1:21; then z`2 in Y by A9,ZFMISC_1:87; then [z`2,y`2] in [:Y,Z:] by A7,ZFMISC_1:87; then A13: o.(z`2,y`2) in o.:[:Y,Z:] by A1,FUNCT_1:def 6; z`1 in X by A9,A12,ZFMISC_1:87; then A14: [z`1,o.(z`2,y`2)] in [:X,o.:[:Y,Z:]:] by A13,ZFMISC_1:87; x = o.(y`1,y`2) by A5,MCART_1:21; then x = o.(z`1,o.(z`2,y`2)) by A2,A11; hence thesis by A1,A14,FUNCT_1:def 6; end; let x be object; assume x in o.:[:X,o.:[:Y,Z:]:]; then consider y being object such that A15: y in dom o and A16: y in [:X,o.:[:Y,Z:]:] and A17: x = o.y by FUNCT_1:def 6; reconsider y as Element of [:D,D:] by A15; A18: y = [y`1,y`2] by MCART_1:21; then A19: y`1 in X by A16,ZFMISC_1:87; y`2 in o.:[:Y,Z:] by A16,A18,ZFMISC_1:87; then consider z being object such that A20: z in dom o and A21: z in [:Y,Z:] and A22: y`2 = o.z by FUNCT_1:def 6; reconsider z as Element of [:D,D:] by A20; A23: y`2 = o.(z`1,z`2) by A22,MCART_1:21; A24: z = [z`1,z`2] by MCART_1:21; then z`1 in Y by A21,ZFMISC_1:87; then [y`1,z`1] in [:X,Y:] by A19,ZFMISC_1:87; then A25: o.(y`1,z`1) in o.:[:X,Y:] by A1,FUNCT_1:def 6; z`2 in Z by A21,A24,ZFMISC_1:87; then A26: [o.(y`1,z`1),z`2] in [:o.:[:X,Y:],Z:] by A25,ZFMISC_1:87; x = o.(y`1,y`2) by A17,MCART_1:21; then x = o.(o.(y`1,z`1),z`2) by A2,A23; hence thesis by A1,A26,FUNCT_1:def 6; end; theorem Th49: o is commutative implies o.:^2 is commutative proof assume A1: o is commutative; let x,y be Subset of D; thus (o.:^2).(x,y) = o.:[:x,y:] by Th44 .= o.:[:y,x:] by A1,Th47 .= (o.:^2).(y,x) by Th44; end; theorem Th50: o is associative implies o.:^2 is associative proof assume A1: o is associative; let x,y,z be Subset of D; thus (o.:^2).((o.:^2).(x,y),z) = (o.:^2).(o.:[:x,y:],z) by Th44 .= o.:[:o.:[:x,y:],z:] by Th44 .= o.:[:x,o.:[:y,z:]:] by A1,Th48 .= (o.:^2).(x,o.:[:y,z:]) by Th44 .= (o.:^2).(x,(o.:^2).(y,z)) by Th44; end; theorem Th51: a is_a_unity_wrt o implies o.:[:{a},X:] = D /\ X & o.:[:X,{a}:] = D /\ X proof assume A1: a is_a_unity_wrt o; thus o.:[:{a},X:] c= D /\ X proof let x be object; assume x in o.:[:{a},X:]; then consider y being object such that A2: y in dom o and A3: y in [:{a},X:] and A4: x = o.y by FUNCT_1:def 6; reconsider y as Element of [:D,D:] by A2; A5: x = o.(y`1,y`2) by A4,MCART_1:21; A6: y = [y`1,y`2] by MCART_1:21; then y`1 in {a} by A3,ZFMISC_1:87; then A7: y`1 = a by TARSKI:def 1; A8: o.(a,y`2) = y`2 by A1,BINOP_1:3; y`2 in X by A3,A6,ZFMISC_1:87; hence thesis by A5,A8,A7,XBOOLE_0:def 4; end; A9: dom o = [:D,D:] by FUNCT_2:def 1; thus D /\ X c= o.:[:{a},X:] proof let x be object; A10: a in {a} by TARSKI:def 1; assume A11: x in D /\ X; then reconsider d = x as Element of D by XBOOLE_0:def 4; A12: x = o.(a,d) by A1,BINOP_1:3 .= o.[a,x]; x in X by A11,XBOOLE_0:def 4; then [a,d] in [:{a},X:] by A10,ZFMISC_1:87; hence thesis by A9,A12,FUNCT_1:def 6; end; thus o.:[:X,{a}:] c= D /\ X proof let x be object; assume x in o.:[:X,{a}:]; then consider y being object such that A13: y in dom o and A14: y in [:X,{a}:] and A15: x = o.y by FUNCT_1:def 6; reconsider y as Element of [:D,D:] by A13; A16: x = o.(y`1,y`2) by A15,MCART_1:21; A17: y = [y`1,y`2] by MCART_1:21; then y`2 in {a} by A14,ZFMISC_1:87; then A18: y`2 = a by TARSKI:def 1; A19: o.(y`1,a) = y`1 by A1,BINOP_1:3; y`1 in X by A14,A17,ZFMISC_1:87; hence thesis by A16,A19,A18,XBOOLE_0:def 4; end; thus D /\ X c= o.:[:X,{a}:] proof let x be object; A20: a in {a} by TARSKI:def 1; assume A21: x in D /\ X; then reconsider d = x as Element of D by XBOOLE_0:def 4; A22: x = o.(d,a) by A1,BINOP_1:3 .= o.[x,a]; x in X by A21,XBOOLE_0:def 4; then [d,a] in [:X,{a}:] by A20,ZFMISC_1:87; hence thesis by A9,A22,FUNCT_1:def 6; end; end; theorem Th52: a is_a_unity_wrt o implies {a} is_a_unity_wrt o.:^2 & o.:^2 is having_a_unity & the_unity_wrt o.:^2 = {a} proof assume A1: a is_a_unity_wrt o; now let x be Subset of D; thus (o.:^2).({a},x) = o.:[:{a},x:] by Th44 .= D /\ x by A1,Th51 .= x by XBOOLE_1:28; thus (o.:^2).(x,{a}) = o.:[:x,{a}:] by Th44 .= D /\ x by A1,Th51 .= x by XBOOLE_1:28; end; hence A2: {a} is_a_unity_wrt o.:^2 by BINOP_1:3; hence ex A being Subset of D st A is_a_unity_wrt o.:^2; thus thesis by A2,BINOP_1:def 8; end; theorem Th53: o is having_a_unity implies o.:^2 is having_a_unity & { the_unity_wrt o} is_a_unity_wrt o.:^2 & the_unity_wrt o.:^2 = {the_unity_wrt o} proof given a such that A1: a is_a_unity_wrt o; a = the_unity_wrt o by A1,BINOP_1:def 8; hence thesis by A1,Th52; end; theorem Th54: o is uniquely-decomposable implies o.:^2 is uniquely-decomposable proof assume that A1: o is having_a_unity and A2: o.(a,b) = the_unity_wrt o implies a = b & b = the_unity_wrt o; thus o.:^2 is having_a_unity by A1,Th53; let A,B be Subset of D such that A3: (o.:^2).(A,B) = the_unity_wrt o.:^2; set a = the_unity_wrt o; A4: the_unity_wrt o.:^2 = {a} by A1,Th53; set a1 = the Element of A,a2 = the Element of B; o.:[:A,B:] = (o.:^2).(A,B) by Th44; then dom o meets [:A,B:] by A3,A4,RELAT_1:118; then dom o /\ [:A,B:] <> {}; then A5: [:A,B:] <> {}; then A6: A <> {} by ZFMISC_1:90; A7: B <> {} by A5,ZFMISC_1:90; then reconsider a1,a2 as Element of D by A6,TARSKI:def 3; A8: {a1} c= A by A6,ZFMISC_1:31; o.(a1,a2) in {a} by A3,A4,A6,A7,Th45; then A9: o.(a1,a2) = a by TARSKI:def 1; then A10: a2 = a by A2; A11: A c= {a} proof let x be object; assume A12: x in A; then reconsider c = x as Element of D; o.(c,a2) in {a} by A3,A4,A7,A12,Th45; then o.(c,a2) = a by TARSKI:def 1; then c = a2 by A2; hence thesis by A10,TARSKI:def 1; end; A13: B c= {a} proof let x be object; assume A14: x in B; then reconsider c = x as Element of D; o.(a1,c) in {a} by A3,A4,A6,A14,Th45; then o.(a1,c) = a by TARSKI:def 1; then c = a by A2; hence thesis by TARSKI:def 1; end; A15: a1 = a2 by A2,A9; {a2} c= B by A7,ZFMISC_1:31; then B = {a} by A10,A13; hence thesis by A1,A15,A10,A8,A11,Th53; end; definition let G be non empty multMagma; func bool G -> multMagma equals : Def9: multLoopStr(#bool the carrier of G, (the multF of G).:^2, {the_unity_wrt the multF of G}#) if G is unital otherwise multMagma(#bool the carrier of G, (the multF of G).:^2#); correctness; end; registration let G be non empty multMagma; cluster bool G -> non empty; coherence proof per cases; suppose G is unital; then bool G = multLoopStr(#bool the carrier of G, (the multF of G).:^2, { the_unity_wrt the multF of G}#) by Def9; hence the carrier of bool G is non empty; end; suppose G is not unital; then bool G = multMagma(#bool the carrier of G, (the multF of G).:^2#) by Def9 ; hence the carrier of bool G is non empty; end; end; end; definition let G be unital non empty multMagma; redefine func bool G -> well-unital strict non empty multLoopStr; coherence proof set M = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#); op(G) is having_a_unity by MONOID_0:def 10; then A1: {the_unity_wrt op(G)} is_a_unity_wrt op(G).:^2 by Th53; 1.M = {the_unity_wrt op(G)} & bool G = M by Def9; hence thesis by A1,MONOID_0:def 21; end; end; theorem Th55: the carrier of bool G = bool the carrier of G & the multF of bool G = (the multF of G).:^2 proof bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#) or bool G = multMagma(#bool the carrier of G, op(G).:^2#) by Def9; hence thesis; end; theorem for G being unital non empty multMagma holds 1.bool G = { the_unity_wrt the multF of G} proof let G be unital non empty multMagma; bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#) by Def9 ; hence thesis; end; theorem for G being non empty multMagma holds (G is commutative implies bool G is commutative) & (G is associative implies bool G is associative) & (G is uniquely-decomposable implies bool G is uniquely-decomposable) proof let G be non empty multMagma; A1: op(bool G) = op(G).:^2 & carr(bool G) = bool carr(G) by Th55; thus G is commutative implies bool G is commutative by A1,Th49; thus G is associative implies bool G is associative by A1,Th50; assume op(G) is uniquely-decomposable; hence op(bool G) is uniquely-decomposable by A1,Th54; end;