:: by Grzegorz Bancerek

::

:: Received December 29, 1992

:: Copyright (c) 1992-2016 Association of Mizar Users

deffunc H

deffunc H

definition
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);

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 func f .. (x1,x2,x) -> Element of D;

coherence

f .. (x1,x2,x) is Element of D

end;
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 func f .. (x1,x2,x) -> Element of D;

coherence

f .. (x1,x2,x) is Element of D

proof 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 func f .: (g1,g2) -> Element of Funcs (A,D);

coherence

f .: (g1,g2) is Element of Funcs (A,D)

end;
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 func f .: (g1,g2) -> Element of Funcs (A,D);

coherence

f .: (g1,g2) is Element of Funcs (A,D)

proof 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;
let n be Element of NAT ;

let x be Element of A;

synonym n .--> x for A |-> n;

definition

let A be non empty set ;

let n be Element of NAT ;

let x be Element of A;

:: original: .-->

redefine func n .--> x -> FinSequence of A;

coherence

x .--> is FinSequence of A by FINSEQ_2:63;

end;
let n be Element of NAT ;

let x be Element of A;

:: original: .-->

redefine func n .--> x -> FinSequence of A;

coherence

x .--> is FinSequence of A by FINSEQ_2:63;

definition

let D be non empty set ;

let A be set ;

let d be Element of D;

:: original: -->

redefine func A --> d -> Element of Funcs (A,D);

coherence

A --> d is Element of Funcs (A,D)

end;
let A be set ;

let d be Element of D;

:: original: -->

redefine func A --> d -> Element of Funcs (A,D);

coherence

A --> d is Element of Funcs (A,D)

proof 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 func f [;] (d,g) -> Element of Funcs (A,D);

coherence

f [;] (d,g) is Element of Funcs (A,D)

end;
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 func f [;] (d,g) -> Element of Funcs (A,D);

coherence

f [;] (d,g) is Element of Funcs (A,D)

proof 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 func f [:] (g,d) -> Element of Funcs (A,D);

coherence

f [:] (g,d) is Element of Funcs (A,D)

end;
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 func f [:] (g,d) -> Element of Funcs (A,D);

coherence

f [:] (g,d) is Element of Funcs (A,D)

proof end;

definition

let D1, D2, D be non empty set ;

let f be Function of [:D1,D2:],D;

let A be set ;

ex b_{1} 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 b_{1} . (f1,f2) = f .: (f1,f2)

for b_{1}, b_{2} 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 b_{1} . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1)

for f2 being Element of Funcs (A,D2) holds b_{2} . (f1,f2) = f .: (f1,f2) ) holds

b_{1} = b_{2}

end;
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 for f1 being Element of Funcs (A,D1)

for f2 being Element of Funcs (A,D2) holds it . (f1,f2) = f .: (f1,f2);

ex b

for f1 being Element of Funcs (A,D1)

for f2 being Element of Funcs (A,D2) holds b

proof end;

uniqueness for b

for f2 being Element of Funcs (A,D2) holds b

for f2 being Element of Funcs (A,D2) holds b

b

proof 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 b_{6} being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) holds

( b_{6} = (f,D) .: A iff for f1 being Element of Funcs (A,D1)

for f2 being Element of Funcs (A,D2) holds b_{6} . (f1,f2) = f .: (f1,f2) );

for D1, D2, D being non empty set

for f being Function of [:D1,D2:],D

for A being set

for b

( b

for f2 being Element of Funcs (A,D2) holds b

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))

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 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)

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 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)))

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 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 )

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 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

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 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

for D being non empty set

for o being BinOp of D st o is commutative holds

(o,D) .: A is commutative

proof 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

for D being non empty set

for o being BinOp of D st o is associative holds

(o,D) .: A is associative

proof 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

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 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 )

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 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

for D being non empty set

for o being BinOp of D st o is idempotent holds

(o,D) .: A is idempotent

proof 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

for D being non empty set

for o being BinOp of D st o is invertible holds

(o,D) .: A is invertible

proof 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

for D being non empty set

for o being BinOp of D st o is cancelable holds

(o,D) .: A is cancelable

proof 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

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 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

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 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

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 end;

definition

let G be non empty multMagma ;

let A be set ;

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 b_{1} being multMagma holds verum;

;

end;
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 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) #);

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 b

;

:: 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) #) ) );

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
end;

deffunc H

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 )

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 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 )

for G being non empty multMagma holds

( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G )

proof end;

Lm1: for X being set

for G being non empty multMagma holds .: (G,X) is constituted-Functions

proof end;

registration
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 )

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 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 object st x in X holds

f . x = g . x ) holds

f = g

for G being non empty multMagma

for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds

f . x = g . x ) holds

f = g

proof 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 func f . a -> Element of G;

coherence

f . a is Element of G

end;
let A be non empty set ;

let f be Element of (.: (G,A));

let a be Element of A;

:: original: .

redefine func f . a -> Element of G;

coherence

f . a is Element of G

proof end;

registration

let G be non empty multMagma ;

let A be non empty set ;

let f be Element of (.: (G,A));

coherence

not rng f is empty

end;
let A be non empty set ;

let f be Element of (.: (G,A));

coherence

not rng f is empty

proof 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)

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 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

end;
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 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)

for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)

proof 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 ) )

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 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)

for G being non empty multMagma

for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

proof 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)

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 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

end;
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 end;

definition

let A be set ;

coherence

