:: MONOID_1 semantic presentation begin deffunc H1( multMagma ) -> Element of bool [:[: the carrier of \$1, the carrier of \$1:], the carrier of \$1:] = the multF of \$1; deffunc H2( multLoopStr ) -> Element of the carrier of \$1 = 1. \$1; definition let f be Function; let x1, x2, y be set ; funcf .. (x1,x2,y) -> set equals :: MONOID_1:def 1 f .. ([x1,x2],y); correctness coherence f .. ([x1,x2],y) is set ; ; end; :: deftheorem defines .. MONOID_1:def_1_:_ for f being Function for x1, x2, y being set holds f .. (x1,x2,y) = f .. ([x1,x2],y); 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; :: original: .. redefine funcf .. (x1,x2,x) -> Element of D; coherence f .. (x1,x2,x) is Element of D 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 f .. (x1,x2,x) is Element of D ; ::_thesis: verum end; end; definition let A be set ; let D1, D2, D be non empty set ; let f be Function of [:D1,D2:],D; let g1 be Function of A,D1; let g2 be Function of A,D2; :: original: .: redefine funcf .: (g1,g2) -> Element of Funcs (A,D); coherence f .: (g1,g2) is Element of Funcs (A,D) 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 f .: (g1,g2) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum end; end; notation let A be non empty set ; let n be Element of NAT ; let x be Element of A; synonym n .--> x for A |-> n; end; definition let A be non empty set ; let n be Element of NAT ; let x be Element of A; :: original: .--> redefine funcn .--> x -> FinSequence of A; coherence x .--> is FinSequence of A by FINSEQ_2:63; end; definition let D be non empty set ; let A be set ; let d be Element of D; :: original: --> redefine funcA --> d -> Element of Funcs (A,D); coherence A --> d is Element of Funcs (A,D) proof ( dom (A --> d) = A & rng (A --> d) c= {d} ) by FUNCOP_1:13; hence A --> d is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum end; end; definition let A be set ; let D1, D2, D be non empty set ; let f be Function of [:D1,D2:],D; let d be Element of D1; let g be Function of A,D2; :: original: [;] redefine funcf [;] (d,g) -> Element of Funcs (A,D); coherence f [;] (d,g) is Element of Funcs (A,D) 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 f [;] (d,g) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum end; end; definition let A be set ; let D1, D2, D be non empty set ; let f be Function of [:D1,D2:],D; let g be Function of A,D1; let d be Element of D2; :: original: [:] redefine funcf [:] (g,d) -> Element of Funcs (A,D); coherence f [:] (g,d) is Element of Funcs (A,D) 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 f [:] (g,d) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum end; end; theorem :: MONOID_1:1 for f, g being Function for X being set holds (f | X) * g = f * (X |` g) proof let f, g be Function; ::_thesis: for X being set holds (f | X) * g = f * (X |` g) let X be set ; ::_thesis: (f | X) * g = f * (X |` g) 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)) :: according to XBOOLE_0:def_10 ::_thesis: dom (f * (X |` g)) c= dom ((f | X) * g) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f | X) * g) or x in dom (f * (X |` g)) ) assume A3: x in dom ((f | X) * g) ; ::_thesis: 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 x in dom (f * (X |` g)) by A6, A7, FUNCT_1:11; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f * (X |` g)) or x in dom ((f | X) * g) ) assume A8: x in dom (f * (X |` g)) ; ::_thesis: 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 x in dom ((f | X) * g) by A10, FUNCT_1:11; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_((f_|_X)_*_g)_holds_ ((f_|_X)_*_g)_._x_=_(f_*_(X_|`_g))_._x let x be set ; ::_thesis: ( x in dom ((f | X) * g) implies ((f | X) * g) . x = (f * (X |` g)) . x ) assume A12: x in dom ((f | X) * g) ; ::_thesis: ((f | X) * g) . x = (f * (X |` g)) . x then ( ((f | X) * g) . x = (f | X) . (g . x) & g . x in dom (f | X) ) by FUNCT_1:11, FUNCT_1: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, FUNCT_1:12; hence ((f | X) * g) . x = (f * (X |` g)) . x by A13, FUNCT_1:53; ::_thesis: verum end; hence (f | X) * g = f * (X |` g) by A2, FUNCT_1:2; ::_thesis: verum end; scheme :: MONOID_1:sch 1 NonUniqFuncDEx{ F1() -> set , F2() -> non empty set , P1[ set , set ] } : ex f being Function of F1(),F2() st for x being set st x in F1() holds P1[x,f . x] provided A1: for x being set st x in F1() holds ex y being Element of F2() st P1[x,y] proof A2: for x being set st x in F1() holds ex y being set st ( y in F2() & P1[x,y] ) proof let x be set ; ::_thesis: ( x in F1() implies ex y being set st ( y in F2() & P1[x,y] ) ) assume x in F1() ; ::_thesis: ex y being set st ( y in F2() & P1[x,y] ) then consider y being Element of F2() such that A3: P1[x,y] by A1; take y ; ::_thesis: ( y in F2() & P1[x,y] ) thus ( y in F2() & P1[x,y] ) by A3; ::_thesis: verum end; consider f being Function such that A4: ( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds P1[x,f . x] ) ) from FUNCT_1:sch_5(A2); reconsider f = f as Function of F1(),F2() by A4, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for x being set st x in F1() holds P1[x,f . x] thus for x being set st x in F1() holds P1[x,f . x] by A4; ::_thesis: verum end; begin 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: :: MONOID_1:def 2 for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds it . (f1,f2) = f .: (f1,f2); existence ex b1 being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) st for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds b1 . (f1,f2) = f .: (f1,f2) proof deffunc H3( Element of Funcs (A,D1), Element of Funcs (A,D2)) -> Element of Funcs (A,D) = 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) = H3(f1,f2) from BINOP_1:sch_4(); take b ; ::_thesis: for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds b . (f1,f2) = f .: (f1,f2) let f1 be Element of Funcs (A,D1); ::_thesis: for f2 being Element of Funcs (A,D2) holds b . (f1,f2) = f .: (f1,f2) let f2 be Element of Funcs (A,D2); ::_thesis: b . (f1,f2) = f .: (f1,f2) thus b . (f1,f2) = f .: (f1,f2) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) st ( for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds b1 . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds b2 . (f1,f2) = f .: (f1,f2) ) holds b1 = b2 proof let o1, o2 be Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)); ::_thesis: ( ( for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds o2 . (f1,f2) = f .: (f1,f2) ) implies o1 = o2 ) assume 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) ; ::_thesis: o1 = o2 now__::_thesis:_for_f1_being_Element_of_Funcs_(A,D1) for_f2_being_Element_of_Funcs_(A,D2)_holds_o1_._(f1,f2)_=_o2_._(f1,f2) let f1 be Element of Funcs (A,D1); ::_thesis: for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = o2 . (f1,f2) let f2 be Element of Funcs (A,D2); ::_thesis: o1 . (f1,f2) = o2 . (f1,f2) thus o1 . (f1,f2) = f .: (f1,f2) by A2 .= o2 . (f1,f2) by A3 ; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines .: MONOID_1:def_2_:_ for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for A being set for b6 being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) holds ( b6 = (f,D) .: A iff for f1 being Element of Funcs (A,D1) for f2 being Element of Funcs (A,D2) holds b6 . (f1,f2) = f .: (f1,f2) ); theorem :: MONOID_1:2 for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for A being set for f1 being Function of A,D1 for f2 being Function of A,D2 for x being set 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 ; ::_thesis: for f being Function of [:D1,D2:],D for A being set for f1 being Function of A,D1 for f2 being Function of A,D2 for x being set st x in A holds ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) let f be Function of [:D1,D2:],D; ::_thesis: for A being set for f1 being Function of A,D1 for f2 being Function of A,D2 for x being set st x in A holds ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) let A be set ; ::_thesis: for f1 being Function of A,D1 for f2 being Function of A,D2 for x being set st x in A holds ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) let f1 be Function of A,D1; ::_thesis: for f2 being Function of A,D2 for x being set st x in A holds ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) let f2 be Function of A,D2; ::_thesis: for x being set st x in A holds ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) ( dom f2 = A & rng f2 c= D2 ) by FUNCT_2:def_1; then reconsider f2 = 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 = 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 be set ; ::_thesis: ( x in A implies ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) ) assume A3: x in A ; ::_thesis: ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) ( 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 ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) by A3, A1, A2, FUNCT_5:38; ::_thesis: verum end; theorem Th3: :: MONOID_1:3 for A being set for D being non empty set for o being BinOp of D for f, g being Function of A,D st o is commutative holds o .: (f,g) = o .: (g,f) proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D for f, g being Function of A,D st o is commutative holds o .: (f,g) = o .: (g,f) let D be non empty set ; ::_thesis: for o being BinOp of D for f, g being Function of A,D st o is commutative holds o .: (f,g) = o .: (g,f) let o be BinOp of D; ::_thesis: for f, g being Function of A,D st o is commutative holds o .: (f,g) = o .: (g,f) let f, g be Function of A,D; ::_thesis: ( o is commutative implies o .: (f,g) = o .: (g,f) ) 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: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: o .: (f,g) = o .: (g,f) now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_.:_(f,g))_._x_=_(o_.:_(g,f))_._x let x be set ; ::_thesis: ( x in A implies (o .: (f,g)) . x = (o .: (g,f)) . x ) assume A5: x in A ; ::_thesis: (o .: (f,g)) . x = (o .: (g,f)) . x 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 ; ::_thesis: verum end; hence o .: (f,g) = o .: (g,f) by A1, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th4: :: MONOID_1:4 for A being set for D being non empty set for o being BinOp of D for f, g, h being Function of A,D st o is associative holds o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D for f, g, h being Function of A,D st o is associative holds o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) let D be non empty set ; ::_thesis: for o being BinOp of D for f, g, h being Function of A,D st o is associative holds o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) let o be BinOp of D; ::_thesis: for f, g, h being Function of A,D st o is associative holds o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) let f, g, h be Function of A,D; ::_thesis: ( o is associative implies o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) ) 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: for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_.:_((o_.:_(f,g)),h))_._x_=_(o_.:_(f,(o_.:_(g,h))))_._x let x be set ; ::_thesis: ( x in A implies (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x ) assume A8: x in A ; ::_thesis: (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x 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 ; ::_thesis: verum end; hence o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) by A4, A6, FUNCT_1:2; ::_thesis: verum end; theorem Th5: :: MONOID_1:5 for A being set for D being non empty set for a being Element of D for o being BinOp of D for f being Function of A,D st a is_a_unity_wrt o holds ( o [;] (a,f) = f & o [:] (f,a) = f ) proof let A be set ; ::_thesis: for D being non empty set for a being Element of D for o being BinOp of D for f being Function of A,D st a is_a_unity_wrt o holds ( o [;] (a,f) = f & o [:] (f,a) = f ) let D be non empty set ; ::_thesis: for a being Element of D for o being BinOp of D for f being Function of A,D st a is_a_unity_wrt o holds ( o [;] (a,f) = f & o [:] (f,a) = f ) let a be Element of D; ::_thesis: for o being BinOp of D for f being Function of A,D st a is_a_unity_wrt o holds ( o [;] (a,f) = f & o [:] (f,a) = f ) let o be BinOp of D; ::_thesis: for f being Function of A,D st a is_a_unity_wrt o holds ( o [;] (a,f) = f & o [:] (f,a) = f ) let f be Function of A,D; ::_thesis: ( a is_a_unity_wrt o implies ( o [;] (a,f) = f & o [:] (f,a) = f ) ) assume A1: a is_a_unity_wrt o ; ::_thesis: ( o [;] (a,f) = f & o [:] (f,a) = f ) A2: dom f = A by FUNCT_2:def_1; A3: dom (o [;] (a,f)) = A by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_[;]_(a,f))_._x_=_f_._x let x be set ; ::_thesis: ( x in A implies (o [;] (a,f)) . x = f . x ) assume A4: x in A ; ::_thesis: (o [;] (a,f)) . x = f . x 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 ; ::_thesis: verum end; hence o [;] (a,f) = f by A3, A2, FUNCT_1:2; ::_thesis: o [:] (f,a) = f A5: dom (o [:] (f,a)) = A by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_[:]_(f,a))_._x_=_f_._x let x be set ; ::_thesis: ( x in A implies (o [:] (f,a)) . x = f . x ) assume A6: x in A ; ::_thesis: (o [:] (f,a)) . x = f . x 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 ; ::_thesis: verum end; hence o [:] (f,a) = f by A5, A2, FUNCT_1:2; ::_thesis: verum end; theorem Th6: :: MONOID_1:6 for A being set for D being non empty set for o being BinOp of D for f being Function of A,D st o is idempotent holds o .: (f,f) = f proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D for f being Function of A,D st o is idempotent holds o .: (f,f) = f let D be non empty set ; ::_thesis: for o being BinOp of D for f being Function of A,D st o is idempotent holds o .: (f,f) = f let o be BinOp of D; ::_thesis: for f being Function of A,D st o is idempotent holds o .: (f,f) = f let f be Function of A,D; ::_thesis: ( o is idempotent implies o .: (f,f) = f ) A1: dom (o .: (f,f)) = A by FUNCT_2:def_1; assume A2: for a being Element of D holds o . (a,a) = a ; :: according to BINOP_1:def_4 ::_thesis: o .: (f,f) = f A3: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_.:_(f,f))_._x_=_f_._x let x be set ; ::_thesis: ( x in A implies (o .: (f,f)) . x = f . x ) assume A4: x in A ; ::_thesis: (o .: (f,f)) . x = f . x 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 ; ::_thesis: verum end; dom f = A by FUNCT_2:def_1; hence o .: (f,f) = f by A1, A3, FUNCT_1:2; ::_thesis: verum end; theorem Th7: :: MONOID_1:7 for A being set for D being non empty set for o being BinOp of D st o is commutative holds (o,D) .: A is commutative proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is commutative holds (o,D) .: A is commutative let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds (o,D) .: A is commutative let o be BinOp of D; ::_thesis: ( o is commutative implies (o,D) .: A is commutative ) assume A1: o is commutative ; ::_thesis: (o,D) .: A is commutative set h = (o,D) .: A; let f, g be Element of Funcs (A,D); :: according to BINOP_1:def_2 ::_thesis: ((o,D) .: A) . (f,g) = ((o,D) .: A) . (g,f) thus ((o,D) .: A) . (f,g) = o .: (f,g) by Def2 .= o .: (g,f) by A1, Th3 .= ((o,D) .: A) . (g,f) by Def2 ; ::_thesis: verum end; theorem Th8: :: MONOID_1:8 for A being set for D being non empty set for o being BinOp of D st o is associative holds (o,D) .: A is associative proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is associative holds (o,D) .: A is associative let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds (o,D) .: A is associative let o be BinOp of D; ::_thesis: ( o is associative implies (o,D) .: A is associative ) assume A1: o is associative ; ::_thesis: (o,D) .: A is associative set F = (o,D) .: A; let f, g, h be Element of Funcs (A,D); :: according to BINOP_1:def_3 ::_thesis: ((o,D) .: A) . (f,(((o,D) .: A) . (g,h))) = ((o,D) .: A) . ((((o,D) .: A) . (f,g)),h) thus ((o,D) .: A) . ((((o,D) .: A) . (f,g)),h) = ((o,D) .: A) . ((o .: (f,g)),h) by Def2 .= o .: ((o .: (f,g)),h) by Def2 .= o .: (f,(o .: (g,h))) by A1, Th4 .= ((o,D) .: A) . (f,(o .: (g,h))) by Def2 .= ((o,D) .: A) . (f,(((o,D) .: A) . (g,h))) by Def2 ; ::_thesis: verum end; theorem Th9: :: MONOID_1:9 for A being set for D being non empty set for a being Element of D for o being BinOp of D st a is_a_unity_wrt o holds A --> a is_a_unity_wrt (o,D) .: A proof let A be set ; ::_thesis: for D being non empty set for a being Element of D for o being BinOp of D st a is_a_unity_wrt o holds A --> a is_a_unity_wrt (o,D) .: A let D be non empty set ; ::_thesis: for a being Element of D for o being BinOp of D st a is_a_unity_wrt o holds A --> a is_a_unity_wrt (o,D) .: A let a be Element of D; ::_thesis: for o being BinOp of D st a is_a_unity_wrt o holds A --> a is_a_unity_wrt (o,D) .: A let o be BinOp of D; ::_thesis: ( a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D) .: A ) set e = A --> a; set F = (o,D) .: A; assume A1: a is_a_unity_wrt o ; ::_thesis: A --> a is_a_unity_wrt (o,D) .: A now__::_thesis:_for_f_being_Element_of_Funcs_(A,D)_holds_ (_((o,D)_.:_A)_._((A_-->_a),f)_=_f_&_((o,D)_.:_A)_._(f,(A_-->_a))_=_f_) let f be Element of Funcs (A,D); ::_thesis: ( ((o,D) .: A) . ((A --> a),f) = f & ((o,D) .: A) . (f,(A --> a)) = f ) A2: dom f = A by FUNCT_2:def_1; thus ((o,D) .: A) . ((A --> a),f) = o .: ((A --> a),f) by Def2 .= o [;] (a,f) by A2, FUNCOP_1:31 .= f by A1, Th5 ; ::_thesis: ((o,D) .: A) . (f,(A --> a)) = f thus ((o,D) .: A) . (f,(A --> a)) = o .: (f,(A --> a)) by Def2 .= o [:] (f,a) by A2, FUNCOP_1:26 .= f by A1, Th5 ; ::_thesis: verum end; hence A --> a is_a_unity_wrt (o,D) .: A by BINOP_1:3; ::_thesis: verum end; theorem Th10: :: MONOID_1:10 for A being set for D being non empty set for o being BinOp of D st o is having_a_unity holds ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is having_a_unity holds ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) let D be non empty set ; ::_thesis: for o being BinOp of D st o is having_a_unity holds ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) let o be BinOp of D; ::_thesis: ( o is having_a_unity implies ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) ) given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def_2 ::_thesis: ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) ( 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; ::_thesis: (o,D) .: A is having_a_unity take A --> a ; :: according to SETWISEO:def_2 ::_thesis: A --> a is_a_unity_wrt (o,D) .: A thus A --> a is_a_unity_wrt (o,D) .: A by A1, Th9; ::_thesis: verum end; theorem Th11: :: MONOID_1:11 for A being set for D being non empty set for o being BinOp of D st o is idempotent holds (o,D) .: A is idempotent proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is idempotent holds (o,D) .: A is idempotent let D be non empty set ; ::_thesis: for o being BinOp of D st o is idempotent holds (o,D) .: A is idempotent let o be BinOp of D; ::_thesis: ( o is idempotent implies (o,D) .: A is idempotent ) assume A1: o is idempotent ; ::_thesis: (o,D) .: A is idempotent let f be Element of Funcs (A,D); :: according to BINOP_1:def_4 ::_thesis: ((o,D) .: A) . (f,f) = f thus ((o,D) .: A) . (f,f) = o .: (f,f) by Def2 .= f by A1, Th6 ; ::_thesis: verum end; theorem Th12: :: MONOID_1:12 for A being set for D being non empty set for o being BinOp of D st o is invertible holds (o,D) .: A is invertible proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is invertible holds (o,D) .: A is invertible let D be non empty set ; ::_thesis: for o being BinOp of D st o is invertible holds (o,D) .: A is invertible let o be BinOp of D; ::_thesis: ( o is invertible implies (o,D) .: A is invertible ) assume A1: for a, b being Element of D ex r, l being Element of D st ( o . (a,r) = b & o . (l,a) = b ) ; :: according to MONOID_0:def_5 ::_thesis: (o,D) .: A is invertible let f, g be Element of Funcs (A,D); :: according to MONOID_0:def_5 ::_thesis: ex b1, b2 being Element of Funcs (A,D) st ( ((o,D) .: A) . (f,b1) = g & ((o,D) .: A) . (b2,f) = g ) defpred S1[ set , set ] means o . ((f . \$1),\$2) = g . \$1; A2: for x being set st x in A holds ex c being Element of D st S1[x,c] proof let x be set ; ::_thesis: ( x in A implies ex c being Element of D st S1[x,c] ) assume x in A ; ::_thesis: ex c being Element of D st S1[x,c] then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5; consider r, l being Element of D such that A3: o . (a,r) = b and o . (l,a) = b by A1; take r ; ::_thesis: S1[x,r] thus S1[x,r] by A3; ::_thesis: verum end; consider h1 being Function of A,D such that A4: for x being set st x in A holds S1[x,h1 . x] from MONOID_1:sch_1(A2); defpred S2[ set , set ] means o . (\$2,(f . \$1)) = g . \$1; A5: for x being set st x in A holds ex c being Element of D st S2[x,c] proof let x be set ; ::_thesis: ( x in A implies ex c being Element of D st S2[x,c] ) assume x in A ; ::_thesis: ex c being Element of D st S2[x,c] then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5; consider r, l being Element of D such that o . (a,r) = b and A6: o . (l,a) = b by A1; take l ; ::_thesis: S2[x,l] thus S2[x,l] by A6; ::_thesis: verum end; consider h2 being Function of A,D such that A7: for x being set st x in A holds S2[x,h2 . x] from MONOID_1:sch_1(A5); A8: ( dom h1 = A & dom h2 = A ) by FUNCT_2:def_1; ( rng h1 c= D & rng h2 c= D ) ; then reconsider h1 = h1, h2 = h2 as Element of Funcs (A,D) by A8, FUNCT_2:def_2; take h1 ; ::_thesis: ex b1 being Element of Funcs (A,D) st ( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b1,f) = g ) take h2 ; ::_thesis: ( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (h2,f) = g ) A9: dom g = A by FUNCT_2:def_1; A10: dom (o .: (f,h1)) = A by FUNCT_2:def_1; A11: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_.:_(f,h1))_._x_=_g_._x let x be set ; ::_thesis: ( x in A implies (o .: (f,h1)) . x = g . x ) assume A12: x in A ; ::_thesis: (o .: (f,h1)) . x = g . x hence (o .: (f,h1)) . x = o . ((f . x),(h1 . x)) by A10, FUNCOP_1:22 .= g . x by A4, A12 ; ::_thesis: verum 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; ::_thesis: ((o,D) .: A) . (h2,f) = g A13: dom (o .: (h2,f)) = A by FUNCT_2:def_1; A14: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ (o_.:_(h2,f))_._x_=_g_._x let x be set ; ::_thesis: ( x in A implies (o .: (h2,f)) . x = g . x ) assume A15: x in A ; ::_thesis: (o .: (h2,f)) . x = g . x hence (o .: (h2,f)) . x = o . ((h2 . x),(f . x)) by A13, FUNCOP_1:22 .= g . x by A7, A15 ; ::_thesis: verum end; o .: (h2,f) = ((o,D) .: A) . (h2,f) by Def2; hence ((o,D) .: A) . (h2,f) = g by A13, A9, A14, FUNCT_1:2; ::_thesis: verum end; theorem Th13: :: MONOID_1:13 for A being set for D being non empty set for o being BinOp of D st o is cancelable holds (o,D) .: A is cancelable proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is cancelable holds (o,D) .: A is cancelable let D be non empty set ; ::_thesis: for o being BinOp of D st o is cancelable holds (o,D) .: A is cancelable let o be BinOp of D; ::_thesis: ( o is cancelable implies (o,D) .: A is cancelable ) assume A1: for a, b, c being Element of D st ( o . (a,b) = o . (a,c) or o . (b,a) = o . (c,a) ) holds b = c ; :: according to MONOID_0:def_8 ::_thesis: (o,D) .: A is cancelable let f, g, h be Element of Funcs (A,D); :: according to MONOID_0:def_8 ::_thesis: ( ( not ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) & not ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) ) or g = h ) assume A2: ( ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) or ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) ) ; ::_thesis: g = h 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__::_thesis:_for_x_being_set_st_x_in_A_holds_ g_._x_=_h_._x let x be set ; ::_thesis: ( x in A implies g . x = h . x ) assume A8: x in A ; ::_thesis: g . x = h . x 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; ::_thesis: verum end; ( dom g = A & dom h = A ) by FUNCT_2:def_1; hence g = h by A7, FUNCT_1:2; ::_thesis: verum end; theorem Th14: :: MONOID_1:14 for A being set for D being non empty set for o being BinOp of D st o is uniquely-decomposable holds (o,D) .: A is uniquely-decomposable proof let A be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is uniquely-decomposable holds (o,D) .: A is uniquely-decomposable let D be non empty set ; ::_thesis: for o being BinOp of D st o is uniquely-decomposable holds (o,D) .: A is uniquely-decomposable let o be BinOp of D; ::_thesis: ( o is uniquely-decomposable implies (o,D) .: A is uniquely-decomposable ) assume that A1: o is having_a_unity and A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds ( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def_9 ::_thesis: (o,D) .: A is uniquely-decomposable 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; :: according to MONOID_0:def_9 ::_thesis: for b1, b2 being Element of Funcs (A,D) holds ( not ((o,D) .: A) . (b1,b2) = the_unity_wrt ((o,D) .: A) or ( b1 = b2 & b2 = the_unity_wrt ((o,D) .: A) ) ) let f, g be Element of Funcs (A,D); ::_thesis: ( not ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) or ( f = g & g = the_unity_wrt ((o,D) .: A) ) ) assume A4: ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) ; ::_thesis: ( f = g & 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__::_thesis:_for_x_being_set_st_x_in_A_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in A implies f . x = g . x ) assume A8: x in A ; ::_thesis: f . x = g . x 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, FUNCOP_1:22; hence f . x = g . x by A2, A4, A6, A3; ::_thesis: verum end; A9: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ g_._x_=_(A_-->_(the_unity_wrt_o))_._x let x be set ; ::_thesis: ( x in A implies g . x = (A --> (the_unity_wrt o)) . x ) assume A10: x in A ; ::_thesis: g . x = (A --> (the_unity_wrt o)) . x 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, FUNCOP_1:22; hence g . x = (A --> (the_unity_wrt o)) . x by A2, A4, A6, A3; ::_thesis: verum 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; ::_thesis: g = the_unity_wrt ((o,D) .: A) dom (A --> (the_unity_wrt o)) = A by FUNCT_2:def_1; hence g = the_unity_wrt ((o,D) .: A) by A3, A11, A9, FUNCT_1:2; ::_thesis: verum end; theorem :: MONOID_1:15 for A being set for D being non empty set for o, o9 being BinOp of D st o absorbs o9 holds (o,D) .: A absorbs (o9,D) .: A proof let A be set ; ::_thesis: for D being non empty set for o, o9 being BinOp of D st o absorbs o9 holds (o,D) .: A absorbs (o9,D) .: A let D be non empty set ; ::_thesis: for o, o9 being BinOp of D st o absorbs o9 holds (o,D) .: A absorbs (o9,D) .: A let o, o9 be BinOp of D; ::_thesis: ( o absorbs o9 implies (o,D) .: A absorbs (o9,D) .: A ) assume A1: for a, b being Element of D holds o . (a,(o9 . (a,b))) = a ; :: according to LATTICE2:def_1 ::_thesis: (o,D) .: A absorbs (o9,D) .: A let f, g be Element of Funcs (A,D); :: according to LATTICE2:def_1 ::_thesis: ((o,D) .: A) . (f,(((o9,D) .: A) . (f,g))) = f 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__::_thesis:_for_x_being_set_st_x_in_A_holds_ f_._x_=_(o_.:_(f,(o9_.:_(f,g))))_._x let x be set ; ::_thesis: ( x in A implies f . x = (o .: (f,(o9 .: (f,g)))) . x ) assume A5: x in A ; ::_thesis: f . x = (o .: (f,(o9 .: (f,g)))) . x 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; ::_thesis: verum 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 ((o,D) .: A) . (f,(((o9,D) .: A) . (f,g))) = f by A6, A2, A4, FUNCT_1:2; ::_thesis: verum end; theorem Th16: :: MONOID_1:16 for A being set for D1, D2, D, E1, E2, E being non empty set for o1 being Function of [:D1,D2:],D for o2 being Function of [:E1,E2:],E st o1 c= o2 holds (o1,D) .: A c= (o2,E) .: A proof let A be set ; ::_thesis: for D1, D2, D, E1, E2, E being non empty set for o1 being Function of [:D1,D2:],D for o2 being Function of [:E1,E2:],E st o1 c= o2 holds (o1,D) .: A c= (o2,E) .: A let D1, D2, D, E1, E2, E be non empty set ; ::_thesis: for o1 being Function of [:D1,D2:],D for o2 being Function of [:E1,E2:],E st o1 c= o2 holds (o1,D) .: A c= (o2,E) .: A let o1 be Function of [:D1,D2:],D; ::_thesis: for o2 being Function of [:E1,E2:],E st o1 c= o2 holds (o1,D) .: A c= (o2,E) .: A let o2 be Function of [:E1,E2:],E; ::_thesis: ( o1 c= o2 implies (o1,D) .: A c= (o2,E) .: A ) A1: dom o1 = [:D1,D2:] by FUNCT_2:def_1; assume A2: o1 c= o2 ; ::_thesis: (o1,D) .: A c= (o2,E) .: A 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__::_thesis:_for_x_being_set_st_x_in_dom_((o1,D)_.:_A)_holds_ ((o1,D)_.:_A)_._x_=_((o2,E)_.:_A)_._x let x be set ; ::_thesis: ( x in dom ((o1,D) .: A) implies ((o1,D) .: A) . x = ((o2,E) .: A) . x ) assume x in dom ((o1,D) .: A) ; ::_thesis: ((o1,D) .: A) . x = ((o2,E) .: A) . x 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, TARSKI:def_3; reconsider f2 = y `2 as Element of Funcs (A,D2) ; reconsider g1 = y `1 as Element of Funcs (A,E1) by A6, TARSKI:def_3; 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__::_thesis:_for_z_being_set_st_z_in_A_holds_ (o2_.:_(g1,g2))_._z_=_(o1_.:_(f1,f2))_._z let z be set ; ::_thesis: ( z in A implies (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z ) assume A11: z in A ; ::_thesis: (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z 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; ::_thesis: verum 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; ::_thesis: verum 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 (o1,D) .: A c= (o2,E) .: A by A7, GRFUNC_1:2; ::_thesis: verum end; definition let G be non empty multMagma ; let A be set ; func .: (G,A) -> multMagma equals :Def3: :: MONOID_1:def 3 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 coherence ( ( G is unital implies multLoopStr(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A),(A --> (the_unity_wrt the multF of G)) #) is multMagma ) & ( not G is unital implies multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) is multMagma ) ); consistency for b1 being multMagma holds verum; ; end; :: deftheorem Def3 defines .: MONOID_1:def_3_:_ for G being non empty multMagma for A being set holds ( ( G is unital implies .: (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)) #) ) & ( not G is unital implies .: (G,A) = multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) ) ); registration let G be non empty multMagma ; let A be set ; cluster .: (G,A) -> non empty ; coherence not .: (G,A) is empty proof percases ( G is unital or not G is unital ) ; suppose G is unital ; ::_thesis: not .: (G,A) is empty 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 not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; suppose not G is unital ; ::_thesis: not .: (G,A) is empty then .: (G,A) = multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) by Def3; hence not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; end; end; deffunc H3( non empty multMagma ) -> set = the carrier of \$1; theorem Th17: :: MONOID_1:17 for X being set for G being non empty multMagma holds ( 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 let X be set ; ::_thesis: for G being non empty multMagma holds ( 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 ) let G be non empty multMagma ; ::_thesis: ( 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 ) A1: ( not G is unital implies .: (G,X) = multMagma(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X) #) ) by Def3; ( G is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X),(X --> (the_unity_wrt H1(G))) #) ) by Def3; hence ( 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 ) by A1; ::_thesis: verum end; theorem :: MONOID_1:18 for x, X being set for G being non empty multMagma holds ( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G ) proof let x, X be set ; ::_thesis: for G being non empty multMagma holds ( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G ) let G be non empty multMagma ; ::_thesis: ( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G ) ( x is Element of (.: (G,X)) implies x is Element of Funcs (X,H3(G)) ) by Th17; hence ( x is Element of (.: (G,X)) implies x is Function of X,H3(G) ) ; ::_thesis: ( x is Function of X, the carrier of G implies x is Element of (.: (G,X)) ) assume x is Function of X,H3(G) ; ::_thesis: x is Element of (.: (G,X)) then reconsider f = x as Function of X,H3(G) ; A1: rng f c= H3(G) ; ( H3( .: (G,X)) = Funcs (X,H3(G)) & dom f = X ) by Th17, FUNCT_2:def_1; hence x is Element of (.: (G,X)) by A1, FUNCT_2:def_2; ::_thesis: verum end; Lm1: for X being set for G being non empty multMagma holds .: (G,X) is constituted-Functions proof let X be set ; ::_thesis: for G being non empty multMagma holds .: (G,X) is constituted-Functions let G be non empty multMagma ; ::_thesis: .: (G,X) is constituted-Functions let a be Element of (.: (G,X)); :: according to MONOID_0:def_1 ::_thesis: a is set a is Element of Funcs (X,H3(G)) by Th17; hence a is set ; ::_thesis: verum end; registration let G be non empty multMagma ; let A be set ; cluster .: (G,A) -> constituted-Functions ; coherence .: (G,A) is constituted-Functions by Lm1; end; theorem Th19: :: MONOID_1:19 for X being set for G being non empty multMagma for f being Element of (.: (G,X)) holds ( dom f = X & rng f c= the carrier of G ) proof let X be set ; ::_thesis: for G being non empty multMagma for f being Element of (.: (G,X)) holds ( dom f = X & rng f c= the carrier of G ) let G be non empty multMagma ; ::_thesis: for f being Element of (.: (G,X)) holds ( dom f = X & rng f c= the carrier of G ) let f be Element of (.: (G,X)); ::_thesis: ( dom f = X & rng f c= the carrier of G ) reconsider f = f as Element of Funcs (X,H3(G)) by Th17; f = f ; hence ( dom f = X & rng f c= the carrier of G ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum end; theorem Th20: :: MONOID_1:20 for X being set for G being non empty multMagma for f, g being Element of (.: (G,X)) st ( for x being set st x in X holds f . x = g . x ) holds f = g proof let X be set ; ::_thesis: for G being non empty multMagma for f, g being Element of (.: (G,X)) st ( for x being set st x in X holds f . x = g . x ) holds f = g let G be non empty multMagma ; ::_thesis: for f, g being Element of (.: (G,X)) st ( for x being set st x in X holds f . x = g . x ) holds f = g let f, g be Element of (.: (G,X)); ::_thesis: ( ( for x being set st x in X holds f . x = g . x ) implies f = g ) ( dom f = X & dom g = X ) by Th19; hence ( ( for x being set st x in X holds f . x = g . x ) implies f = g ) by FUNCT_1:2; ::_thesis: verum end; definition let G be non empty multMagma ; let A be non empty set ; let f be Element of (.: (G,A)); let a be Element of A; :: original: . redefine funcf . a -> Element of G; coherence f . a is Element of G proof dom f = A by Th19; then A1: f . a in rng f by FUNCT_1:def_3; rng f c= H3(G) by Th19; hence f . a is Element of G by A1; ::_thesis: verum end; end; registration let G be non empty multMagma ; let A be non empty set ; let f be Element of (.: (G,A)); cluster rng f -> non empty ; coherence not rng f is empty proof set a = the Element of A; dom f = A by Th19; then f . the Element of A in rng f by FUNCT_1:def_3; hence not rng f is empty ; ::_thesis: verum end; end; theorem Th21: :: MONOID_1:21 for D being non empty set for G being non empty multMagma for f1, f2 being Element of (.: (G,D)) for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a) proof let D be non empty set ; ::_thesis: for G being non empty multMagma for f1, f2 being Element of (.: (G,D)) for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a) let G be non empty multMagma ; ::_thesis: for f1, f2 being Element of (.: (G,D)) for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a) let f1, f2 be Element of (.: (G,D)); ::_thesis: for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a) let a be Element of D; ::_thesis: (f1 * f2) . a = (f1 . a) * (f2 . a) reconsider g1 = f1, g2 = f2 as Element of Funcs (D,H3(G)) by Th17; H1( .: (G,D)) = (H1(G),H3(G)) .: D by Th17; then ( dom (H1(G) .: (g1,g2)) = D & f1 * f2 = H1(G) .: (g1,g2) ) by Def2, FUNCT_2:def_1; hence (f1 * f2) . a = (f1 . a) * (f2 . a) by FUNCOP_1:22; ::_thesis: verum end; definition let G be non empty unital multMagma ; let A be set ; :: original: .: redefine func .: (G,A) -> non empty strict well-unital constituted-Functions multLoopStr ; coherence .: (G,A) is non empty strict well-unital constituted-Functions multLoopStr proof set M = multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #); H1(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 H1(G) by SETWISEO:def_2; A2: ( 1. multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #) = A --> (the_unity_wrt the multF of G) & .: (G,A) = multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #) ) by Def3; ( a = the_unity_wrt H1(G) & A --> a is_a_unity_wrt (H1(G),H3(G)) .: A ) by A1, Th9, BINOP_1:def_8; hence .: (G,A) is non empty strict well-unital constituted-Functions multLoopStr by A2, MONOID_0:def_21; ::_thesis: verum end; end; theorem Th22: :: MONOID_1:22 for X being set for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) proof let X be set ; ::_thesis: for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) let G be non empty unital multMagma ; ::_thesis: 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) .: (G,X) = multLoopStr(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X),(X --> (the_unity_wrt H1(G))) #) by Def3; hence 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) ; ::_thesis: verum end; theorem Th23: :: MONOID_1:23 for G being non empty multMagma for 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 be non empty multMagma ; ::_thesis: for 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 ) ) let A be set ; ::_thesis: ( ( 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 ) ) A1: ( H1( .: (G,A)) = (H1(G),H3(G)) .: A & H3( .: (G,A)) = Funcs (A,H3(G)) ) by Th17; thus ( G is commutative implies .: (G,A) is commutative ) ::_thesis: ( ( 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 assume H1(G) is commutative ; :: according to MONOID_0:def_11 ::_thesis: .: (G,A) is commutative hence H1( .: (G,A)) is commutative by A1, Th7; :: according to MONOID_0:def_11 ::_thesis: verum end; thus ( G is associative implies .: (G,A) is associative ) ::_thesis: ( ( 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 assume H1(G) is associative ; :: according to MONOID_0:def_12 ::_thesis: .: (G,A) is associative hence H1( .: (G,A)) is associative by A1, Th8; :: according to MONOID_0:def_12 ::_thesis: verum end; thus ( G is idempotent implies .: (G,A) is idempotent ) ::_thesis: ( ( 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 assume H1(G) is idempotent ; :: according to MONOID_0:def_13 ::_thesis: .: (G,A) is idempotent hence H1( .: (G,A)) is idempotent by A1, Th11; :: according to MONOID_0:def_13 ::_thesis: verum end; thus ( G is invertible implies .: (G,A) is invertible ) ::_thesis: ( ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) ) proof assume H1(G) is invertible ; :: according to MONOID_0:def_16 ::_thesis: .: (G,A) is invertible hence H1( .: (G,A)) is invertible by A1, Th12; :: according to MONOID_0:def_16 ::_thesis: verum end; thus ( G is cancelable implies .: (G,A) is cancelable ) ::_thesis: ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) proof assume H1(G) is cancelable ; :: according to MONOID_0:def_19 ::_thesis: .: (G,A) is cancelable hence H1( .: (G,A)) is cancelable by A1, Th13; :: according to MONOID_0:def_19 ::_thesis: verum end; assume H1(G) is uniquely-decomposable ; :: according to MONOID_0:def_20 ::_thesis: .: (G,A) is uniquely-decomposable hence H1( .: (G,A)) is uniquely-decomposable by A1, Th14; :: according to MONOID_0:def_20 ::_thesis: verum end; theorem :: MONOID_1:24 for X being set for G being non empty multMagma for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X) proof let X be set ; ::_thesis: for G being non empty multMagma for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X) let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X) let H be non empty SubStr of G; ::_thesis: .: (H,X) is SubStr of .: (G,X) A1: H1( .: (H,X)) = (H1(H),H3(H)) .: X by Th17; ( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X ) by Th17, MONOID_0:def_23; hence H1( .: (H,X)) c= H1( .: (G,X)) by A1, Th16; :: according to MONOID_0:def_23 ::_thesis: verum end; theorem :: MONOID_1:25 for X being set for G being non empty unital multMagma for 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 X be set ; ::_thesis: for G being non empty unital multMagma for 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) let G be non empty unital multMagma ; ::_thesis: for 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) let H be non empty SubStr of G; ::_thesis: ( the_unity_wrt the multF of G in the carrier of H implies .: (H,X) is MonoidalSubStr of .: (G,X) ) assume A1: the_unity_wrt the multF of G in H3(H) ; ::_thesis: .: (H,X) is MonoidalSubStr of .: (G,X) then reconsider G9 = G, H9 = H as non empty unital multMagma by MONOID_0:30; A2: the_unity_wrt H1(H9) = the_unity_wrt H1(G9) by A1, MONOID_0:30; A3: H1( .: (H,X)) = (H1(H),H3(H)) .: X by Th17; ( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X ) by Th17, MONOID_0:def_23; then A4: H1( .: (H,X)) c= H1( .: (G,X)) by A3, Th16; ( 1. (.: (G9,X)) = X --> (the_unity_wrt H1(G)) & 1. (.: (H9,X)) = X --> (the_unity_wrt H1(H)) ) by Th22; hence .: (H,X) is MonoidalSubStr of .: (G,X) by A2, A4, MONOID_0:def_25; ::_thesis: verum end; definition let G be non empty unital associative commutative cancelable uniquely-decomposable multMagma ; let A be set ; :: original: .: redefine func .: (G,A) -> strict commutative constituted-Functions cancelable uniquely-decomposable Monoid; coherence .: (G,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid proof ( .: (G,A) is commutative & .: (G,A) is cancelable ) by Th23; hence .: (G,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid by Th23; ::_thesis: verum end; end; begin definition let A be set ; func MultiSet_over A -> strict commutative constituted-Functions cancelable uniquely-decomposable Monoid equals :: MONOID_1:def 4 .: (,A); correctness coherence .: (,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid; ; end; :: deftheorem defines MultiSet_over MONOID_1:def_4_:_ for A being set holds MultiSet_over A = .: (,A); theorem Th26: :: MONOID_1:26 for X being set holds ( 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 let X be set ; ::_thesis: ( the carrier of (MultiSet_over X) = Funcs (X,NAT) & the multF of (MultiSet_over X) = (addnat,NAT) .: X & 1. (MultiSet_over X) = X --> 0 ) ( multMagma(# the carrier of , the multF of #) = & the_unity_wrt H1( ) = 0 ) by MONOID_0:40, MONOID_0:def_22; hence ( the carrier of (MultiSet_over X) = Funcs (X,NAT) & the multF of (MultiSet_over X) = (addnat,NAT) .: X & 1. (MultiSet_over X) = X --> 0 ) by Th17, Th22, MONOID_0:46; ::_thesis: verum end; definition let A be set ; mode Multiset of A is Element of (MultiSet_over A); end; theorem Th27: :: MONOID_1:27 for x, X being set holds ( x is Multiset of X iff x is Function of X,NAT ) proof let x, X be set ; ::_thesis: ( x is Multiset of X iff x is Function of X,NAT ) A1: now__::_thesis:_for_x_being_Function_of_X,NAT_holds_x_is_Element_of_Funcs_(X,NAT) let x be Function of X,NAT; ::_thesis: x is Element of Funcs (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; ::_thesis: verum end; ( x is Multiset of X iff x is Element of Funcs (X,NAT) ) by Th26; hence ( x is Multiset of X iff x is Function of X,NAT ) by A1; ::_thesis: verum end; theorem Th28: :: MONOID_1:28 for X being set for m being Multiset of X holds ( dom m = X & rng m c= NAT ) proof let X be set ; ::_thesis: for m being Multiset of X holds ( dom m = X & rng m c= NAT ) let m be Multiset of X; ::_thesis: ( dom m = X & rng m c= NAT ) m is Function of X,NAT by Th27; hence ( dom m = X & rng m c= NAT ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum end; definition let A be non empty set ; let m be Multiset of A; :: original: rng redefine func rng m -> Subset of NAT; coherence rng m is Subset of NAT by Th19, MONOID_0:46; let a be Element of A; :: original: . redefine funcm . a -> Element of NAT ; coherence m . a is Element of NAT proof dom m = A by Th19; then A1: m . a in rng m by FUNCT_1:def_3; rng m c= NAT by Th19, MONOID_0:46; hence m . a is Element of NAT by A1; ::_thesis: verum end; end; theorem Th29: :: MONOID_1:29 for D being non empty set for m1, m2 being Multiset of D for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a) proof let D be non empty set ; ::_thesis: for m1, m2 being Multiset of D for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a) reconsider N = as non empty multMagma ; let m1, m2 be Multiset of D; ::_thesis: for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a) let a be Element of D; ::_thesis: (m1 [*] m2) . a = (m1 . a) + (m2 . a) 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 ; ::_thesis: verum end; theorem Th30: :: MONOID_1:30 for Y, X being set holds chi (Y,X) is Multiset of X proof let Y, X be set ; ::_thesis: chi (Y,X) is Multiset of X rng (chi (Y,X)) c= {0,1} ; then A1: rng (chi (Y,X)) c= NAT by XBOOLE_1:1; ( dom (chi (Y,X)) = X & H3( MultiSet_over X) = Funcs (X,NAT) ) by Th26, FUNCT_3:def_3; hence chi (Y,X) is Multiset of X by A1, FUNCT_2:def_2; ::_thesis: verum end; definition let Y, X be set ; :: original: chi redefine func chi (Y,X) -> Multiset of X; coherence chi (Y,X) is Multiset of X by Th30; end; definition let X be set ; let n be Element of NAT ; :: original: --> redefine funcX --> n -> Multiset of X; coherence X --> n is Multiset of X proof thus X --> n is Multiset of X by Th27; ::_thesis: verum end; end; definition let A be non empty set ; let a be Element of A; func chi a -> Multiset of A equals :: MONOID_1:def 5 chi ({a},A); coherence chi ({a},A) is Multiset of A ; end; :: deftheorem defines chi MONOID_1:def_5_:_ for A being non empty set for a being Element of A holds chi a = chi ({a},A); theorem Th31: :: MONOID_1:31 for A being non empty set for 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 ; ::_thesis: for a, b being Element of A holds ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) let a, b be Element of A; ::_thesis: ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) A1: ( b <> a implies not b in {a} ) by TARSKI:def_1; a in {a} by TARSKI:def_1; hence ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) by A1, FUNCT_3:def_3; ::_thesis: verum end; theorem Th32: :: MONOID_1:32 for A being non empty set for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds m1 = m2 proof let A be non empty set ; ::_thesis: for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds m1 = m2 let m1, m2 be Multiset of A; ::_thesis: ( ( for a being Element of A holds m1 . a = m2 . a ) implies m1 = m2 ) assume for a being Element of A holds m1 . a = m2 . a ; ::_thesis: m1 = m2 then for x being set st x in A holds m1 . x = m2 . x ; hence m1 = m2 by Th20; ::_thesis: verum end; definition let A be set ; func finite-MultiSet_over A -> non empty strict MonoidalSubStr of MultiSet_over A means :Def6: :: MONOID_1:def 6 for f being Multiset of A holds ( f in the carrier of it iff f " (NAT \ {0}) is finite ); existence ex b1 being non empty strict MonoidalSubStr of MultiSet_over A st for f being Multiset of A holds ( f in the carrier of b1 iff f " (NAT \ {0}) is finite ) proof reconsider e = A --> 0 as Function of A,NAT by Th27; defpred S1[ 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 st S1[a] & S1[b] holds S1[a [*] b] proof let a, b be Multiset of A; ::_thesis: ( S1[a] & S1[b] implies S1[a [*] b] ) 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 ; ::_thesis: ( not S1[b] or S1[a [*] b] ) given g being Function of A,NAT such that A4: b = g and A5: g " (NAT \ {0}) is finite ; ::_thesis: S1[a [*] b] take h ; ::_thesis: ( a [*] b = h & h " (NAT \ {0}) is finite ) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h " (NAT \ {0}) or x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) ) assume A7: x in h " (NAT \ {0}) ; ::_thesis: x in (f " (NAT \ {0})) \/ (g " (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 x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) by XBOOLE_0:def_3; ::_thesis: verum end; hence ( a [*] b = h & h " (NAT \ {0}) is finite ) by A3, A5; ::_thesis: verum end; A9: dom e = A by FUNCOP_1:13; now__::_thesis:_not_e_"_(NAT_\_{0})_<>_{} set x = the Element of e " (NAT \ {0}); assume A10: e " (NAT \ {0}) <> {} ; ::_thesis: contradiction then e . the Element of e " (NAT \ {0}) in NAT \ {0} by FUNCT_1:def_7; then A11: not e . the Element of e " (NAT \ {0}) in {0} by XBOOLE_0:def_5; the Element of e " (NAT \ {0}) in A by A9, A10, FUNCT_1:def_7; then e . the Element of e " (NAT \ {0}) = 0 by FUNCOP_1:7; hence contradiction by A11, TARSKI:def_1; ::_thesis: verum end; then A12: S1[ 1. (MultiSet_over A)] by Th26; consider M being non empty strict MonoidalSubStr of MultiSet_over A such that A13: for a being Multiset of A holds ( a in the carrier of M iff S1[a] ) from MONOID_0:sch_2(A1, A12); reconsider M = M as non empty strict MonoidalSubStr of MultiSet_over A ; take M ; ::_thesis: for f being Multiset of A holds ( f in the carrier of M iff f " (NAT \ {0}) is finite ) let f be Multiset of A; ::_thesis: ( f in the carrier of M iff f " (NAT \ {0}) is finite ) thus ( f in H3(M) implies f " (NAT \ {0}) is finite ) ::_thesis: ( f " (NAT \ {0}) is finite implies f in the carrier of M ) proof assume f in H3(M) ; ::_thesis: f " (NAT \ {0}) is finite then ex g being Function of A,NAT st ( f = g & g " (NAT \ {0}) is finite ) by A13; hence f " (NAT \ {0}) is finite ; ::_thesis: verum end; reconsider g = f as Function of A,NAT by Th27; assume f " (NAT \ {0}) is finite ; ::_thesis: f in the carrier of M then g " (NAT \ {0}) is finite ; hence f in the carrier of M by A13; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict MonoidalSubStr of MultiSet_over A st ( for f being Multiset of A holds ( f in the carrier of b1 iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds ( f in the carrier of b2 iff f " (NAT \ {0}) is finite ) ) holds b1 = b2 proof set M = MultiSet_over A; let M1, M2 be non empty strict MonoidalSubStr of MultiSet_over A; ::_thesis: ( ( for f being Multiset of A holds ( f in the carrier of M1 iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds ( f in the carrier of M2 iff f " (NAT \ {0}) is finite ) ) implies M1 = M2 ) assume that A14: for f being Multiset of A holds ( f in H3(M1) iff f " (NAT \ {0}) is finite ) and A15: for f being Multiset of A holds ( f in H3(M2) iff f " (NAT \ {0}) is finite ) ; ::_thesis: M1 = M2 A16: H3(M2) c= H3( MultiSet_over A) by MONOID_0:23; A17: H3(M1) c= H3( MultiSet_over A) by MONOID_0:23; H3(M1) = H3(M2) proof thus H3(M1) c= H3(M2) :: according to XBOOLE_0:def_10 ::_thesis: H3(M2) c= H3(M1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H3(M1) or x in H3(M2) ) assume A18: x in H3(M1) ; ::_thesis: x in H3(M2) then reconsider f = x as Multiset of A by A17; f " (NAT \ {0}) is finite by A14, A18; hence x in H3(M2) by A15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H3(M2) or x in H3(M1) ) assume A19: x in H3(M2) ; ::_thesis: x in H3(M1) then reconsider f = x as Multiset of A by A16; f " (NAT \ {0}) is finite by A15, A19; hence x in H3(M1) by A14; ::_thesis: verum end; hence M1 = M2 by MONOID_0:27; ::_thesis: verum end; end; :: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def_6_:_ for A being set for b2 being non empty strict MonoidalSubStr of MultiSet_over A holds ( b2 = finite-MultiSet_over A iff for f being Multiset of A holds ( f in the carrier of b2 iff f " (NAT \ {0}) is finite ) ); theorem Th33: :: MONOID_1:33 for A being non empty set for a being Element of A holds chi a is Element of (finite-MultiSet_over A) proof let A be non empty set ; ::_thesis: for a being Element of A holds chi a is Element of (finite-MultiSet_over A) let a be Element of A; ::_thesis: chi a is Element of (finite-MultiSet_over A) (chi a) " (NAT \ {0}) c= {a} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (chi a) " (NAT \ {0}) or x in {a} ) assume A1: x in (chi a) " (NAT \ {0}) ; ::_thesis: x in {a} 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 x in {a} by TARSKI:def_1; ::_thesis: verum end; hence chi a is Element of (finite-MultiSet_over A) by Def6; ::_thesis: verum end; theorem Th34: :: MONOID_1:34 for x being set for A being non empty set for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)} proof let x be set ; ::_thesis: for A being non empty set for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)} let A be non empty set ; ::_thesis: for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)} let p be FinSequence of A; ::_thesis: dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)} thus dom ({x} |` (p ^ <*x*>)) c= (dom ({x} |` p)) \/ {((len p) + 1)} :: according to XBOOLE_0:def_10 ::_thesis: (dom ({x} |` p)) \/ {((len p) + 1)} c= dom ({x} |` (p ^ <*x*>)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` (p ^ <*x*>)) or a in (dom ({x} |` p)) \/ {((len p) + 1)} ) 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*>)) ; ::_thesis: a in (dom ({x} |` p)) \/ {((len p) + 1)} 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 = 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 a in (dom ({x} |` p)) \/ {((len p) + 1)} by A5, XBOOLE_0:def_3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (dom ({x} |` p)) \/ {((len p) + 1)} or a in dom ({x} |` (p ^ <*x*>)) ) 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)} ; ::_thesis: a in dom ({x} |` (p ^ <*x*>)) 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, FINSEQ_1: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 = a as Element of NAT by A8; ( a in dom p implies (p ^ <*x*>) . a = p . a ) by FINSEQ_1:def_7; hence a in dom ({x} |` (p ^ <*x*>)) by A9, A10, FUNCT_1:54; ::_thesis: verum end; theorem Th35: :: MONOID_1:35 for x, y being set for A being non empty set for p being FinSequence of A st x <> y holds dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) proof let x, y be set ; ::_thesis: for A being non empty set for p being FinSequence of A st x <> y holds dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) let A be non empty set ; ::_thesis: for p being FinSequence of A st x <> y holds dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) let p be FinSequence of A; ::_thesis: ( x <> y implies dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) ) assume A1: x <> y ; ::_thesis: dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) thus dom ({x} |` (p ^ <*y*>)) c= dom ({x} |` p) :: according to XBOOLE_0:def_10 ::_thesis: dom ({x} |` p) c= dom ({x} |` (p ^ <*y*>)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` (p ^ <*y*>)) or a in dom ({x} |` p) ) 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*>)) ; ::_thesis: a in dom ({x} |` p) 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 = 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 a in dom ({x} |` p) by A7, A6, A8, FUNCT_1:54, TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` p) or a in dom ({x} |` (p ^ <*y*>)) ) assume A9: a in dom ({x} |` p) ; ::_thesis: a in dom ({x} |` (p ^ <*y*>)) 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, FINSEQ_1: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 = a as Element of NAT by A9; (p ^ <*y*>) . a = p . a by A10, FINSEQ_1:def_7; hence a in dom ({x} |` (p ^ <*y*>)) by A13, A12, FUNCT_1:54; ::_thesis: verum end; definition let A be non empty set ; let p be FinSequence of A; func|.p.| -> Multiset of A means :Def7: :: MONOID_1:def 7 for a being Element of A holds it . a = card (dom ({a} |` p)); existence ex b1 being Multiset of A st for a being Element of A holds b1 . a = card (dom ({a} |` p)) proof deffunc H4( Element of A) -> Element of NAT = card (dom ({\$1} |` p)); consider m being Function of A,NAT such that A1: for a being Element of A holds m . a = H4(a) from FUNCT_2:sch_4(); m is Multiset of A by Th27; hence ex b1 being Multiset of A st for a being Element of A holds b1 . a = card (dom ({a} |` p)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Multiset of A st ( for a being Element of A holds b1 . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds b2 . a = card (dom ({a} |` p)) ) holds b1 = b2 proof let m1, m2 be Multiset of A; ::_thesis: ( ( for a being Element of A holds m1 . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds m2 . a = card (dom ({a} |` p)) ) implies m1 = m2 ) assume 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)) ; ::_thesis: m1 = m2 now__::_thesis:_for_a_being_Element_of_A_holds_m1_._a_=_m2_._a let a be Element of A; ::_thesis: m1 . a = m2 . a thus m1 . a = card (dom ({a} |` p)) by A2 .= m2 . a by A3 ; ::_thesis: verum end; hence m1 = m2 by Th32; ::_thesis: verum end; end; :: deftheorem Def7 defines |. MONOID_1:def_7_:_ for A being non empty set for p being FinSequence of A for b3 being Multiset of A holds ( b3 = |.p.| iff for a being Element of A holds b3 . a = card (dom ({a} |` p)) ); theorem :: MONOID_1:36 for A being non empty set for a being Element of A holds |.(<*> A).| . a = 0 proof let A be non empty set ; ::_thesis: for a being Element of A holds |.(<*> A).| . a = 0 let a be Element of A; ::_thesis: |.(<*> A).| . a = 0 dom ({a} |` {}) c= dom {} by FUNCT_1:56; then dom ({a} |` (<*> A)) = {} ; hence |.(<*> A).| . a = 0 by Def7, CARD_1:27; ::_thesis: verum end; theorem Th37: :: MONOID_1:37 for A being non empty set holds |.(<*> A).| = A --> 0 proof let A be non empty set ; ::_thesis: |.(<*> A).| = A --> 0 A1: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ |.(<*>_A).|_._x_=_0 let x be set ; ::_thesis: ( x in A implies |.(<*> A).| . x = 0 ) assume x in A ; ::_thesis: |.(<*> A).| . x = 0 then reconsider a = x as Element of A ; thus |.(<*> A).| . x = card (dom ({a} |` {})) by Def7 .= 0 by CARD_1:27, RELAT_1:38, RELAT_1:107 ; ::_thesis: verum end; dom |.(<*> A).| = A by Th28; hence |.(<*> A).| = A --> 0 by A1, FUNCOP_1:11; ::_thesis: verum end; theorem :: MONOID_1:38 for A being non empty set for a being Element of A holds |.<*a*>.| = chi a proof let A be non empty set ; ::_thesis: for a being Element of A holds |.<*a*>.| = chi a let a be Element of A; ::_thesis: |.<*a*>.| = chi a A1: rng <*a*> = {a} by FINSEQ_1:39; now__::_thesis:_for_b_being_Element_of_A_holds_|.<*a*>.|_._b_=_(chi_a)_._b let b be Element of A; ::_thesis: |.<*a*>.| . b = (chi a) . b set x = b; A2: ( dom <*a*> = Seg 1 & card (Seg 1) = 1 ) by FINSEQ_1:38, FINSEQ_1:57; ( a <> b implies {b} misses {a} ) by ZFMISC_1:11; then A3: ( a <> b implies {b} /\ {a} = {} ) by XBOOLE_0:def_7; A4: ( (chi a) . a = 1 & {a} |` <*a*> = <*a*> ) by A1, Th31, RELAT_1:94; <*a*> = (rng <*a*>) |` <*a*> ; then {b} |` <*a*> = ({b} /\ (rng <*a*>)) |` <*a*> by RELAT_1:96; then ( b <> a implies ( {b} |` <*a*> = {} & (chi a) . b = 0 ) ) by A1, A3, Th31; hence |.<*a*>.| . b = (chi a) . b by A2, A4, Def7, CARD_1:27, RELAT_1:38; ::_thesis: verum end; hence |.<*a*>.| = chi a by Th32; ::_thesis: verum end; theorem Th39: :: MONOID_1:39 for A being non empty set for a being Element of A for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a) proof let A be non empty set ; ::_thesis: for a being Element of A for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a) let a be Element of A; ::_thesis: for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a) let p be FinSequence of A; ::_thesis: |.(p ^ <*a*>).| = |.p.| [*] (chi a) now__::_thesis:_for_b_being_Element_of_A_holds_|.(p_^_<*a*>).|_._b_=_(|.p.|_[*]_(chi_a))_._b reconsider pa = p ^ <*a*> as FinSequence of A ; let b be Element of A; ::_thesis: |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b ( 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; ::_thesis: verum end; hence |.(p ^ <*a*>).| = |.p.| [*] (chi a) by Th32; ::_thesis: verum end; theorem Th40: :: MONOID_1:40 for A being non empty set for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.| proof let A be non empty set ; ::_thesis: for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.| let p, q be FinSequence of A; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.| defpred S1[ Element of NAT ] means for q being FinSequence of A st len q = \$1 holds |.(p ^ q).| = |.p.| [*] |.q.|; A1: len q = len q ; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: for q being FinSequence of A st len q = n holds |.(p ^ q).| = |.p.| [*] |.q.| ; ::_thesis: S1[n + 1] let q be FinSequence of A; ::_thesis: ( len q = n + 1 implies |.(p ^ q).| = |.p.| [*] |.q.| ) assume A4: len q = n + 1 ; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.| then q <> {} ; then consider r being FinSequence, x being set 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 = 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 = 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 ; ::_thesis: verum end; A8: S1[ 0 ] proof let q be FinSequence of A; ::_thesis: ( len q = 0 implies |.(p ^ q).| = |.p.| [*] |.q.| ) A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H2( MultiSet_over A) ) by Th26, Th37; assume len q = 0 ; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.| then A10: q = {} ; then p ^ q = p by FINSEQ_1:34; hence |.(p ^ q).| = |.p.| [*] |.q.| by A10, A9, MONOID_0:16; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2); hence |.(p ^ q).| = |.p.| [*] |.q.| by A1; ::_thesis: verum end; theorem Th41: :: MONOID_1:41 for n being Element of NAT for A being non empty set for a being Element of A holds ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds |.(n .--> a).| . b = 0 ) ) proof let n be Element of NAT ; ::_thesis: for A being non empty set for a being Element of A holds ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds |.(n .--> a).| . b = 0 ) ) let A be non empty set ; ::_thesis: for a being Element of A holds ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds |.(n .--> a).| . b = 0 ) ) let a be Element of A; ::_thesis: ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds |.(n .--> a).| . b = 0 ) ) defpred S1[ Element of NAT ] means |.(\$1 .--> a).| . a = \$1; A1: ( 0 .--> a = {} & {} = <*> A ) by FINSEQ_2:58; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: |.(n .--> a).| . a = n ; ::_thesis: S1[n + 1] thus |.((n + 1) .--> a).| . a = |.((n .--> a) ^ <*a*>).| . a by FINSEQ_2:60 .= (|.(n .--> a).| [*] (chi a)) . a by Th39 .= n + ((chi a) . a) by A3, Th29 .= n + 1 by Th31 ; ::_thesis: verum end; (A --> 0) . a = 0 by FUNCOP_1:7; then A4: S1[ 0 ] by A1, Th37; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence |.(n .--> a).| . a = n ; ::_thesis: for b being Element of A st b <> a holds |.(n .--> a).| . b = 0 let b be Element of A; ::_thesis: ( b <> a implies |.(n .--> a).| . b = 0 ) assume A5: b <> a ; ::_thesis: |.(n .--> a).| . b = 0 defpred S2[ Element of NAT ] means |.(\$1 .--> a).| . b = 0 ; A6: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A7: |.(n .--> a).| . b = 0 ; ::_thesis: S2[n + 1] thus |.((n + 1) .--> a).| . b = |.((n .--> a) ^ <*a*>).| . b by FINSEQ_2:60 .= (|.(n .--> a).| [*] (chi a)) . b by Th39 .= 0 + ((chi a) . b) by A7, Th29 .= 0 by A5, Th31 ; ::_thesis: verum end; (A --> 0) . b = 0 by FUNCOP_1:7; then A8: S2[ 0 ] by A1, Th37; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A8, A6); hence |.(n .--> a).| . b = 0 ; ::_thesis: verum end; theorem :: MONOID_1:42 for A being non empty set for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A) proof let A be non empty set ; ::_thesis: for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A) let p be FinSequence of A; ::_thesis: |.p.| is Element of (finite-MultiSet_over A) defpred S1[ FinSequence of A] means |.\$1.| is Element of (finite-MultiSet_over A); defpred S2[ Element of NAT ] means for p being FinSequence of A st len p = \$1 holds S1[p]; A1: len p = len p ; A2: for n being Element of NAT st S2[n] holds S2[n + 1] proof set M = finite-MultiSet_over A; let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A3: for p being FinSequence of A st len p = n holds S1[p] ; ::_thesis: S2[n + 1] let p be FinSequence of A; ::_thesis: ( len p = n + 1 implies S1[p] ) assume A4: len p = n + 1 ; ::_thesis: S1[p] then p <> {} ; then consider r being FinSequence, x being set 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 = r as FinSequence of A by A5, FINSEQ_1:36; A7: len <*x*> = 1 by FINSEQ_1:40; reconsider x = 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 (finite-MultiSet_over A) by A3, Th33; finite-MultiSet_over A 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 S1[p] ; ::_thesis: verum end; A8: S2[ 0 ] proof let p be FinSequence of A; ::_thesis: ( len p = 0 implies S1[p] ) assume len p = 0 ; ::_thesis: S1[p] then p = <*> A ; then |.p.| = A --> 0 by Th37 .= H2( MultiSet_over A) by Th26 .= H2( finite-MultiSet_over A) by MONOID_0:def_24 ; hence S1[p] ; ::_thesis: verum end; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A8, A2); hence |.p.| is Element of (finite-MultiSet_over A) by A1; ::_thesis: verum end; theorem :: MONOID_1:43 for x being set for A being non empty set st x is Element of (finite-MultiSet_over A) holds ex p being FinSequence of A st x = |.p.| proof let x be set ; ::_thesis: for A being non empty set st x is Element of (finite-MultiSet_over A) holds ex p being FinSequence of A st x = |.p.| let A be non empty set ; ::_thesis: ( x is Element of (finite-MultiSet_over A) implies ex p being FinSequence of A st x = |.p.| ) defpred S1[ Element of NAT ] means for fm being Element of (finite-MultiSet_over A) st ( for V being finite set st V = fm " (NAT \ {0}) holds card V = \$1 ) holds ex p being FinSequence of A st fm = |.p.|; assume x is Element of (finite-MultiSet_over A) ; ::_thesis: ex p being FinSequence of A st x = |.p.| then reconsider m = x as Element of (finite-MultiSet_over A) ; H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23; then m is Multiset of A by TARSKI:def_3; 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 Element of NAT st S1[n] holds S1[n + 1] proof deffunc H4( set ) -> Element of NAT = 0 ; let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: for fm being Element of (finite-MultiSet_over A) st ( for V being finite set st V = fm " (NAT \ {0}) holds card V = n ) holds ex p being FinSequence of A st fm = |.p.| ; ::_thesis: S1[n + 1] let fm be Element of (finite-MultiSet_over A); ::_thesis: ( ( for V being finite set st V = fm " (NAT \ {0}) holds card V = n + 1 ) implies ex p being FinSequence of A st fm = |.p.| ) assume A4: for V being finite set st V = fm " (NAT \ {0}) holds card V = n + 1 ; ::_thesis: ex p being FinSequence of A st fm = |.p.| deffunc H5( set ) -> set = fm . \$1; set x = the Element of fm " (NAT \ {0}); H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23; then reconsider m = fm as Multiset of A by TARSKI:def_3; 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 = the Element of fm " (NAT \ {0}) as Element of A by A5, CARD_1:27, FUNCT_1:def_7; defpred S2[ set ] means x = \$1; consider f being Function such that A7: ( dom f = A & ( for a being set st a in A holds ( ( S2[a] implies f . a = H4(a) ) & ( not S2[a] implies f . a = H5(a) ) ) ) ) from PARTFUN1:sch_1(); rng f c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT ) assume y in rng f ; ::_thesis: y in NAT then consider z being set such that A8: z in dom f and A9: y = f . z by FUNCT_1:def_3; reconsider z = z as Element of A by A7, A8; ( y = 0 or y = m . z ) by A7, A9; hence y in NAT ; ::_thesis: verum end; then reconsider f = f as Function of A,NAT by A7, FUNCT_2:def_1, RELSET_1:4; reconsider f = 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} :: according to XBOOLE_0:def_10 ::_thesis: (fm " (NAT \ {0})) \ {x} c= f " (NAT \ {0}) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " (NAT \ {0}) or y in (fm " (NAT \ {0})) \ {x} ) assume A11: y in f " (NAT \ {0}) ; ::_thesis: y in (fm " (NAT \ {0})) \ {x} 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 y in (fm " (NAT \ {0})) \ {x} by A14, XBOOLE_0:def_5; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (fm " (NAT \ {0})) \ {x} or y in f " (NAT \ {0}) ) assume A15: y in (fm " (NAT \ {0})) \ {x} ; ::_thesis: y in f " (NAT \ {0}) 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 y in f " (NAT \ {0}) by A6, A7, A16, A17, FUNCT_1:def_7; ::_thesis: verum 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 being FinSequence of A such that A19: f = |.p.| by A3; take q = p ^ ((m . x) .--> x); ::_thesis: fm = |.q.| now__::_thesis:_for_a_being_Element_of_A_holds_(f_[*]_|.((m_._x)_.-->_x).|)_._a_=_m_._a let a be Element of A; ::_thesis: (f [*] |.((m . x) .--> x).|) . a = m . a A20: 0 + (m . a) = m . a ; A21: ( a <> x implies ( f . a = m . a & |.((m . x) .--> x).| . a = 0 ) ) by A7, Th41; ( f . x = 0 & |.((m . x) .--> x).| . x = m . x ) by A7, Th41; hence (f [*] |.((m . x) .--> x).|) . a = m . a by A20, A21, Th29; ::_thesis: verum end; hence fm = f [*] |.((m . x) .--> x).| by Th32 .= |.q.| by A19, Th40 ; ::_thesis: verum end; A22: S1[ 0 ] proof set a = the Element of A; let fm be Element of (finite-MultiSet_over A); ::_thesis: ( ( for V being finite set st V = fm " (NAT \ {0}) holds card V = 0 ) implies ex p being FinSequence of A st fm = |.p.| ) assume A23: for V being finite set st V = fm " (NAT \ {0}) holds card V = 0 ; ::_thesis: ex p being FinSequence of A st fm = |.p.| H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23; 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 A23; then fm " (NAT \ {0}) = {} ; then rng fm misses NAT \ {0} by RELAT_1:138; then A24: {} = (rng fm) /\ (NAT \ {0}) by XBOOLE_0:def_7 .= ((rng fm) /\ NAT) \ {0} by XBOOLE_1:49 ; take p = <*> A; ::_thesis: fm = |.p.| 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 . the Element of A in rng fm by FUNCT_1:def_3; then fm . the Element of A = 0 by A25, TARSKI:def_1; then {0} c= rng fm by A27, ZFMISC_1:31; then rng fm = {0} by A25, XBOOLE_0:def_10; hence fm = A --> 0 by A26, FUNCOP_1:9 .= |.p.| by Th37 ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A22, A2); hence ex p being FinSequence of A st x = |.p.| by A1; ::_thesis: verum end; begin definition let D1, D2, D be non empty set ; let f be Function of [:D1,D2:],D; funcf .:^2 -> Function of [:(bool D1),(bool D2):],(bool D) means :Def8: :: MONOID_1:def 8 for x being Element of [:(bool D1),(bool D2):] holds it . x = f .: [:(x `1),(x `2):]; existence ex b1 being Function of [:(bool D1),(bool D2):],(bool D) st for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1),(x `2):] proof deffunc H4( Element of [:(bool D1),(bool D2):]) -> Element of bool D = 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 = H4(x) from FUNCT_2:sch_4(); hence ex b1 being Function of [:(bool D1),(bool D2):],(bool D) st for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1),(x `2):] ; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:(bool D1),(bool D2):],(bool D) st ( for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds b2 . x = f .: [:(x `1),(x `2):] ) holds b1 = b2 proof let F1, F2 be Function of [:(bool D1),(bool D2):],(bool D); ::_thesis: ( ( for x being Element of [:(bool D1),(bool D2):] holds F1 . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds F2 . x = f .: [:(x `1),(x `2):] ) implies F1 = F2 ) assume 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):] ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_Element_of_[:(bool_D1),(bool_D2):]_holds_F1_._x_=_F2_._x let x be Element of [:(bool D1),(bool D2):]; ::_thesis: F1 . x = F2 . x thus F1 . x = f .: [:(x `1),(x `2):] by A1 .= F2 . x by A2 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def8 defines .:^2 MONOID_1:def_8_:_ for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for b5 being Function of [:(bool D1),(bool D2):],(bool D) holds ( b5 = f .:^2 iff for x being Element of [:(bool D1),(bool D2):] holds b5 . x = f .: [:(x `1),(x `2):] ); theorem Th44: :: MONOID_1:44 for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for X1 being Subset of D1 for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:] proof let D1, D2, D be non empty set ; ::_thesis: for f being Function of [:D1,D2:],D for X1 being Subset of D1 for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:] let f be Function of [:D1,D2:],D; ::_thesis: for X1 being Subset of D1 for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:] let X1 be Subset of D1; ::_thesis: for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:] let X2 be Subset of D2; ::_thesis: (f .:^2) . (X1,X2) = f .: [:X1,X2:] ( [X1,X2] `1 = X1 & [X1,X2] `2 = X2 ) by MCART_1:7; hence (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Def8; ::_thesis: verum end; theorem Th45: :: MONOID_1:45 for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for X1 being Subset of D1 for X2 being Subset of D2 for 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 ; ::_thesis: for f being Function of [:D1,D2:],D for X1 being Subset of D1 for X2 being Subset of D2 for x1, x2 being set st x1 in X1 & x2 in X2 holds f . (x1,x2) in (f .:^2) . (X1,X2) let f be Function of [:D1,D2:],D; ::_thesis: for X1 being Subset of D1 for X2 being Subset of D2 for x1, x2 being set st x1 in X1 & x2 in X2 holds f . (x1,x2) in (f .:^2) . (X1,X2) let X1 be Subset of D1; ::_thesis: for X2 being Subset of D2 for x1, x2 being set st x1 in X1 & x2 in X2 holds f . (x1,x2) in (f .:^2) . (X1,X2) let X2 be Subset of D2; ::_thesis: for x1, x2 being set st x1 in X1 & x2 in X2 holds f . (x1,x2) in (f .:^2) . (X1,X2) let x1, x2 be set ; ::_thesis: ( x1 in X1 & x2 in X2 implies f . (x1,x2) in (f .:^2) . (X1,X2) ) assume that A1: x1 in X1 and A2: x2 in X2 ; ::_thesis: f . (x1,x2) in (f .:^2) . (X1,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 f . (x1,x2) in (f .:^2) . (X1,X2) by A3, FUNCT_1:def_6; ::_thesis: verum end; theorem :: MONOID_1:46 for D1, D2, D being non empty set for f being Function of [:D1,D2:],D for X1 being Subset of D1 for 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 ; ::_thesis: for f being Function of [:D1,D2:],D for X1 being Subset of D1 for 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 ) } let f be Function of [:D1,D2:],D; ::_thesis: for X1 being Subset of D1 for 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 ) } let X1 be Subset of D1; ::_thesis: for 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 ) } let X2 be Subset of D2; ::_thesis: (f .:^2) . (X1,X2) = { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } 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= { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } c= (f .:^2) . (X1,X2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f .:^2) . (X1,X2) or x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } ) assume x in (f .:^2) . (X1,X2) ; ::_thesis: x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } then consider y being set 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 set such that A4: y1 in X1 and A5: y2 in X2 and A6: y = [y1,y2] by A2, ZFMISC_1:84; reconsider y2 = y2 as Element of D2 by A5; reconsider y1 = y1 as Element of D1 by A4; x = f . (y1,y2) by A3, A6; hence x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } by A4, A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } or x in (f .:^2) . (X1,X2) ) assume x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } ; ::_thesis: x in (f .:^2) . (X1,X2) then ex a being Element of D1 ex b being Element of D2 st ( x = f . (a,b) & a in X1 & b in X2 ) ; hence x in (f .:^2) . (X1,X2) by Th45; ::_thesis: verum end; theorem Th47: :: MONOID_1:47 for X, Y being set for D being non empty set for o being BinOp of D st o is commutative holds o .: [:X,Y:] = o .: [:Y,X:] proof let X, Y be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is commutative holds o .: [:X,Y:] = o .: [:Y,X:] let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds o .: [:X,Y:] = o .: [:Y,X:] let o be BinOp of D; ::_thesis: ( o is commutative implies o .: [:X,Y:] = o .: [:Y,X:] ) assume A1: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: o .: [:X,Y:] = o .: [:Y,X:] now__::_thesis:_for_X,_Y_being_set_holds_o_.:_[:X,Y:]_c=_o_.:_[:Y,X:] let X, Y be set ; ::_thesis: o .: [:X,Y:] c= o .: [:Y,X:] thus o .: [:X,Y:] c= o .: [:Y,X:] ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,Y:] or x in o .: [:Y,X:] ) assume x in o .: [:X,Y:] ; ::_thesis: x in o .: [:Y,X:] then consider y being set 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 = 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 x in o .: [:Y,X:] by A6, A5, FUNCT_1:def_6; ::_thesis: verum end; end; hence ( o .: [:X,Y:] c= o .: [:Y,X:] & o .: [:Y,X:] c= o .: [:X,Y:] ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum end; theorem Th48: :: MONOID_1:48 for X, Y, Z being set for D being non empty set for o being BinOp of D st o is associative holds o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] proof let X, Y, Z be set ; ::_thesis: for D being non empty set for o being BinOp of D st o is associative holds o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] let o be BinOp of D; ::_thesis: ( o is associative implies o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] ) A1: dom o = [:D,D:] by FUNCT_2:def_1; assume A2: for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] thus o .: [:(o .: [:X,Y:]),Z:] c= o .: [:X,(o .: [:Y,Z:]):] :: according to XBOOLE_0:def_10 ::_thesis: o .: [:X,(o .: [:Y,Z:]):] c= o .: [:(o .: [:X,Y:]),Z:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:(o .: [:X,Y:]),Z:] or x in o .: [:X,(o .: [:Y,Z:]):] ) assume x in o .: [:(o .: [:X,Y:]),Z:] ; ::_thesis: x in o .: [:X,(o .: [:Y,Z:]):] then consider y being set 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 = 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 set 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 = 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 x in o .: [:X,(o .: [:Y,Z:]):] by A1, A14, FUNCT_1:def_6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,(o .: [:Y,Z:]):] or x in o .: [:(o .: [:X,Y:]),Z:] ) assume x in o .: [:X,(o .: [:Y,Z:]):] ; ::_thesis: x in o .: [:(o .: [:X,Y:]),Z:] then consider y being set 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 = 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 set 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 = 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 x in o .: [:(o .: [:X,Y:]),Z:] by A1, A26, FUNCT_1:def_6; ::_thesis: verum end; theorem Th49: :: MONOID_1:49 for D being non empty set for o being BinOp of D st o is commutative holds o .:^2 is commutative proof let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds o .:^2 is commutative let o be BinOp of D; ::_thesis: ( o is commutative implies o .:^2 is commutative ) assume A1: o is commutative ; ::_thesis: o .:^2 is commutative let x, y be Subset of D; :: according to BINOP_1:def_2 ::_thesis: (o .:^2) . (x,y) = (o .:^2) . (y,x) thus (o .:^2) . (x,y) = o .: [:x,y:] by Th44 .= o .: [:y,x:] by A1, Th47 .= (o .:^2) . (y,x) by Th44 ; ::_thesis: verum end; theorem Th50: :: MONOID_1:50 for D being non empty set for o being BinOp of D st o is associative holds o .:^2 is associative proof let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds o .:^2 is associative let o be BinOp of D; ::_thesis: ( o is associative implies o .:^2 is associative ) assume A1: o is associative ; ::_thesis: o .:^2 is associative let x, y, z be Subset of D; :: according to BINOP_1:def_3 ::_thesis: (o .:^2) . (x,((o .:^2) . (y,z))) = (o .:^2) . (((o .:^2) . (x,y)),z) 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 ; ::_thesis: verum end; theorem Th51: :: MONOID_1:51 for X being set for D being non empty set for o being BinOp of D for a being Element of D st a is_a_unity_wrt o holds ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) proof let X be set ; ::_thesis: for D being non empty set for o being BinOp of D for a being Element of D st a is_a_unity_wrt o holds ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) let D be non empty set ; ::_thesis: for o being BinOp of D for a being Element of D st a is_a_unity_wrt o holds ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) let o be BinOp of D; ::_thesis: for a being Element of D st a is_a_unity_wrt o holds ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) let a be Element of D; ::_thesis: ( a is_a_unity_wrt o implies ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) ) assume A1: a is_a_unity_wrt o ; ::_thesis: ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) thus o .: [:{a},X:] c= D /\ X :: according to XBOOLE_0:def_10 ::_thesis: ( D /\ X c= o .: [:{a},X:] & o .: [:X,{a}:] = D /\ X ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:{a},X:] or x in D /\ X ) assume x in o .: [:{a},X:] ; ::_thesis: x in D /\ X then consider y being set 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 = 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 x in D /\ X by A5, A8, A7, XBOOLE_0:def_4; ::_thesis: verum end; A9: dom o = [:D,D:] by FUNCT_2:def_1; thus D /\ X c= o .: [:{a},X:] ::_thesis: o .: [:X,{a}:] = D /\ X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D /\ X or x in o .: [:{a},X:] ) A10: a in {a} by TARSKI:def_1; assume A11: x in D /\ X ; ::_thesis: x in o .: [:{a},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 x in o .: [:{a},X:] by A9, A12, FUNCT_1:def_6; ::_thesis: verum end; thus o .: [:X,{a}:] c= D /\ X :: according to XBOOLE_0:def_10 ::_thesis: D /\ X c= o .: [:X,{a}:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,{a}:] or x in D /\ X ) assume x in o .: [:X,{a}:] ; ::_thesis: x in D /\ X then consider y being set 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 = 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 x in D /\ X by A16, A19, A18, XBOOLE_0:def_4; ::_thesis: verum end; thus D /\ X c= o .: [:X,{a}:] ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D /\ X or x in o .: [:X,{a}:] ) A20: a in {a} by TARSKI:def_1; assume A21: x in D /\ X ; ::_thesis: x in o .: [:X,{a}:] 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 x in o .: [:X,{a}:] by A9, A22, FUNCT_1:def_6; ::_thesis: verum end; end; theorem Th52: :: MONOID_1:52 for D being non empty set for o being BinOp of D for a being Element of D st a is_a_unity_wrt o holds ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) proof let D be non empty set ; ::_thesis: for o being BinOp of D for a being Element of D st a is_a_unity_wrt o holds ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) let o be BinOp of D; ::_thesis: for a being Element of D st a is_a_unity_wrt o holds ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) let a be Element of D; ::_thesis: ( 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} ) ) assume A1: a is_a_unity_wrt o ; ::_thesis: ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) now__::_thesis:_for_x_being_Subset_of_D_holds_ (_(o_.:^2)_._({a},x)_=_x_&_(o_.:^2)_._(x,{a})_=_x_) let x be Subset of D; ::_thesis: ( (o .:^2) . ({a},x) = x & (o .:^2) . (x,{a}) = x ) thus (o .:^2) . ({a},x) = o .: [:{a},x:] by Th44 .= D /\ x by A1, Th51 .= x by XBOOLE_1:28 ; ::_thesis: (o .:^2) . (x,{a}) = x thus (o .:^2) . (x,{a}) = o .: [:x,{a}:] by Th44 .= D /\ x by A1, Th51 .= x by XBOOLE_1:28 ; ::_thesis: verum end; hence A2: {a} is_a_unity_wrt o .:^2 by BINOP_1:3; ::_thesis: ( o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) hence ex A being Subset of D st A is_a_unity_wrt o .:^2 ; :: according to SETWISEO:def_2 ::_thesis: the_unity_wrt (o .:^2) = {a} thus the_unity_wrt (o .:^2) = {a} by A2, BINOP_1:def_8; ::_thesis: verum end; theorem Th53: :: MONOID_1:53 for D being non empty set for o being BinOp of D st o is having_a_unity holds ( 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 let D be non empty set ; ::_thesis: for o being BinOp of D st o is having_a_unity holds ( 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)} ) let o be BinOp of D; ::_thesis: ( 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)} ) ) given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def_2 ::_thesis: ( 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)} ) a = the_unity_wrt o by A1, BINOP_1:def_8; hence ( 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)} ) by A1, Th52; ::_thesis: verum end; theorem Th54: :: MONOID_1:54 for D being non empty set for o being BinOp of D st o is uniquely-decomposable holds o .:^2 is uniquely-decomposable proof let D be non empty set ; ::_thesis: for o being BinOp of D st o is uniquely-decomposable holds o .:^2 is uniquely-decomposable let o be BinOp of D; ::_thesis: ( o is uniquely-decomposable implies o .:^2 is uniquely-decomposable ) assume that A1: o is having_a_unity and A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds ( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def_9 ::_thesis: o .:^2 is uniquely-decomposable thus o .:^2 is having_a_unity by A1, Th53; :: according to MONOID_0:def_9 ::_thesis: for b1, b2 being Element of bool D holds ( not (o .:^2) . (b1,b2) = the_unity_wrt (o .:^2) or ( b1 = b2 & b2 = the_unity_wrt (o .:^2) ) ) let A, B be Subset of D; ::_thesis: ( not (o .:^2) . (A,B) = the_unity_wrt (o .:^2) or ( A = B & B = the_unity_wrt (o .:^2) ) ) assume A3: (o .:^2) . (A,B) = the_unity_wrt (o .:^2) ; ::_thesis: ( A = B & B = the_unity_wrt (o .:^2) ) set a = the_unity_wrt o; A4: the_unity_wrt (o .:^2) = {(the_unity_wrt o)} by A1, Th53; set a1 = the Element of A; set 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:] <> {} by XBOOLE_0:def_7; then A5: [:A,B:] <> {} ; then A6: A <> {} by ZFMISC_1:90; A7: B <> {} by A5, ZFMISC_1:90; then reconsider a1 = the Element of A, a2 = the Element of B as Element of D by A6, TARSKI:def_3; A8: {a1} c= A by A6, ZFMISC_1:31; o . (a1,a2) in {(the_unity_wrt o)} by A3, A4, A6, A7, Th45; then A9: o . (a1,a2) = the_unity_wrt o by TARSKI:def_1; then A10: a2 = the_unity_wrt o by A2; A11: A c= {(the_unity_wrt o)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(the_unity_wrt o)} ) assume A12: x in A ; ::_thesis: x in {(the_unity_wrt o)} then reconsider c = x as Element of D ; o . (c,a2) in {(the_unity_wrt o)} by A3, A4, A7, A12, Th45; then o . (c,a2) = the_unity_wrt o by TARSKI:def_1; then c = a2 by A2; hence x in {(the_unity_wrt o)} by A10, TARSKI:def_1; ::_thesis: verum end; A13: B c= {(the_unity_wrt o)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in {(the_unity_wrt o)} ) assume A14: x in B ; ::_thesis: x in {(the_unity_wrt o)} then reconsider c = x as Element of D ; o . (a1,c) in {(the_unity_wrt o)} by A3, A4, A6, A14, Th45; then o . (a1,c) = the_unity_wrt o by TARSKI:def_1; then c = the_unity_wrt o by A2; hence x in {(the_unity_wrt o)} by TARSKI:def_1; ::_thesis: verum end; A15: a1 = a2 by A2, A9; {a2} c= B by A7, ZFMISC_1:31; then B = {(the_unity_wrt o)} by A10, A13, XBOOLE_0:def_10; hence ( A = B & B = the_unity_wrt (o .:^2) ) by A1, A15, A10, A8, A11, Th53, XBOOLE_0:def_10; ::_thesis: verum end; definition let G be non empty multMagma ; func bool G -> multMagma equals :Def9: :: MONOID_1:def 9 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 coherence ( ( G is unital implies multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) is multMagma ) & ( not G is unital implies multMagma(# (bool the carrier of G),( the multF of G .:^2) #) is multMagma ) ); consistency for b1 being multMagma holds verum; ; end; :: deftheorem Def9 defines bool MONOID_1:def_9_:_ for G being non empty multMagma holds ( ( G is unital implies bool G = multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) ) & ( not G is unital implies bool G = multMagma(# (bool the carrier of G),( the multF of G .:^2) #) ) ); registration let G be non empty multMagma ; cluster bool G -> non empty ; coherence not bool G is empty proof percases ( G is unital or not G is unital ) ; suppose G is unital ; ::_thesis: not bool G is empty then bool G = multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) by Def9; hence not the carrier of (bool G) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; suppose not G is unital ; ::_thesis: not bool G is empty then bool G = multMagma(# (bool the carrier of G),( the multF of G .:^2) #) by Def9; hence not the carrier of (bool G) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; end; end; definition let G be non empty unital multMagma ; :: original: bool redefine func bool G -> non empty strict well-unital multLoopStr ; coherence bool G is non empty strict well-unital multLoopStr proof set M = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #); H1(G) is having_a_unity by MONOID_0:def_10; then A1: {(the_unity_wrt H1(G))} is_a_unity_wrt H1(G) .:^2 by Th53; ( 1. multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) = {(the_unity_wrt H1(G))} & bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) ) by Def9; hence bool G is non empty strict well-unital multLoopStr by A1, MONOID_0:def_21; ::_thesis: verum end; end; theorem Th55: :: MONOID_1:55 for G being non empty multMagma holds ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) proof let G be non empty multMagma ; ::_thesis: ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) ( bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) or bool G = multMagma(# (bool the carrier of G),(H1(G) .:^2) #) ) by Def9; hence ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) ; ::_thesis: verum end; theorem :: MONOID_1:56 for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)} proof let G be non empty unital multMagma ; ::_thesis: 1. (bool G) = {(the_unity_wrt the multF of G)} bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) by Def9; hence 1. (bool G) = {(the_unity_wrt the multF of G)} ; ::_thesis: verum end; theorem :: MONOID_1:57 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 ; ::_thesis: ( ( 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 ) ) A1: ( H1( bool G) = H1(G) .:^2 & H3( bool G) = bool H3(G) ) by Th55; thus ( G is commutative implies bool G is commutative ) ::_thesis: ( ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) ) proof assume H1(G) is commutative ; :: according to MONOID_0:def_11 ::_thesis: bool G is commutative hence H1( bool G) is commutative by A1, Th49; :: according to MONOID_0:def_11 ::_thesis: verum end; thus ( G is associative implies bool G is associative ) ::_thesis: ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) proof assume H1(G) is associative ; :: according to MONOID_0:def_12 ::_thesis: bool G is associative hence H1( bool G) is associative by A1, Th50; :: according to MONOID_0:def_12 ::_thesis: verum end; assume H1(G) is uniquely-decomposable ; :: according to MONOID_0:def_20 ::_thesis: bool G is uniquely-decomposable hence H1( bool G) is uniquely-decomposable by A1, Th54; :: according to MONOID_0:def_20 ::_thesis: verum end;