Copyright (c) 1992 Association of Mizar Users
environ vocabulary VECTSP_1, FUNCT_1, FINSEQ_4, RELAT_1, FUNCT_2, PARTFUN1, FINSEQ_2, FINSEQ_1, CAT_1, FUNCOP_1, BOOLE, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0, LATTICE2, MCART_1, GROUP_1, VECTSP_2, FUNCT_3, FINSET_1, COMPLEX1, CARD_1, ARYTM_1, MONOID_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, MONOID_0, FUNCT_2, BINOP_1, FUNCOP_1, SETWISEO, FINSET_1, FRAENKEL, FUNCT_3, FINSEQ_2, CARD_1, LATTICE2, FUNCT_4, FUNCT_6, VECTSP_1, DOMAIN_1; constructors REAL_1, NAT_1, BINOP_1, FUNCOP_1, SETWISEO, FRAENKEL, FUNCT_3, LATTICE2, FUNCT_6, MONOID_0, DOMAIN_1, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSET_1, MONOID_0, RELAT_1, PRELAMB, STRUCT_0, RELSET_1, FINSEQ_1, FUNCOP_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, BINOP_1, LATTICE2, SETWISEO, MONOID_0, STRUCT_0, XBOOLE_0; theorems TARSKI, NAT_1, FINSET_1, FINSEQ_1, BINOP_1, SETWISEO, MCART_1, FUNCOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3, CARD_1, CARD_2, FINSEQ_2, FINSEQ_3, FUNCT_5, FUNCT_6, BORSUK_1, MONOID_0, VECTSP_1, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes NAT_1, FUNCT_2, MONOID_0, PARTFUN1, COMPTS_1; begin :: Updating reserve x,y,z, X,Y,Z for set, n for Nat; deffunc op(HGrStr) = the mult of $1; deffunc un(multLoopStr) = the unity of $1; definition let D1,D2,D be non empty set; mode Function of D1,D2,D is Function of [:D1,D2:],D; end; definition let f be Function, x1,x2,y be set; func f..(x1,x2,y) equals: Def1: f..([x1,x2],y); correctness; end; theorem Th1: for f,g being Function, x1,x2,x being set st [x1,x2] in dom f & g = f.(x1,x2) & x in dom g holds f..(x1,x2,x) = g.x proof let f,g be Function, x1,x2,x be set; f..(x1,x2,x) = f..([x1,x2],x) & f.(x1,x2) = f.[x1,x2] by Def1,BINOP_1:def 1; hence thesis by FUNCT_6:44; 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); dom f = [:D1,D2:] & dom g = A & [x1,x2] in [:D1,D2:] by FUNCT_2:def 1; then f..(x1,x2,x) = g.x by Th1; 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, RELSET_1:12; hence thesis by FUNCT_2:def 2; end; end; definition let A be non empty set; let n be Nat, x be Element of A; redefine func n |-> x -> FinSequence of A; coherence by FINSEQ_2:77; synonym n .--> x; 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 A1: dom (A --> d) = A & rng (A --> d) c= {d} & {d} c= D by FUNCOP_1:19; then rng (A --> d) c= D by XBOOLE_1:1; hence thesis by A1,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,RELSET_1: 12; 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,RELSET_1: 12; 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 FUNCT_1:68; A2: dom ((f|X)*g) = dom (f*(X|g)) proof thus dom ((f|X)*g) c= dom (f*(X|g)) proof let x; assume x in dom ((f|X)*g); then A3: x in dom g & g.x in dom (f|X) by FUNCT_1:21; then A4: g.x in X & g.x in dom f by A1,XBOOLE_0:def 3; then A5: x in dom (X|g) by A3,FUNCT_1:85; then g.x = (X|g).x by FUNCT_1:85; hence thesis by A4,A5,FUNCT_1:21; end; let x; assume x in dom (f*(X|g)); then x in dom (X|g) & (X|g).x in dom f by FUNCT_1:21; then A6: x in dom g & g.x in X & g.x in dom f by FUNCT_1:85; then g.x in dom (f|X) by A1,XBOOLE_0:def 3; hence thesis by A6,FUNCT_1:21; end; now let x; assume x in dom ((f|X)*g); then ((f|X)*g).x = (f|X).(g.x) & g.x in dom (f|X) & (f*(X|g)).x = f.((X|g).x) & x in dom (X|g) by A2,FUNCT_1:21,22; then ((f|X)*g).x = f.(g.x) & (f*(X|g)).x = f.(g.x) by FUNCT_1:70,85; hence ((f|X)*g).x = (f*(X|g)).x; end; hence thesis by A2,FUNCT_1:9; end; scheme NonUniqFuncDEx { X() -> set, Y() -> non empty set, P[set,set] }: ex f being Function of X(), Y() st for x st x in X() holds P[x,f.x] provided A1: for x st x in X() ex y being Element of Y() st P[x,y] proof defpred Q[set,set] means P[$1,$2]; A2: for x st x in X() ex y st y in Y() & Q[x,y] proof let x; 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 st x in X() holds Q[x,f.x] from NonUniqBoundFuncEx(A2); reconsider f as Function of X(), Y() by A4,FUNCT_2:def 1,RELSET_1:11; 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 Lambda2D; take b; let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2); thus b.(f1,f2) = b.[f1,f2] by BINOP_1:def 1 .= f.:(f1,f2) 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 by BINOP_1:2; 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; let x such that A1: x in A; A2: dom f1 = A & rng f1 c= D1 & dom f2 = A & rng f2 c= D2 by FUNCT_2:def 1,RELSET_1:12; then reconsider f1 as Element of Funcs(A,D1) by FUNCT_2:def 2; reconsider f2 as Element of Funcs(A,D2) by A2,FUNCT_2:def 2; A3: ((f,D).:A).(f1,f2) = f.:(f1,f2) & dom (f.: (f1,f2)) = A & [f1,f2] = [f1,f2] & dom ((f,D).:A) = [:Funcs(A,D1), Funcs(A,D2):] by Def2,FUNCT_2:def 1; then (f.:(f1,f2)).x = f.(f1.x,f2.x) by A1,FUNCOP_1:28; hence thesis by A1,A3,Th1; end; reserve A for set, D for non empty set, a,b,c,l,r for Element of D, o,o' for BinOp of D, f,g,h for Function of A,D; theorem Th4: o is commutative implies o.:(f,g) = o.:(g,f) proof assume A1: o.(a,b) = o.(b,a); A2: dom (o.:(f,g)) = A & dom (o.:(g,f)) = A & dom f = A & rng f c= D & dom g = A & rng g c= D by FUNCT_2:def 1,RELSET_1: 12; now let x; assume A3: x in A; then f.x in rng f & g.x in rng g by A2,FUNCT_1:def 5; then reconsider a = f.x, b = g.x as Element of D by A2; thus (o.:(f,g)).x = o.(a,b) by A2,A3,FUNCOP_1:28 .= o.(b,a) by A1 .= (o.:(g,f)).x by A2,A3,FUNCOP_1:28; end; hence thesis by A2,FUNCT_1:9; end; theorem Th5: o is associative implies o.:(o.:(f,g),h) = o.:(f,o.:(g,h)) proof assume A1: o.(o.(a,b),c) = o.(a,o.(b,c)); A2: dom (o.:(f,g)) = A & dom (o.:(g,h)) = A & dom (o.:(o.:(f,g),h)) = A & dom (o.:(f,o.:(g,h))) = A & dom f = A & rng f c= D & dom g = A & rng g c= D & dom h = A & rng h c= D by FUNCT_2:def 1,RELSET_1:12; now let x; assume A3: x in A; then f.x in rng f & g.x in rng g & h.x in rng h by A2,FUNCT_1:def 5; then reconsider a = f.x, b = g.x, c = h.x as Element of D by A2; thus (o.:(o.:(f,g),h)).x = o.((o.:(f,g)).x,c) by A2,A3,FUNCOP_1:28 .= o.(o.(a,b),c) by A2,A3,FUNCOP_1:28 .= o.(a,o.(b,c)) by A1 .= o.(a,(o.:(g,h)).x) by A2,A3,FUNCOP_1:28 .= (o.:(f,o.:(g,h))).x by A2,A3,FUNCOP_1:28; end; hence thesis by A2,FUNCT_1:9; end; theorem Th6: 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 (o[;](a,f)) = A & dom (o[:](f,a)) = A & dom f = A & rng f c= D by FUNCT_2:def 1,RELSET_1:12; now let x; assume A3: x in A; then f.x in rng f by A2,FUNCT_1:def 5; then reconsider b = f.x as Element of D by A2; thus (o[;](a,f)).x = o.(a,b) by A2,A3,FUNCOP_1:42 .= f.x by A1,BINOP_1:11 ; end; hence o[;](a,f) = f by A2,FUNCT_1:9; now let x; assume A4: x in A; then f.x in rng f by A2,FUNCT_1:def 5; then reconsider b = f.x as Element of D by A2; thus (o[:](f,a)).x = o.(b,a) by A2,A4,FUNCOP_1:35 .= f.x by A1,BINOP_1:11 ; end; hence o[:](f,a) = f by A2,FUNCT_1:9; end; theorem Th7: o is idempotent implies o.:(f,f) = f proof assume A1: o.(a,a) = a; A2: dom f = A & dom (o.:(f,f)) = A by FUNCT_2:def 1; now let x; assume A3: x in A; then reconsider a = f.x as Element of D by FUNCT_2:7; thus o.:(f,f).x = o.(a,a) by A2,A3,FUNCOP_1:28 .= f.x by A1; end; hence thesis by A2,FUNCT_1:9; end; theorem Th8: o is commutative implies (o,D).:A is commutative proof assume A1: o is commutative; let f,g be Element of Funcs(A,D); set h = (o,D).:A; thus h.(f,g) = o.:(f, g) by Def2 .= o.:(g, f) by A1,Th4 .= h.(g,f) by Def2; end; theorem Th9: o is associative implies (o,D).:A is associative proof assume A1: o is associative; let f,g,h be Element of Funcs(A,D); set F = (o,D).:A; 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,Th5 .= F.(f,o.:(g,h)) by Def2 .= F.(f,F.(g,h)) by Def2; end; theorem Th10: a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D).:A proof assume A1: a is_a_unity_wrt o; set e = A --> a; set F = (o,D).:A; 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:41 .= f by A1,Th6; thus F.(f,e) = o.:(f,e) by Def2 .= o[:](f,a) by A2,FUNCOP_1:34 .= f by A1,Th6; end; hence thesis by BINOP_1:11; end; theorem Th11: o has_a_unity implies the_unity_wrt (o,D).:A = A --> the_unity_wrt o & (o,D).:A has_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,Th10,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,Th10; end; theorem Th12: 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,Th7; end; theorem Th13: 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[set,set] means o.(f.$1,$2) = g.$1; A2: for x st x in A ex c st P[x,c] proof let x; assume x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7 ; consider r,l such that A3: o.(a,r) = b & o.(l,a) = b by A1; take r; thus thesis by A3; end; defpred Q[set,set] means o.($2,f.$1) = g.$1; A4: for x st x in A ex c st Q[x,c] proof let x; assume x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7; consider r,l such that A5: o.(a,r) = b & o.(l,a) = b by A1; take l; thus thesis by A5; end; consider h1 being Function of A,D such that A6: for x st x in A holds P[x,h1.x] from NonUniqFuncDEx(A2); consider h2 being Function of A,D such that A7: for x st x in A holds Q[x,h2.x] from NonUniqFuncDEx(A4); dom h1 = A & dom h2 = A & rng h1 c= D & rng h2 c= D by FUNCT_2:def 1, RELSET_1:12; then reconsider h1, h2 as Element of Funcs(A,D) by FUNCT_2:def 2; take h1, h2; A8: dom (o.:(f,h1)) = A & dom (o.:(h2,f)) = A & dom g = A & o.:(f,h1) = ((o,D).:A).(f,h1) & o.:(h2,f) = ((o,D).:A).(h2,f) by Def2,FUNCT_2:def 1; now let x; assume A9: x in A; hence o.:(f,h1).x = o.(f.x,h1.x) by A8,FUNCOP_1:28 .= g.x by A6,A9; end; hence ((o,D).:A).(f,h1) = g by A8,FUNCT_1:9; now let x; assume A10: x in A; hence o.:(h2,f).x = o.(h2.x,f.x) by A8,FUNCOP_1:28 .= g.x by A7,A10; end; hence ((o,D).:A).(h2,f) = g by A8,FUNCT_1:9; end; theorem Th14: 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: (o,D).:A.(f,g) = o.:(f,g) & (o,D).:A.(g,f) = o.:(g,f) & (o,D).:A.(f,h) = o.:(f,h) & (o,D).:A.(h,f) = o.:(h,f) by Def2; A4: A = dom (o.:(f,g)) & A = dom (o.:(g,f)) & A = dom (o.:(f,h)) & A = dom (o.:(h,f)) & dom g = A & dom h = A by FUNCT_2:def 1; now let x; assume A5: x in A; then reconsider a = f.x, b = g.x, c = h.x as Element of D by FUNCT_2:7; o.:(f,g).x = o.(a,b) & o.:(f,h).x = o.(a,c) & o.:(g,f).x = o.(b,a) & o.:(h,f).x = o.(c,a) by A4,A5,FUNCOP_1:28; hence g.x = h.x by A1,A2,A3; end; hence thesis by A4,FUNCT_1:9; end; theorem Th15: o is uniquely-decomposable implies (o,D).:A is uniquely-decomposable proof assume A1: o has_a_unity & for a,b st o.(a,b) = the_unity_wrt o holds a = b & b = the_unity_wrt o; hence (o,D).:A has_a_unity by Th11; let f,g be Element of Funcs(A,D) such that A2: (o,D).:A.(f,g) = the_unity_wrt (o,D).:A; A3: (o,D).:A.(f,g) = o.:(f,g) & the_unity_wrt (o,D).:A = A --> the_unity_wrt o by A1,Def2,Th11; A4: dom (A --> the_unity_wrt o) = A & dom f = A & dom g = A & dom (o.:(f,g)) = A by FUNCT_2:def 1; now let x; assume A5: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7 ; (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o by A4,A5,FUNCOP_1:13,28; hence f.x = g.x by A1,A2,A3; end; hence f = g by A4,FUNCT_1:9; now let x; assume A6: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7 ; (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o by A4,A6,FUNCOP_1:13,28; hence g.x = (A --> the_unity_wrt o).x by A1,A2,A3; end; hence thesis by A3,A4,FUNCT_1:9; end; theorem o absorbs o' implies (o,D).:A absorbs (o',D).:A proof assume A1: o.(a,o'.(a,b)) = a; let f,g be Element of Funcs(A,D); A2: ((o',D).:A).(f,g) = o'.:(f,g) & ((o,D).:A).(f,o'.:(f,g)) = o.:(f,o'.: (f,g)) by Def2; A3: dom f = A & dom g = A & dom (o'.:(f,g)) = A & dom (o.:(f,o'.:(f,g))) = A by FUNCT_2:def 1; now let x; assume A4: x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7; (o.:(f,o'.:(f,g))).x = o.(a,(o'.:(f,g)).x) & (o'.:(f,g)).x = o'.(a,b) by A3,A4,FUNCOP_1:28; hence f.x = (o.:(f,o'.:(f,g))).x by A1; end; hence thesis by A2,A3,FUNCT_1:9; end; theorem Th17: 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 <= o2 holds (o1,D).:A <= (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; assume A1: o1 <= o2; then A2: dom o1 c= dom o2 & dom o1 = [:D1,D2:] & dom o2 = [:E1,E2:] & dom (o1,D).:A = [:Funcs(A,D1),Funcs(A,D2):] & dom (o2,E).:A = [:Funcs(A,E1),Funcs(A,E2):] & for x st x in dom o1 holds o1.x = o2.x by FUNCT_2:def 1,GRFUNC_1:8; then D1 c= E1 & D2 c= E2 by BORSUK_1:7; then A3: Funcs(A,D1) c= Funcs(A,E1) & Funcs(A,D2) c= Funcs(A,E2) by FUNCT_5:63 ; then A4: dom (o1,D).:A c= dom (o2,E).:A by A2,ZFMISC_1:119; now let x; assume x in dom (o1,D).:A; then reconsider y = x as Element of [:Funcs(A,D1),Funcs(A,D2):] by FUNCT_2 :def 1; reconsider f1 = y`1 as Element of Funcs(A,D1); reconsider g1 = y`1 as Element of Funcs(A,E1) by A3,TARSKI:def 3; reconsider f2 = y`2 as Element of Funcs(A,D2); reconsider g2 = y`2 as Element of Funcs(A,E2) by A3,TARSKI:def 3; A5: ((o1,D).:A).(f1,f2) = o1.:(f1,f2) & ((o2,E).:A).(g1,g2) = o2.:(g1,g2) & rng f1 c= D1 & rng f2 c= D2 & dom f1 = A & dom f2 = A & dom (o2.:(g1,g2)) = A & dom (o1.:(f1,f2)) = A by Def2,FUNCT_2:def 1, RELSET_1:12; now let z be set; assume z in A; then A6: (o2.:(g1,g2)).z = o2.(g1.z,g2.z) & (o1.:(f1,f2)).z = o1.(f1.z,f2. z) & o1.(f1.z,f2.z) = o1.[f1.z,f2.z] & o2.(f1.z,f2.z) = o2.[f1.z,f2.z] & f1.z in rng f1 & f2.z in rng f2 by A5,BINOP_1:def 1,FUNCOP_1:28,FUNCT_1:def 5; then [f1.z,f2.z] in dom o1 by A2,A5,ZFMISC_1:106; hence (o2.:(g1,g2)).z = (o1.:(f1,f2)).z by A1,A6,GRFUNC_1:8; end; then ((o1,D).:A).(f1,f2) = ((o1,D).:A).[f1,f2] & [f1,f2] = x & ((o2,E).:A).(g1,g2) = ((o2,E).:A).[g1,g2] & o2.:(g1,g2) = o1.:(f1,f2) by A5,BINOP_1:def 1,FUNCT_1:9,MCART_1:23; hence ((o1,D).:A).x = ((o2,E).:A).x by A5; end; hence thesis by A4,GRFUNC_1:8; end; definition let G be non empty HGrStr; let A be set; func .:(G,A) -> HGrStr equals: Def3: multLoopStr (# Funcs(A, the carrier of G), (the mult of G,the carrier of G).:A, (A --> the_unity_wrt the mult of G)#) if G is unital otherwise HGrStr (# Funcs(A, the carrier of G), (the mult of G,the carrier of G).:A #); correctness; end; definition let G be non empty HGrStr; 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 mult of G,the carrier of G).:A, (A --> the_unity_wrt the mult of G)#) by Def3; hence the carrier of .:(G,A) is non empty; suppose G is not unital; then .:(G,A) = HGrStr (# Funcs(A, the carrier of G), (the mult of G,the carrier of G).:A #) by Def3; hence the carrier of .:(G,A) is non empty; end; end; reserve G for non empty HGrStr; deffunc carr(non empty HGrStr) = the carrier of $1; theorem Th18: the carrier of .:(G,X) = Funcs(X, the carrier of G) & the mult of .:(G,X) = (the mult of G, the carrier of G).:X proof (G is unital implies .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G),carr(G)).:X, (X --> the_unity_wrt op(G))#)) & (not G is unital implies .:(G,X) = HGrStr(#Funcs(X, carr(G)), (op(G),carr(G)).:X#)) & (G is unital or not G is unital) by Def3; hence thesis; end; theorem x is Element of .: (G,X) iff x is Function of X, the carrier of G proof A1: carr(.:(G,X)) = Funcs(X, carr(G)) by Th18; x is Element of .:(G,X) implies x is Element of Funcs(X, carr(G)) by Th18; 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); dom f = X & rng f c= carr(G) by FUNCT_2:def 1,RELSET_1:12; 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 Th18; hence thesis; end; definition let G be non empty HGrStr, A be set; cluster .:(G,A) -> constituted-Functions; coherence by Lm1; end; theorem Th20: 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 Th18; f = f; hence thesis by FUNCT_2:def 1,RELSET_1:12; end; theorem Th21: for f,g being Element of .:(G,X) st for x 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 Th20; hence thesis by FUNCT_1:9; end; definition let G be non empty HGrStr, A be non empty set; let f be Element of .:(G,A); cluster rng f -> non empty; coherence proof consider a being Element of A; rng f c= carr(G) & dom f = A by Th20; then f.a in rng f by FUNCT_1:def 5; hence thesis; end; let a be Element of A; redefine func f.a -> Element of G; coherence proof A1: rng f c= carr(G) & dom f = A by Th20; then f.a in rng f by FUNCT_1:def 5 ; hence thesis by A1; end; end; theorem Th22: 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 Th18; op(.:(G,D)) = (op(G),carr(G)).:D & f1*f2 = op(.:(G,D)).(f1,f2) by Th18,VECTSP_1:def 10; then dom (op(G).:(g1,g2)) = D & f1*f2 = op(G).:(g1,g2) by Def2,FUNCT_2:def 1; hence (f1*f2).a = op(G).(f1.a,f2.a) by FUNCOP_1:28 .= (f1.a)*(f2.a) by VECTSP_1:def 10; end; definition let G be unital (non empty HGrStr); let A be set; redefine func .:(G,A) -> well-unital constituted-Functions strict (non empty multLoopStr); coherence proof op(G) has_a_unity by MONOID_0:def 10; then consider a being Element of G such that A1: a is_a_unity_wrt op(G) by SETWISEO:def 2; A2: a = the_unity_wrt op(G) & .:(G,A) = multLoopStr(#Funcs(A, carr(G)), (op(G),carr(G)).:A, (A --> the_unity_wrt op(G))#) by A1,Def3,BINOP_1:def 8; A --> a is_a_unity_wrt (op(G),carr(G)).:A by A1,Th10; hence thesis by A2,MONOID_0:def 21; end; end; theorem Th23: for G being unital (non empty HGrStr) holds the unity of .:(G,X) = X --> the_unity_wrt the mult of G proof let G be unital (non empty HGrStr); .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G), carr(G)).:X, (X --> the_unity_wrt op(G))#) by Def3; hence thesis; end; theorem Th24: for G being non empty HGrStr, 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 Th18; thus G is commutative implies .:(G,A) is commutative proof assume op(G) is commutative; hence op(.:(G,A)) is commutative by A1,Th8; end; thus G is associative implies .:(G,A) is associative proof assume op(G) is associative; hence op(.:(G,A)) is associative by A1,Th9; end; thus G is idempotent implies .:(G,A) is idempotent proof assume op(G) is idempotent; hence op(.:(G,A)) is idempotent by A1,Th12; end; thus G is invertible implies .:(G,A) is invertible proof assume op(G) is invertible; hence op(.:(G,A)) is invertible by A1,Th13; end; thus G is cancelable implies .:(G,A) is cancelable proof assume op(G) is cancelable; hence op(.:(G,A)) is cancelable by A1,Th14; end; assume op(G) is uniquely-decomposable; hence op(.:(G,A)) is uniquely-decomposable by A1,Th15; 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; op(H) <= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X & op(.:(H,X)) = (op(H), carr(H)).:X by Th18,MONOID_0:def 23; hence op(.:(H,X)) <= op(.:(G,X)) by Th17; end; theorem for G being unital (non empty HGrStr), H being non empty SubStr of G st the_unity_wrt the mult of G in the carrier of H holds .:(H,X) is MonoidalSubStr of .:(G,X) proof let G be unital (non empty HGrStr), H be non empty SubStr of G; assume A1: the_unity_wrt the mult of G in carr(H); then reconsider G' = G, H' = H as unital (non empty HGrStr) by MONOID_0:32; A2: op(H) <= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X & the unity of .:(G',X) = X --> the_unity_wrt op(G) & the unity of .:(H',X) = X --> the_unity_wrt op(H) & the_unity_wrt op(H') = the_unity_wrt op(G') & op(.:(H,X)) = (op(H), carr(H)).:X by A1,Th18,Th23,MONOID_0:32,def 23; then op(.:(H,X)) <= op(.:(G,X)) by Th17; hence thesis by A2,MONOID_0:def 25; end; definition let G be unital associative commutative cancelable uniquely-decomposable (non empty HGrStr); let A be set; redefine func .:(G,A) -> commutative cancelable uniquely-decomposable constituted-Functions strict Monoid; coherence proof .:(G,A) is commutative cancelable by Th24; hence thesis by Th24; 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: Def4: .:(<NAT,+,0>, A); correctness; end; theorem Th27: the carrier of MultiSet_over X = Funcs(X,NAT) & the mult of MultiSet_over X = (addnat,NAT).:X & the unity of MultiSet_over X = X --> 0 proof the HGrStr of <NAT,+,0> = <NAT,+> & MultiSet_over X = .:(<NAT,+,0>, X) & the_unity_wrt op(<NAT,+>) = 0 by Def4,MONOID_0:44,def 22; hence thesis by Th18,Th23,MONOID_0:52; end; definition let A be set; mode Multiset of A is Element of MultiSet_over A; end; theorem Th28: x is Multiset of X iff x is Function of X,NAT proof A1: x is Multiset of X iff x is Element of Funcs(X,NAT) by Th27; now let x be Function of X,NAT; dom x = X & rng x c= NAT by FUNCT_2:def 1,RELSET_1:12; hence x is Element of Funcs(X,NAT) by FUNCT_2:def 2; end; hence thesis by A1; end; theorem Th29: 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 Th28; hence thesis by FUNCT_2:def 1,RELSET_1:12; end; definition let A be non empty set; let m be Multiset of A; redefine func rng m -> non empty Subset of NAT; coherence proof consider a being Element of A; A1: MultiSet_over A = .:(<NAT,+,0>, A) & carr(<NAT,+,0>) = NAT by Def4,MONOID_0:52; then rng m c= NAT & dom m = A by Th20; then m.a in rng m by FUNCT_1:def 5; hence thesis by A1,Th20; end; let a be Element of A; func m.a -> Nat; coherence proof MultiSet_over A = .:(<NAT,+,0>, A) & carr(<NAT,+,0>) = NAT by Def4,MONOID_0:52; then A2: rng m c= NAT & dom m = A by Th20; then m.a in rng m by FUNCT_1:def 5 ; hence thesis by A2; end; end; theorem Th30: for m1,m2 being Multiset of D, a being Element of D holds (m1 [*] m2).a = (m1.a)+(m2.a) proof let m1,m2 be Multiset of D, a be Element of D; reconsider N = <NAT,+,0> as non empty HGrStr; reconsider f1 = m1, f2 = m2 as Element of .:(N,D) by Def4; thus (m1 [*] m2).a = (f1 [*] f2).a by Def4 .= (f1.a)*(f2.a) by Th22 .= (m1.a)+(m2.a) by MONOID_0:51; end; theorem Th31: chi(Y,X) is Multiset of X proof A1: dom chi(Y,X) = X & rng chi(Y,X) c= {0,1} & carr(MultiSet_over X) = Funcs(X,NAT) by Th27,FUNCT_3:48,def 3; then rng chi(Y,X) c= NAT by XBOOLE_1:1; hence thesis by A1,FUNCT_2:def 2; end; definition let Y,X; redefine func chi(Y,X) -> Multiset of X; coherence by Th31; end; definition let X; let n be Nat; redefine func X --> n -> Multiset of X; coherence proof thus X --> n is Multiset of X by Th28; end; end; definition let A be non empty set, a be Element of A; func chi a -> Multiset of A equals: Def5: chi({a},A); coherence; end; theorem Th32: 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; chi a = chi({a},A) & a in {a} & (b <> a implies not b in {a}) by Def5,TARSKI:def 1; hence thesis by 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 Th33: (for a holds m1.a = m2.a) implies m1 = m2 proof assume for a holds m1.a = m2.a; then (for x st x in A holds m1.x = m2.x) & MultiSet_over A = .:(<NAT,+,0>, A) by Def4; hence thesis by Th21; 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 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; given f being Function of A,NAT such that A2: a = f & f"(NAT\{0}) is finite; given g being Function of A,NAT such that A3: b = g & g"(NAT\{0}) is finite; reconsider h = a [*] b as Function of A,NAT by Th28; take h; A4: (f"(NAT\{0})) \/ (g"(NAT\{0})) is finite by A2,A3,FINSET_1:14; A5: dom h = A & dom f = A & dom g = A & rng f c= NAT & rng g c= NAT by FUNCT_2:def 1,RELSET_1:12; h"(NAT\{0}) c= (f"(NAT\{0})) \/ (g"(NAT\{0})) proof let x; assume A6: x in h"(NAT\{0}); then A7: x in A & h.x in NAT\{0} by FUNCT_1:def 13; f.x in rng f & g.x in rng g by A5,A6,FUNCT_1:def 5; then reconsider n = f.x, m = g.x as Nat by A5; h.x = n+m & not h.x in {0} by A2,A3,A7,Th30,XBOOLE_0:def 4; then n <> 0 or m <> 0 by 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 4; then x in f"(NAT\{0}) or x in g"(NAT\{0}) by A5,A6,FUNCT_1:def 13; hence thesis by XBOOLE_0:def 2; end; hence thesis by A4,FINSET_1:13; end; reconsider e = A --> 0 as Function of A,NAT by Th28; A8: dom e = A & rng e c= {0} & {0} c= NAT by FUNCOP_1:19; A9: now consider x being Element of e"(NAT\{0}); assume e"(NAT\{0}) <> {}; then x in A & e.x in NAT\{0} by A8,FUNCT_1:def 13; then e.x = 0 & not e.x in {0} by FUNCOP_1:13,XBOOLE_0:def 4; hence contradiction by TARSKI:def 1; end; e = un(MultiSet_over A) by Th27; then A10: P[the unity of MultiSet_over A] by A9; consider M being strict non empty MonoidalSubStr of MultiSet_over A such that A11: for a being Multiset of A holds a in the carrier of M iff P[a] from MonoidalSubStrEx2(A1,A10); reconsider M as strict non empty MonoidalSubStr of MultiSet_over A; take M; let f be Multiset of A; reconsider g = f as Function of A,NAT by Th28; 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 A11; hence thesis; end; assume f"(NAT\{0}) is finite; then g"(NAT\{0}) is finite; hence thesis by A11; end; uniqueness proof let M1,M2 be strict non empty MonoidalSubStr of MultiSet_over A such that A12: for f being Multiset of A holds f in carr(M1) iff f"(NAT\{0}) is finite and A13: for f being Multiset of A holds f in carr(M2) iff f"(NAT\{0}) is finite; set M = MultiSet_over A; A14: carr(M1) c= carr(M) & carr(M2) c= carr(M) & carr(M) = Funcs(A,NAT) by Th27,MONOID_0:25; carr(M1) = carr(M2) proof thus carr(M1) c= carr(M2) proof let x; assume A15: x in carr(M1); then reconsider f = x as Multiset of A by A14; f"(NAT\{0}) is finite by A12,A15; hence thesis by A13; end; let x; assume A16: x in carr(M2); then reconsider f = x as Multiset of A by A14; f"(NAT\{0}) is finite by A13,A16; hence thesis by A12; end; hence thesis by MONOID_0:29; end; end; theorem Th34: chi a is Element of finite-MultiSet_over A proof (chi a)"(NAT\{0}) c= {a} proof let x; assume x in (chi a)"(NAT\{0}); then A1: x in dom chi a & (chi a).x in NAT\{0} & dom chi a = A by Th29,FUNCT_1:def 13; then reconsider y = x as Element of A; not (chi a).y in {0} by A1,XBOOLE_0:def 4; then (chi a).y <> 0 by TARSKI:def 1; then y = a by Th32; hence thesis by TARSKI:def 1; end; then (chi a)"(NAT\{0}) is finite by FINSET_1:13; hence thesis by Def6; end; theorem Th35: 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 set; assume a in dom ({x}|(p^<*x*>)); then A1: a in dom (p^<*x*>) & (p^<*x*>).a in {x} by FUNCT_1:86; then a in Seg (len p+len <*x*>) & len <*x*> = 1 by FINSEQ_1:57,def 7 ; then a in Seg len p \/ {len p+1} & Seg len p = dom p by FINSEQ_1:11,def 3; then A2: a in dom p or a in {len p+1} by XBOOLE_0:def 2; reconsider a as Nat by A1; 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 A1,FUNCT_1:86; hence thesis by A2,XBOOLE_0:def 2; end; let a be set; assume a in dom ({x}|p) \/ {len p+1}; then a in dom ({x}|p) or a in {len p+1} by XBOOLE_0:def 2; then A3: a in dom p & p.a in {x} or a in {len p+1} & a = len p+1 & x in {x} by FUNCT_1:86,TARSKI:def 1; len <*x*> = 1 by FINSEQ_1:57; then A4: Seg len p = dom p & dom (p^<*x*>) = Seg (len p+1) & Seg (len p+1) = Seg len p \/ {len p+1} & (p^<*x*>).(len p+1) = x by FINSEQ_1:11,59,def 3,def 7; then A5: a in dom (p^<*x*>) by A3,XBOOLE_0:def 2; reconsider a as Nat by A3; a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7; hence thesis by A3,A4,A5,FUNCT_1:86; end; theorem Th36: 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 set; assume a in dom ({x}|(p^<*y*>)); then A2: a in dom (p^<*y*>) & (p^<*y*>).a in {x} by FUNCT_1:86; then a in Seg (len p+len <*y*>) & len <*y*> = 1 by FINSEQ_1:57,def 7 ; then a in Seg len p \/ {len p+1} & Seg len p = dom p by FINSEQ_1:11,def 3; then A3: a in dom p or a in {len p+1} by XBOOLE_0:def 2; reconsider a as Nat by A2; A4: (p^<*y*>).(len p+1) = y & not y in {x} by A1,FINSEQ_1:59,TARSKI:def 1; then (p^<*y*>).a = p.a by A2,A3,FINSEQ_1:def 7,TARSKI:def 1; hence thesis by A2,A3,A4,FUNCT_1:86,TARSKI:def 1; end; let a be set; assume a in dom ({x}|p); then A5: a in dom p & p.a in {x} by FUNCT_1:86; len <*y*> = 1 by FINSEQ_1:57; then Seg len p = dom p & dom (p^<*y*>) = Seg (len p+1) & Seg (len p+1) = Seg len p \/ {len p+1} & (p^<*y*>).(len p+1) = y by FINSEQ_1:11,59,def 3,def 7; then A6: a in dom (p^<*y*>) by A5,XBOOLE_0:def 2; reconsider a as Nat by A5; (p^<*y*>).a = p.a by A5,FINSEQ_1:def 7; hence thesis by A5,A6,FUNCT_1:86; end; definition let A be set, F be finite Relation; cluster A|F -> finite; coherence proof A|F c= F by RELAT_1:117; hence thesis by FINSET_1:13; end; 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 LambdaD; m is Multiset of A by Th28; 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 Th33; end; end; theorem |.<*> A.|.a = 0 proof <*> A = {} & dom {} = {} & dom ({a}|{}) c= dom {} by FUNCT_1:89; then dom ({a}|<*> A) = {} by XBOOLE_1:3; hence thesis by Def7,CARD_1:78; end; theorem Th38: |.<*> A.| = A --> 0 proof A1: dom |.<*>A.| = A by Th29; now let x; assume x in A; then reconsider a = x as Element of A; thus |.<*>A.|.x = card dom ({a}|{}) by Def7 .= 0 by CARD_1:78,RELAT_1:60,138; end; hence thesis by A1,FUNCOP_1:17; end; theorem |.<*a*>.| = chi a proof A1: rng <*a*> = {a} by FINSEQ_1:56; now let b be Element of A; set x = b; A2: <*a*> = (rng<*a*>)|<*a*> by RELAT_1:125; a <> x implies {x} misses {a} by ZFMISC_1:17; then {x}|<*a*> = ({x}/\rng<*a*>)|<*a*> & (a <> x implies {x}/\{a} = {}) by A2,RELAT_1:127,XBOOLE_0:def 7; then dom <*a*> = Seg 1 & card Seg 1 = 1 & (chi a).a = 1 & {a}|<*a*> = <*a*> & (x <> a implies {x}|<*a*> = {} & (chi a).b = 0) by A1,Th32,FINSEQ_1:55,78,RELAT_1:125,137; hence |.<*a*>.|.x = (chi a).x by Def7,CARD_1:78,RELAT_1:60; end; hence thesis by Th33; end; reserve p,q for FinSequence of A; theorem Th40: |.p^<*a*>.| = |.p.| [*] chi a proof now let b be Element of A; reconsider pa = p^<*a*> as FinSequence of A; len p < len p+1 by NAT_1:38; then not len p+1 in dom p & dom p is finite & dom ({b}|p) c= dom p by FINSEQ_3:27,FUNCT_1:89; then not len p+1 in dom ({b}|p) & dom ({b}|p) is finite; then |.p^<*a*>.|.b = card dom ({b}|pa) & |.p.|.b = card dom ({b}|p) & dom ({a}|(p^<*a*>)) = dom ({a}|p) \/ {len p+1} & (chi a).a = 1 & (a <> b implies dom ({b}|(p^<*a*>)) = dom ({b}|p) & (chi a).b = 0) & card (dom ({b}|p) \/ {len p+1}) = (card dom ({b}|p))+1 & (b = a or b <> a) & (|.p.| [*] chi a).b = (|.p.|.b) + ((chi a).b) by Def7,Th30,Th32,Th35,Th36,CARD_2:54; hence |.p^<*a*>.|.b = (|.p.| [*] chi a).b; end; hence thesis by Th33; end; theorem Th41: |.p^q.| = |.p.|[*]|.q.| proof defpred P[Nat] means for q st len q = $1 holds |.p^q.| = |.p.|[*]|.q.|; A1: P[0] proof let q; assume len q = 0; then q = {} by FINSEQ_1:25; then p^q = p & q = <*> A & |.<*>A.| = A-->0 & A-->0 = un(MultiSet_over A) by Th27,Th38,FINSEQ_1:47; hence thesis by MONOID_0:18; end; A2: for n st P[n] holds P[n+1] proof let n such that A3: for q st len q = n holds |.p^q.| = |.p.|[*]|.q.|; let q; assume A4: len q = n+1; then q <> {} by FINSEQ_1:25; then consider r being FinSequence, x being set such that A5: q = r^<*x*> by FINSEQ_1:63; reconsider r as FinSequence of A by A5,FINSEQ_1:50; len <*x*> = 1 by FINSEQ_1:57; then n+1 = len r+1 by A4,A5,FINSEQ_1:35; then A6: len r = n by XCMPLX_1:2; rng <*x*> = {x} by FINSEQ_1:56; then {x} c= rng q & rng q c= A by A5,FINSEQ_1:43,def 4; then {x} c= A by XBOOLE_1:1; then reconsider x as Element of A by ZFMISC_1:37; thus |.p^q.| = |.p^r^<*x*>.| by A5,FINSEQ_1:45 .= |.p^r.|[*] chi x by Th40 .= |.p.|[*]|.r.|[*] chi x by A3,A6 .= |.p.|[*](|.r.|[*] chi x) by VECTSP_1:def 16 .= |.p.|[*]|.q.| by A5,Th40; end; A7: for n holds P[n] from Ind(A1,A2); len q = len q; hence thesis by A7; end; theorem Th42: |.n .--> a.|.a = n & for b being Element of A st b <> a holds |.n .--> a.|.b = 0 proof defpred P[Nat] means |.$1 .--> a.|.a = $1; A1: (A-->0).a = 0 & 0.-->a = {} & {} = <*>A by FINSEQ_2:72,FUNCOP_1:13; then A2: P[0] by Th38; A3: for n st P[n] holds P[n+1] proof let n such that A4: |.n .--> a.|.a = n; thus |.(n+1) .--> a.|.a = |.(n .--> a)^<*a*>.|.a by FINSEQ_2:74 .= (|.n .--> a.|[*]chi a).a by Th40 .= n+(chi a).a by A4,Th30 .= n+1 by Th32; end; for n holds P[n] from Ind(A2,A3); hence |.n .--> a.|.a = n; let b be Element of A such that A5: b <> a; defpred P[Nat] means |.$1 .--> a.|.b = 0; (A-->0).b = 0 by FUNCOP_1:13; then A6: P[0] by A1,Th38; A7: for n st P[n] holds P[(n+1)] proof let n such that A8: |.n .--> a.|.b = 0; thus |.(n+1) .--> a.|.b = |.(n .--> a)^<*a*>.|.b by FINSEQ_2:74 .= (|.n .--> a.|[*]chi a).b by Th40 .= 0+(chi a).b by A8,Th30 .= 0 by A5,Th32; end; for n holds P[n] from Ind(A6,A7); 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: Q[0] proof let p; assume len p = 0; then p = <*> A by FINSEQ_1:32; then |.p.| = A --> 0 by Th38 .= un(MultiSet_over A) by Th27 .= un(finite-MultiSet_over A) by MONOID_0:def 24; hence thesis; end; A2: for n st Q[n] holds Q[n+1] proof let n such that A3: for p st len p = n holds P[p]; let p; assume A4: len p = n+1; then p <> {} by FINSEQ_1:25; then consider r being FinSequence, x being set such that A5: p = r^<*x*> by FINSEQ_1:63; reconsider r as FinSequence of A by A5,FINSEQ_1:50; len <*x*> = 1 by FINSEQ_1:57; then n+1 = len r+1 by A4,A5,FINSEQ_1:35; then A6: len r = n by XCMPLX_1:2; rng <*x*> = {x} by FINSEQ_1:56; then {x} c= rng p & rng p c= A by A5,FINSEQ_1:43,def 4; then {x} c= A by XBOOLE_1:1; then reconsider x as Element of A by ZFMISC_1:37; set M = finite-MultiSet_over A; reconsider r' = |.r.|, a = chi x as Element of M by A3,A6,Th34; M is SubStr of MultiSet_over A by MONOID_0:23; then r'[*]a = |.r.|[*]chi x by MONOID_0:27 .= |.p.| by A5,Th40; hence thesis; end; A7: for n holds Q[n] from Ind(A1,A2); len p = len p; hence thesis by A7; 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.|; A1: Z[0] proof let fm such that A2: for V being finite set st V = fm"(NAT\{0}) holds card V = 0; take p = <*> A; carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:25; then reconsider m = fm as Multiset of A by TARSKI:def 3; reconsider V = m"(NAT\{0}) as finite set by Def6; card V = 0 by A2; then fm"(NAT\{0}) = {} by CARD_2:59; then rng fm misses (NAT\{0}) by RELAT_1:173; then A3: {} = rng fm /\ (NAT\{0}) by XBOOLE_0:def 7 .= (rng fm /\ NAT)\{0} by XBOOLE_1:49; rng m c= NAT; then rng fm /\ NAT = rng fm by XBOOLE_1:28; then A4: rng fm c= {0} & dom m = A by A3,Th29,XBOOLE_1:37; consider a; A5: fm.a in rng fm by A4,FUNCT_1:def 5 ; then fm.a = 0 by A4,TARSKI:def 1; then {0} c= rng fm by A5,ZFMISC_1:37; then rng fm = {0} by A4,XBOOLE_0:def 10; hence fm = A --> 0 by A4,FUNCOP_1:15 .= |.p.| by Th38; end; A6: for n st Z[n] holds Z[n+1] proof let n such that A7: 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 A8: for V being finite set st V = fm"(NAT\{0}) holds card V = n+1; carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:25; then reconsider m = fm as Multiset of A by TARSKI:def 3; consider x being Element of fm"(NAT\{0}); reconsider V = m"(NAT\{0}) as finite set by Def6; A9: card V = n+1 by A8; then A10: x in dom fm & fm.x in NAT\{0} & dom m = A by Th29,CARD_1:47,FUNCT_1 :def 13; then reconsider x as Element of A; defpred C[set] means x = $1; deffunc F(set) = 0; deffunc G(set) = fm.$1; consider f being Function such that A11: dom f = A & for a being set st a in A holds (C[a] implies f.a = F(a)) & (not C[a] implies f.a = G(a)) from LambdaC; rng f c= NAT proof let y; assume y in rng f; then consider z being set such that A12: z in dom f & y = f.z by FUNCT_1:def 5; reconsider z as Element of A by A11,A12; z = x or z <> x; then y = 0 or y = m.z by A11,A12; hence thesis; end; then reconsider f as Function of A,NAT by A11,FUNCT_2:def 1,RELSET_1:11; reconsider f as Multiset of A by Th28; A13: f"(NAT\{0}) = (fm"(NAT\{0}))\{x} proof thus f"(NAT\{0}) c= (fm"(NAT\{0}))\{x} proof let y; assume A14: y in f"(NAT\{0}); then A15: y in dom f & f.y in NAT\{0} by FUNCT_1:def 13; reconsider a = y as Element of A by A11,A14,FUNCT_1:def 13; not f.a in {0} by A15,XBOOLE_0:def 4; then f.a <> 0 by TARSKI:def 1; then a <> x by A11; then A16: not a in {x} & f.a = fm.a by A11,TARSKI:def 1; then a in fm"(NAT\{0}) by A10,A15,FUNCT_1:def 13; hence thesis by A16,XBOOLE_0:def 4; end; let y; assume y in (fm"(NAT\{0}))\{x}; then y in fm"(NAT\{0}) & not y in {x} by XBOOLE_0:def 4; then A17: y in dom fm & fm.y in NAT\{0} & y <> x by FUNCT_1:def 13,TARSKI :def 1 ; then fm.y = f.y by A10,A11; hence thesis by A10,A11,A17,FUNCT_1:def 13; end; then f"(NAT\{0}) is finite by A9,FINSET_1:16; then reconsider f' = f as Element of finite-MultiSet_over A by Def6; reconsider V' = f'"(NAT\{0}) as finite set by Def6; {x} c= fm"(NAT\{0}) & card {x} = 1 by A9,CARD_1:47,79,ZFMISC_1:37; then card V' = n+1-1 by A9,A13,CARD_2:63 .= n+(1-1) by XCMPLX_1:29 .= n; then for V being finite set st V = f'"(NAT\{0}) holds card V = n; then consider p such that A18: f = |.p.| by A7; take q = p^((m.x) .--> x); set g = |.(m.x) .--> x.|; now let a; A19: f.x = 0 & g.x = m.x & 0 + m.a = m.a & m.a + 0 = m.a by A11,Th42; a <> x implies f.a = m.a & g.a = 0 by A11,Th42; hence (f[*]g).a = m.a by A19,Th30; end; hence fm = f[*]g by Th33 .= |.q.| by A18,Th41; end; A20: for n holds Z[n] from Ind(A1,A6); 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:25; then m is Multiset of A by TARSKI:def 3; then reconsider V = m"(NAT\{0}) as finite set by Def6; for V' being finite set st V' = m"(NAT\{0}) holds card V' = card V; hence thesis by A20; 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 LambdaD; 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:113; end; 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 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; A1: [X1,X2]`1 = X1 & [X1,X2]`2 = X2 by MCART_1:7; thus (f.:^2).(X1,X2) = (f.:^2).[X1,X2] by BINOP_1:def 1 .= f.:[:X1,X2:] by A1,Def8; end; theorem Th46: 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 A1: x1 in X1 & x2 in X2; then reconsider a = x1 as Element of D1; reconsider b = x2 as Element of D2 by A1; A2: (f.:^2).(X1,X2) = f.:[:X1,X2:] by Th45; f.(a,b) = f.[a,b] & [a,b] in [:X1,X2:] & dom f = [:D1,D2:] by A1,BINOP_1:def 1,FUNCT_2:def 1,ZFMISC_1:106; hence thesis by A2,FUNCT_1:def 12; 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:] & X1 c= D1 & X2 c= D2 by Th45; thus (f.:^2).(X1,X2) c= A proof let x; assume x in f.:^2.(X1,X2); then consider y such that A2: y in dom f & y in [:X1,X2:] & x = f.y by A1,FUNCT_1:def 12; consider y1,y2 being set such that A3: y1 in X1 & y2 in X2 & y = [y1,y2] by A2,ZFMISC_1:103; reconsider y1 as Element of D1 by A3; reconsider y2 as Element of D2 by A3; x = f.(y1,y2) by A2,A3,BINOP_1:def 1; hence thesis by A3; end; let x; 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 Th46; end; theorem Th48: 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; assume x in o.:[:X,Y:]; then consider y such that A2: y in dom o & y in [:X,Y:] & x = o.y by FUNCT_1:def 12; A3: dom o = [:D,D:] by FUNCT_2:def 1; reconsider y as Element of [:D,D:] by A2,FUNCT_2:def 1; y = [y`1,y`2] by MCART_1:23; then y`1 in X & y`2 in Y & x = o.(y`1,y`2) & o.(y`1,y`2) = o.(y`2,y`1 ) by A1,A2,BINOP_1:def 1,ZFMISC_1:106; then [y`2,y`1] in [:D,D:] & [y`2,y`1] in [:Y,X:] & x = o.[y`2,y`1] by BINOP_1:def 1,ZFMISC_1:106; hence thesis by A3,FUNCT_1:def 12; end; end; hence o.:[:X,Y:] c= o.:[:Y,X:] & o.:[:Y,X:] c= o.:[:X,Y:]; end; theorem Th49: o is associative implies o.:[:o.:[:X,Y:],Z:] = o.:[:X,o.:[:Y,Z:]:] proof assume A1: o.(o.(a,b),c) = o.(a,o.(b,c)); A2: dom o = [:D,D:] by FUNCT_2:def 1; thus o.:[:o.:[:X,Y:],Z:] c= o.:[:X,o.:[:Y,Z:]:] proof let x; assume x in o.:[:o.:[:X,Y:],Z:]; then consider y such that A3: y in dom o & y in [:o.:[:X,Y:],Z:] & x = o.y by FUNCT_1:def 12; reconsider y as Element of [:D,D:] by A3,FUNCT_2:def 1; y = [y`1,y`2] by MCART_1:23; then A4: y`1 in o.:[:X,Y:] & y`2 in Z & x = o.(y`1,y`2) by A3,BINOP_1:def 1,ZFMISC_1:106; then consider z such that A5: z in dom o & z in [:X,Y:] & y`1 = o.z by FUNCT_1:def 12; reconsider z as Element of [:D,D:] by A5,FUNCT_2:def 1; z = [z`1,z`2] by MCART_1:23; then A6: z`1 in X & z`2 in Y & y`1 = o.(z`1,z`2) by A5,BINOP_1:def 1,ZFMISC_1:106; then x = o.(z`1,o.(z`2,y`2)) & o.(z`2,y`2) = o.[z`2,y`2] & [z`2,y`2] in [:Y,Z:] by A1,A4,BINOP_1:def 1,ZFMISC_1:106; then A7: o.(z`2,y`2) in o.:[:Y,Z:] & x = o.[z`1,o.(z`2,y`2)] by A2,BINOP_1:def 1,FUNCT_1:def 12; then [z`1,o.(z`2,y`2)] in [:X,o.:[:Y,Z:]:] by A6,ZFMISC_1:106; hence thesis by A2,A7,FUNCT_1:def 12; end; let x; assume x in o.:[:X,o.:[:Y,Z:]:]; then consider y such that A8: y in dom o & y in [:X,o.:[:Y,Z:]:] & x = o.y by FUNCT_1:def 12; reconsider y as Element of [:D,D:] by A8,FUNCT_2:def 1; y = [y`1,y`2] by MCART_1:23; then A9: y`2 in o.:[:Y,Z:] & y`1 in X & x = o.(y`1,y`2) by A8,BINOP_1:def 1,ZFMISC_1:106; then consider z such that A10: z in dom o & z in [:Y,Z:] & y`2 = o.z by FUNCT_1:def 12; reconsider z as Element of [:D,D:] by A10,FUNCT_2:def 1; z = [z`1,z`2] by MCART_1:23; then A11: z`1 in Y & z`2 in Z & y`2 = o.(z`1,z`2) by A10,BINOP_1:def 1,ZFMISC_1:106; then x = o.(o.(y`1,z`1),z`2) & o.(y`1,z`1) = o.[y`1,z`1] & [y`1,z`1] in [:X,Y:] by A1,A9,BINOP_1:def 1,ZFMISC_1:106; then A12: o.(y`1,z`1) in o.:[:X,Y:] & x = o.[o.(y`1,z`1),z`2] by A2,BINOP_1:def 1,FUNCT_1:def 12; then [o.(y`1,z`1),z`2] in [:o.:[:X,Y:],Z:] by A11,ZFMISC_1:106; hence thesis by A2,A12,FUNCT_1:def 12; end; theorem Th50: 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 Th45 .= o.:[:y,x:] by A1,Th48 .= (o.:^2).(y,x) by Th45; end; theorem Th51: 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 Th45 .= o.:[:o.:[:x,y:],z:] by Th45 .= o.:[:x,o.:[:y,z:]:] by A1,Th49 .= (o.:^2).(x,o.:[:y,z:]) by Th45 .= (o.:^2).(x,(o.:^2).(y,z)) by Th45; end; theorem Th52: 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; A2: dom o = [:D,D:] by FUNCT_2:def 1; thus o.:[:{a},X:] c= D /\ X proof let x; assume x in o.:[:{a},X:]; then consider y such that A3: y in dom o & y in [:{a},X:] & x = o.y by FUNCT_1:def 12; reconsider y as Element of [:D,D:] by A3,FUNCT_2:def 1; A4: y = [y`1,y`2] by MCART_1:23; then y`1 in {a} & y`2 in X by A3,ZFMISC_1:106; then x = o.(y`1,y`2) & o.(a,y`2) = y`2 & y`1 = a & y`2 in D /\ X by A1,A3,A4,BINOP_1:11,def 1,TARSKI:def 1,XBOOLE_0:def 3; hence thesis; end; thus D /\ X c= o.:[:{a},X:] proof let x; assume A5: x in D /\ X; then A6: x in D & x in X by XBOOLE_0:def 3; reconsider d = x as Element of D by A5,XBOOLE_0:def 3; A7: x = o.(a,d) by A1,BINOP_1:11 .= o.[a,x] by BINOP_1:def 1; a in {a} by TARSKI:def 1; then [a,d] in [:{a},X:] by A6,ZFMISC_1:106; hence thesis by A2,A7,FUNCT_1:def 12; end; thus o.:[:X,{a}:] c= D /\ X proof let x; assume x in o.:[:X,{a}:]; then consider y such that A8: y in dom o & y in [:X,{a}:] & x = o.y by FUNCT_1:def 12; reconsider y as Element of [:D,D:] by A8,FUNCT_2:def 1; A9: y = [y`1,y`2] by MCART_1:23; then y`2 in {a} & y`1 in X by A8,ZFMISC_1:106; then x = o.(y`1,y`2) & o.(y`1,a) = y`1 & y`2 = a & y`1 in D /\ X by A1,A8,A9,BINOP_1:11,def 1,TARSKI:def 1,XBOOLE_0:def 3; hence thesis; end; thus D /\ X c= o.:[:X,{a}:] proof let x; assume A10: x in D /\ X; then A11: x in D & x in X by XBOOLE_0:def 3; reconsider d = x as Element of D by A10,XBOOLE_0:def 3; A12: x = o.(d,a) by A1,BINOP_1:11 .= o.[x,a] by BINOP_1:def 1; a in {a} by TARSKI:def 1; then [d,a] in [:X,{a}:] by A11,ZFMISC_1:106; hence thesis by A2,A12,FUNCT_1:def 12; end; end; theorem Th53: a is_a_unity_wrt o implies {a} is_a_unity_wrt o.:^2 & o.:^2 has_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 Th45 .= D /\ x by A1,Th52 .= x by XBOOLE_1:28; thus (o.:^2).(x,{a}) = o.:[:x,{a}:] by Th45 .= D /\ x by A1,Th52 .= x by XBOOLE_1:28; end; hence A2: {a} is_a_unity_wrt o.:^2 by BINOP_1:11; 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 Th54: o has_a_unity implies o.:^2 has_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} is_a_unity_wrt o.:^2 & o.:^2 has_a_unity & a = the_unity_wrt o & the_unity_wrt o.:^2 = {a} by A1,Th53,BINOP_1:def 8; hence thesis; end; theorem Th55: o is uniquely-decomposable implies o.:^2 is uniquely-decomposable proof assume that A1: o has_a_unity and A2: o.(a,b) = the_unity_wrt o implies a = b & b = the_unity_wrt o; thus o.:^2 has_a_unity by A1,Th54; set a = the_unity_wrt o; let A,B be Subset of D such that A3: (o.:^2).(A,B) = the_unity_wrt o.:^2; A4: the_unity_wrt o.:^2 = {a} & o.:[:A,B:] = (o.:^2).(A,B) & a in {a} by A1,Th45,Th54,TARSKI:def 1; then dom o meets [:A,B:] by A3,RELAT_1:151; then dom o /\ [:A,B:] <> {} by XBOOLE_0:def 7; then [:A,B:] <> {}; then A5: A <> {} & B <> {} & A c= D & B c= D by ZFMISC_1:113; consider a1 being Element of A, a2 being Element of B; reconsider a1,a2 as Element of D by A5,TARSKI:def 3; o.(a1,a2) in {a} by A3,A4,A5,Th46; then o.(a1,a2) = a by TARSKI:def 1; then A6: a1 = a2 & a2 = a & {a1} c= A & {a2} c= B by A2,A5,ZFMISC_1:37; A7: A c= {a} proof let x; assume A8: x in A; then reconsider c = x as Element of D; o.(c,a2) in {a} by A3,A4,A5,A8,Th46; then o.(c,a2) = a by TARSKI:def 1; then c = a2 by A2; hence thesis by A6,TARSKI:def 1; end; B c= {a} proof let x; assume A9: x in B; then reconsider c = x as Element of D; o.(a1,c) in {a} by A3,A4,A5,A9,Th46; then o.(a1,c) = a by TARSKI:def 1; then c = a by A2; hence thesis by TARSKI:def 1; end; then A = {a} & B = {a} by A6,A7,XBOOLE_0:def 10; hence thesis by A1,Th54; end; definition let G be non empty HGrStr; func bool G -> HGrStr equals: Def9: multLoopStr(#bool the carrier of G, (the mult of G).:^2, {the_unity_wrt the mult of G}#) if G is unital otherwise HGrStr(#bool the carrier of G, (the mult of G).:^2#); correctness; end; definition let G be non empty HGrStr; cluster bool G -> non empty; coherence proof per cases; suppose G is unital; then bool G = multLoopStr(#bool the carrier of G, (the mult of G).:^2, {the_unity_wrt the mult of G}#) by Def9; hence the carrier of bool G is non empty; suppose G is not unital; then bool G = HGrStr(#bool the carrier of G, (the mult of G).:^2#) by Def9 ; hence the carrier of bool G is non empty; end; end; definition let G be unital (non empty HGrStr); redefine func bool G -> well-unital strict (non empty multLoopStr); coherence proof op(G) has_a_unity by MONOID_0:def 10; then bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)} #) & {the_unity_wrt op(G)} is_a_unity_wrt op(G).:^2 by Def9,Th54; hence thesis by MONOID_0:def 21; end; end; theorem Th56: the carrier of bool G = bool the carrier of G & the mult of bool G = (the mult of G).:^2 proof G is unital or not G is unital; then bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#) or bool G = HGrStr(#bool the carrier of G, op(G).:^2#) by Def9; hence thesis; end; theorem for G being unital (non empty HGrStr) holds the unity of bool G = {the_unity_wrt the mult of G} proof let G be unital (non empty HGrStr); 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 HGrStr 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 HGrStr; A1: op(bool G) = op(G).:^2 & carr(bool G) = bool carr(G) by Th56; thus G is commutative implies bool G is commutative proof assume op(G) is commutative; hence op(bool G) is commutative by A1,Th50; end; thus G is associative implies bool G is associative proof assume op(G) is associative; hence op(bool G) is associative by A1,Th51; end; assume op(G) is uniquely-decomposable; hence op(bool G) is uniquely-decomposable by A1,Th55; end;