.: (<NAT,+,0>,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid;

;

end;
func MultiSet_over A -> strict commutative constituted-Functions cancelable uniquely-decomposable Monoid equals :: MONOID_1:def 4

.: (<NAT,+,0>,A);

correctness .: (<NAT,+,0>,A);

coherence

.: (<NAT,+,0>,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid;

;

:: deftheorem defines MultiSet_over MONOID_1:def 4 :

for A being set holds MultiSet_over A = .: (<NAT,+,0>,A);

for A being set holds MultiSet_over A = .: (<NAT,+,0>,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 )

( 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 end;

registration
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)

for m1, m2 being Multiset of D

for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)

proof 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;
:: original: chi

redefine func chi (Y,X) -> Multiset of X;

coherence

chi (Y,X) is Multiset of X by Th30;

definition

let X be set ;

let n be Element of NAT ;

:: original: -->

redefine func X --> n -> Multiset of X;

coherence

X --> n is Multiset of X

end;
let n be Element of NAT ;

:: original: -->

redefine func X --> n -> Multiset of X;

coherence

X --> n is Multiset of X

proof end;

definition
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);

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 ) )

for a, b being Element of A holds

( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

proof 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

for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds

m1 = m2

proof end;

definition

let A be set ;

ex b_{1} being non empty strict MonoidalSubStr of MultiSet_over A st

for f being Multiset of A holds

( f in the carrier of b_{1} iff f " (NAT \ {0}) is finite )

for b_{1}, b_{2} being non empty strict MonoidalSubStr of MultiSet_over A st ( for f being Multiset of A holds

( f in the carrier of b_{1} iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds

( f in the carrier of b_{2} iff f " (NAT \ {0}) is finite ) ) holds

b_{1} = b_{2}

end;
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 for f being Multiset of A holds

( f in the carrier of it iff f " (NAT \ {0}) is finite );

ex b

for f being Multiset of A holds

( f in the carrier of b

proof end;

uniqueness for b

( f in the carrier of b

( f in the carrier of b

b

proof end;

:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :

for A being set

for b_{2} being non empty strict MonoidalSubStr of MultiSet_over A holds

( b_{2} = finite-MultiSet_over A iff for f being Multiset of A holds

( f in the carrier of b_{2} iff f " (NAT \ {0}) is finite ) );

for A being set

for b

( b

( f in the carrier of b

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)

for a being Element of A holds chi a is Element of (finite-MultiSet_over A)

proof 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)}

for A being non empty set

for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)}

proof 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)

for A being non empty set

for p being FinSequence of A st x <> y holds

dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)

proof end;

definition

let A be non empty set ;

let p be FinSequence of A;

ex b_{1} being Multiset of A st

for a being Element of A holds b_{1} . a = card (dom ({a} |` p))

for b_{1}, b_{2} being Multiset of A st ( for a being Element of A holds b_{1} . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds b_{2} . a = card (dom ({a} |` p)) ) holds

b_{1} = b_{2}

end;
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 for a being Element of A holds it . a = card (dom ({a} |` p));

ex b

for a being Element of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines |. MONOID_1:def 7 :

for A being non empty set

for p being FinSequence of A

for b_{3} being Multiset of A holds

( b_{3} = |.p.| iff for a being Element of A holds b_{3} . a = card (dom ({a} |` p)) );

for A being non empty set

for p being FinSequence of A

for b

( b

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)

for a being Element of A

for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)

proof 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 ) )

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 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)

for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A)

proof 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.|

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 end;

definition

let D1, D2, D be non empty set ;

let f be Function of [:D1,D2:],D;

ex b_{1} being Function of [:(bool D1),(bool D2):],(bool D) st

for x being Element of [:(bool D1),(bool D2):] holds b_{1} . x = f .: [:(x `1),(x `2):]

for b_{1}, b_{2} being Function of [:(bool D1),(bool D2):],(bool D) st ( for x being Element of [:(bool D1),(bool D2):] holds b_{1} . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds b_{2} . x = f .: [:(x `1),(x `2):] ) holds

b_{1} = b_{2}

end;
let f be Function of [:D1,D2:],D;

func f .:^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 for x being Element of [:(bool D1),(bool D2):] holds it . x = f .: [:(x `1),(x `2):];

ex b

for x being Element of [:(bool D1),(bool D2):] holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of [:(bool D1),(bool D2):],(bool D) holds

( b_{5} = f .:^2 iff for x being Element of [:(bool D1),(bool D2):] holds b_{5} . x = f .: [:(x `1),(x `2):] );

for D1, D2, D being non empty set

for f being Function of [:D1,D2:],D

for b

( b

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:]

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 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)

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 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 ) }

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 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:]

for D being non empty set

for o being BinOp of D st o is commutative holds

o .: [:X,Y:] = o .: [:Y,X:]

proof 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:]):]

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 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 )

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 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} )

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 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)} )

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 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

for o being BinOp of D st o is uniquely-decomposable holds

o .:^2 is uniquely-decomposable

proof end;

definition

let G be non empty multMagma ;

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 b_{1} being multMagma holds verum;

;

end;
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 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) #);

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 b

;

:: 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) #) ) );

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) #) ) );

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

end;
:: original: bool

redefine func bool G -> non empty strict well-unital multLoopStr ;

coherence

bool G is non empty strict well-unital multLoopStr

proof 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 )

( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 )

proof 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 ) )

( ( 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 end;