:: Free Magmas
:: by Marco Riccardi
::
:: Received October 20, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users


registration
let X be set ;
let f be sequence of X;
let n be Nat;
cluster f | n -> Sequence-like ;
correctness
coherence
f | n is Sequence-like
;
proof end;
end;

definition
let X, x be set ;
func IFXFinSequence (x,X) -> XFinSequence of X equals :Def1: :: ALGSTR_4:def 1
x if x is XFinSequence of X
otherwise <%> X;
correctness
coherence
( ( x is XFinSequence of X implies x is XFinSequence of X ) & ( x is not XFinSequence of X implies <%> X is XFinSequence of X ) )
;
consistency
for b1 being XFinSequence of X holds verum
;
;
end;

:: deftheorem Def1 defines IFXFinSequence ALGSTR_4:def 1 :
for X, x being set holds
( ( x is XFinSequence of X implies IFXFinSequence (x,X) = x ) & ( x is not XFinSequence of X implies IFXFinSequence (x,X) = <%> X ) );

definition
let X be non empty set ;
let f be Function of (X ^omega),X;
let c be XFinSequence of X;
:: original: .
redefine func f . c -> Element of X;
correctness
coherence
f . c is Element of X
;
proof end;
end;

theorem Th1: :: ALGSTR_4:1
for X, Y, Z being set st Y c= the_universe_of X & Z c= the_universe_of X holds
[:Y,Z:] c= the_universe_of X
proof end;

scheme :: ALGSTR_4:sch 1
FuncRecursiveUniq{ F1( set ) -> set , F2() -> Function, F3() -> Function } :
F2() = F3()
provided
A1: ( dom F2() = NAT & ( for n being Nat holds F2() . n = F1((F2() | n)) ) ) and
A2: ( dom F3() = NAT & ( for n being Nat holds F3() . n = F1((F3() | n)) ) )
proof end;

scheme :: ALGSTR_4:sch 2
FuncRecursiveExist{ F1( set ) -> set } :
ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = F1((f | n)) ) )
proof end;

scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2{ F1() -> non empty set , F2( XFinSequence of F1()) -> Element of F1(), F3() -> sequence of F1(), F4() -> sequence of F1() } :
F3() = F4()
provided
A1: for n being Nat holds F3() . n = F2((F3() | n)) and
A2: for n being Nat holds F4() . n = F2((F4() | n))
proof end;

scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2{ F1() -> non empty set , F2( XFinSequence of F1()) -> Element of F1() } :
ex f being sequence of F1() st
for n being Nat holds f . n = F2((f | n))
proof end;

definition
let f, g be Function;
pred f extends g means :: ALGSTR_4:def 2
( dom g c= dom f & f tolerates g );
end;

:: deftheorem defines extends ALGSTR_4:def 2 :
for f, g being Function holds
( f extends g iff ( dom g c= dom f & f tolerates g ) );

registration
cluster empty for multMagma ;
existence
ex b1 being multMagma st b1 is empty
proof end;
end;

:: Ch I ?1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma ;
let R be Equivalence_Relation of M;
attr R is compatible means :Def3: :: ALGSTR_4:def 3
for v, v9, w, w9 being Element of M st v in Class (R,v9) & w in Class (R,w9) holds
v * w in Class (R,(v9 * w9));
end;

:: deftheorem Def3 defines compatible ALGSTR_4:def 3 :
for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff for v, v9, w, w9 being Element of M st v in Class (R,v9) & w in Class (R,w9) holds
v * w in Class (R,(v9 * w9)) );

registration
let M be multMagma ;
cluster nabla the carrier of M -> compatible ;
correctness
coherence
nabla the carrier of M is compatible
;
proof end;
end;

registration
let M be multMagma ;
cluster Relation-like the carrier of M -defined the carrier of M -valued total quasi_total V65() V70() compatible for Element of bool [: the carrier of M, the carrier of M:];
correctness
existence
ex b1 being Equivalence_Relation of M st b1 is compatible
;
proof end;
end;

theorem Th2: :: ALGSTR_4:2
for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff for v, v9, w, w9 being Element of M st Class (R,v) = Class (R,v9) & Class (R,w) = Class (R,w9) holds
Class (R,(v * w)) = Class (R,(v9 * w9)) )
proof end;

definition
let M be multMagma ;
let R be compatible Equivalence_Relation of M;
func ClassOp R -> BinOp of (Class R) means :Def4: :: ALGSTR_4:def 4
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
it . (x,y) = Class (R,(v * w)) if not M is empty
otherwise it = {} ;
correctness
consistency
for b1 being BinOp of (Class R) holds verum
;
existence
( ( for b1 being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b1 being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( M is empty implies ex b1 being BinOp of (Class R) st b1 = {} ) )
;
uniqueness
for b1, b2 being BinOp of (Class R) holds
( ( not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b2 . (x,y) = Class (R,(v * w)) ) implies b1 = b2 ) & ( M is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
;
proof end;
end;

:: deftheorem Def4 defines ClassOp ALGSTR_4:def 4 :
for M being multMagma
for R being compatible Equivalence_Relation of M
for b3 being BinOp of (Class R) holds
( ( not M is empty implies ( b3 = ClassOp R iff for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b3 . (x,y) = Class (R,(v * w)) ) ) & ( M is empty implies ( b3 = ClassOp R iff b3 = {} ) ) );

:: Ch I ?1.6 Def.11 Algebra I Bourbaki
definition
let M be multMagma ;
let R be compatible Equivalence_Relation of M;
func M ./. R -> multMagma equals :: ALGSTR_4:def 5
multMagma(# (Class R),(ClassOp R) #);
correctness
coherence
multMagma(# (Class R),(ClassOp R) #) is multMagma
;
;
end;

:: deftheorem defines ./. ALGSTR_4:def 5 :
for M being multMagma
for R being compatible Equivalence_Relation of M holds M ./. R = multMagma(# (Class R),(ClassOp R) #);

registration
let M be multMagma ;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> strict ;
correctness
coherence
M ./. R is strict
;
;
end;

registration
let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> non empty ;
correctness
coherence
not M ./. R is empty
;
;
end;

definition
let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
func nat_hom R -> Function of M,(M ./. R) means :Def6: :: ALGSTR_4:def 6
for v being Element of M holds it . v = Class (R,v);
existence
ex b1 being Function of M,(M ./. R) st
for v being Element of M holds b1 . v = Class (R,v)
proof end;
uniqueness
for b1, b2 being Function of M,(M ./. R) st ( for v being Element of M holds b1 . v = Class (R,v) ) & ( for v being Element of M holds b2 . v = Class (R,v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines nat_hom ALGSTR_4:def 6 :
for M being non empty multMagma
for R being compatible Equivalence_Relation of M
for b3 being Function of M,(M ./. R) holds
( b3 = nat_hom R iff for v being Element of M holds b3 . v = Class (R,v) );

registration
let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> multiplicative ;
correctness
coherence
nat_hom R is multiplicative
;
proof end;
end;

registration
let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> onto ;
correctness
coherence
nat_hom R is onto
;
proof end;
end;

definition
let M be multMagma ;
mode Relators of M is [: the carrier of M, the carrier of M:] -valued Function;
end;

:: Ch I ?1.6 Algebra I Bourbaki
definition
let M be multMagma ;
let r be Relators of M;
func equ_rel r -> Equivalence_Relation of M equals :: ALGSTR_4:def 7
meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w)
}
;
correctness
coherence
meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w)
}
is Equivalence_Relation of M
;
proof end;
end;

:: deftheorem defines equ_rel ALGSTR_4:def 7 :
for M being multMagma
for r being Relators of M holds equ_rel r = meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w)
}
;

theorem Th3: :: ALGSTR_4:3
for M being multMagma
for r being Relators of M
for R being compatible Equivalence_Relation of M st ( for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w) ) holds
equ_rel r c= R
proof end;

registration
let M be multMagma ;
let r be Relators of M;
cluster equ_rel r -> compatible ;
coherence
equ_rel r is compatible
proof end;
end;

definition
let X, Y be set ;
let f be Function of X,Y;
func equ_kernel f -> Equivalence_Relation of X means :Def8: :: ALGSTR_4:def 8
for x, y being object holds
( [x,y] in it iff ( x in X & y in X & f . x = f . y ) );
existence
ex b1 being Equivalence_Relation of X st
for x, y being object holds
( [x,y] in b1 iff ( x in X & y in X & f . x = f . y ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of X st ( for x, y being object holds
( [x,y] in b1 iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ( x in X & y in X & f . x = f . y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines equ_kernel ALGSTR_4:def 8 :
for X, Y being set
for f being Function of X,Y
for b4 being Equivalence_Relation of X holds
( b4 = equ_kernel f iff for x, y being object holds
( [x,y] in b4 iff ( x in X & y in X & f . x = f . y ) ) );

theorem Th4: :: ALGSTR_4:4
for M, N being non empty multMagma
for f being Function of M,N st f is multiplicative holds
equ_kernel f is compatible
proof end;

theorem Th5: :: ALGSTR_4:5
for M, N being non empty multMagma
for f being Function of M,N st f is multiplicative holds
ex r being Relators of M st equ_kernel f = equ_rel r
proof end;

definition
let M be multMagma ;
mode multSubmagma of M -> multMagma means :Def9: :: ALGSTR_4:def 9
( the carrier of it c= the carrier of M & the multF of it = the multF of M || the carrier of it );
existence
ex b1 being multMagma st
( the carrier of b1 c= the carrier of M & the multF of b1 = the multF of M || the carrier of b1 )
proof end;
end;

:: deftheorem Def9 defines multSubmagma ALGSTR_4:def 9 :
for M, b2 being multMagma holds
( b2 is multSubmagma of M iff ( the carrier of b2 c= the carrier of M & the multF of b2 = the multF of M || the carrier of b2 ) );

registration
let M be multMagma ;
cluster strict for multSubmagma of M;
existence
ex b1 being multSubmagma of M st b1 is strict
proof end;
end;

registration
let M be non empty multMagma ;
cluster non empty for multSubmagma of M;
existence
not for b1 being multSubmagma of M holds b1 is empty
proof end;
end;

:: like GROUP_2:64
theorem Th6: :: ALGSTR_4:6
for M being multMagma
for N, K being multSubmagma of M st N is multSubmagma of K & K is multSubmagma of N holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #)
proof end;

theorem Th7: :: ALGSTR_4:7
for M being multMagma
for N being multSubmagma of M st the carrier of N = the carrier of M holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of M, the multF of M #)
proof end;

:: Ch I ?1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma ;
let A be Subset of M;
attr A is stable means :Def10: :: ALGSTR_4:def 10
for v, w being Element of M st v in A & w in A holds
v * w in A;
end;

:: deftheorem Def10 defines stable ALGSTR_4:def 10 :
for M being multMagma
for A being Subset of M holds
( A is stable iff for v, w being Element of M st v in A & w in A holds
v * w in A );

registration
let M be multMagma ;
cluster stable for Element of bool the carrier of M;
correctness
existence
ex b1 being Subset of M st b1 is stable
;
proof end;
end;

theorem Th8: :: ALGSTR_4:8
for M being multMagma
for N being multSubmagma of M holds the carrier of N is stable Subset of M
proof end;

registration
let M be multMagma ;
let N be multSubmagma of M;
cluster the carrier of N -> stable for Subset of M;
correctness
coherence
for b1 being Subset of M st b1 = the carrier of N holds
b1 is stable
;
by Th8;
end;

theorem Th9: :: ALGSTR_4:9
for M being multMagma
for F being Function st ( for i being set st i in dom F holds
F . i is stable Subset of M ) holds
meet F is stable Subset of M
proof end;

theorem :: ALGSTR_4:10
for M being non empty multMagma
for A being Subset of M holds
( A is stable iff A * A c= A )
proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th11: :: ALGSTR_4:11
for M, N being non empty multMagma
for f being Function of M,N
for X being stable Subset of M st f is multiplicative holds
f .: X is stable Subset of N
proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th12: :: ALGSTR_4:12
for M, N being non empty multMagma
for f being Function of M,N
for Y being stable Subset of N st f is multiplicative holds
f " Y is stable Subset of M
proof end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem :: ALGSTR_4:13
for M, N being non empty multMagma
for f, g being Function of M,N st f is multiplicative & g is multiplicative holds
{ v where v is Element of M : f . v = g . v } is stable Subset of M
proof end;

:: Ch I ?1.4 Def.6 Algebra I Bourbaki
definition
let M be multMagma ;
let A be stable Subset of M;
func the_mult_induced_by A -> BinOp of A equals :: ALGSTR_4:def 11
the multF of M || A;
correctness
coherence
the multF of M || A is BinOp of A
;
proof end;
end;

:: deftheorem defines the_mult_induced_by ALGSTR_4:def 11 :
for M being multMagma
for A being stable Subset of M holds the_mult_induced_by A = the multF of M || A;

:: like GROUP_4:def 5
definition
let M be multMagma ;
let A be Subset of M;
func the_submagma_generated_by A -> strict multSubmagma of M means :Def12: :: ALGSTR_4:def 12
( A c= the carrier of it & ( for N being strict multSubmagma of M st A c= the carrier of N holds
it is multSubmagma of N ) );
existence
ex b1 being strict multSubmagma of M st
( A c= the carrier of b1 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b1 is multSubmagma of N ) )
proof end;
uniqueness
for b1, b2 being strict multSubmagma of M st A c= the carrier of b1 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b1 is multSubmagma of N ) & A c= the carrier of b2 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b2 is multSubmagma of N ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines the_submagma_generated_by ALGSTR_4:def 12 :
for M being multMagma
for A being Subset of M
for b3 being strict multSubmagma of M holds
( b3 = the_submagma_generated_by A iff ( A c= the carrier of b3 & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b3 is multSubmagma of N ) ) );

theorem Th14: :: ALGSTR_4:14
for M being multMagma
for A being Subset of M holds
( A is empty iff the_submagma_generated_by A is empty )
proof end;

registration
let M be multMagma ;
let A be empty Subset of M;
cluster the_submagma_generated_by A -> empty strict ;
correctness
coherence
the_submagma_generated_by A is empty
;
by Th14;
end;

:: Ch I ?1.4 Pro.1 Algebra I Bourbaki
theorem Th15: :: ALGSTR_4:15
for M, N being non empty multMagma
for f being Function of M,N
for X being Subset of M st f is multiplicative holds
f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))
proof end;

:: Ch I ?7.1 Algebra I Bourbaki
definition
let X be set ;
defpred S1[ object , object ] means for fs being XFinSequence of bool (the_universe_of (X \/ NAT)) st $1 = fs holds
( ( dom fs = 0 implies $2 = {} ) & ( dom fs = 1 implies $2 = X ) & ( for n being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):] ) & $2 = Union (disjoin fs1) ) ) );
A1: for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
ex u being object st S1[e,u]
proof end;
consider F being Function such that
A10: ( dom F = (bool (the_universe_of (X \/ NAT))) ^omega & ( for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
S1[e,F . e] ) ) from CLASSES1:sch 1(A1);
A11: for e being object st e in (bool (the_universe_of (X \/ NAT))) ^omega holds
F . e in bool (the_universe_of (X \/ NAT))
proof end;
func free_magma_seq X -> sequence of (bool (the_universe_of (X \/ NAT))) means :Def13: :: ALGSTR_4:def 13
( it . 0 = {} & it . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(it . p),(it . (n - p)):] ) & it . n = Union (disjoin fs) ) ) );
existence
ex b1 being sequence of (bool (the_universe_of (X \/ NAT))) st
( b1 . 0 = {} & b1 . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(b1 . p),(b1 . (n - p)):] ) & b1 . n = Union (disjoin fs) ) ) )
proof end;
uniqueness
for b1, b2 being sequence of (bool (the_universe_of (X \/ NAT))) st b1 . 0 = {} & b1 . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(b1 . p),(b1 . (n - p)):] ) & b1 . n = Union (disjoin fs) ) ) & b2 . 0 = {} & b2 . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(b2 . p),(b2 . (n - p)):] ) & b2 . n = Union (disjoin fs) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines free_magma_seq ALGSTR_4:def 13 :
for X being set
for b2 being sequence of (bool (the_universe_of (X \/ NAT))) holds
( b2 = free_magma_seq X iff ( b2 . 0 = {} & b2 . 1 = X & ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(b2 . p),(b2 . (n - p)):] ) & b2 . n = Union (disjoin fs) ) ) ) );

definition
let X be set ;
let n be Nat;
func free_magma (X,n) -> set equals :: ALGSTR_4:def 14
(free_magma_seq X) . n;
correctness
coherence
(free_magma_seq X) . n is set
;
;
end;

:: deftheorem defines free_magma ALGSTR_4:def 14 :
for X being set
for n being Nat holds free_magma (X,n) = (free_magma_seq X) . n;

registration
let X be non empty set ;
let n be non zero Nat;
cluster free_magma (X,n) -> non empty ;
correctness
coherence
not free_magma (X,n) is empty
;
proof end;
end;

theorem :: ALGSTR_4:16
for X being set holds free_magma (X,0) = {} by Def13;

theorem :: ALGSTR_4:17
for X being set holds free_magma (X,1) = X by Def13;

theorem Th18: :: ALGSTR_4:18
for X being set holds free_magma (X,2) = [:[:X,X:],{1}:]
proof end;

theorem :: ALGSTR_4:19
for X being set holds free_magma (X,3) = [:[:X,[:[:X,X:],{1}:]:],{1}:] \/ [:[:[:[:X,X:],{1}:],X:],{2}:]
proof end;

theorem Th20: :: ALGSTR_4:20
for X being set
for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma (X,p)),(free_magma (X,(n -' p))):] ) & free_magma (X,n) = Union (disjoin fs) )
proof end;

theorem Th21: :: ALGSTR_4:21
for X, x being set
for n being Nat st n >= 2 & x in free_magma (X,n) holds
ex p, m being Nat st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1) `1 in free_magma (X,p) & (x `1) `2 in free_magma (X,m) & n = p + m & x in [:[:(free_magma (X,p)),(free_magma (X,m)):],{p}:] )
proof end;

theorem Th22: :: ALGSTR_4:22
for X, x, y being set
for n, m being Nat st x in free_magma (X,n) & y in free_magma (X,m) holds
[[x,y],n] in free_magma (X,(n + m))
proof end;

theorem Th23: :: ALGSTR_4:23
for X, Y being set
for n being Nat st X c= Y holds
free_magma (X,n) c= free_magma (Y,n)
proof end;

definition
let X be set ;
func free_magma_carrier X -> set equals :: ALGSTR_4:def 15
Union (disjoin ((free_magma_seq X) | NATPLUS));
correctness
coherence
Union (disjoin ((free_magma_seq X) | NATPLUS)) is set
;
;
end;

:: deftheorem defines free_magma_carrier ALGSTR_4:def 15 :
for X being set holds free_magma_carrier X = Union (disjoin ((free_magma_seq X) | NATPLUS));

Lm1: for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X

proof end;

theorem Th24: :: ALGSTR_4:24
for X being set holds
( X = {} iff free_magma_carrier X = {} )
proof end;

registration
let X be empty set ;
cluster free_magma_carrier X -> empty ;
correctness
coherence
free_magma_carrier X is empty
;
by Th24;
end;

registration
let X be non empty set ;
cluster free_magma_carrier X -> non empty ;
correctness
coherence
not free_magma_carrier X is empty
;
by Th24;
let w be Element of free_magma_carrier X;
cluster w `2 -> natural non zero for number ;
correctness
coherence
for b1 being number st b1 = w `2 holds
( not b1 is zero & b1 is natural )
;
proof end;
end;

theorem Th25: :: ALGSTR_4:25
for X being non empty set
for w being Element of free_magma_carrier X holds w in [:(free_magma (X,(w `2))),{(w `2)}:]
proof end;

theorem Th26: :: ALGSTR_4:26
for X being non empty set
for v, w being Element of free_magma_carrier X holds [[[(v `1),(w `1)],(v `2)],((v `2) + (w `2))] is Element of free_magma_carrier X
proof end;

theorem Th27: :: ALGSTR_4:27
for X, Y being set st X c= Y holds
free_magma_carrier X c= free_magma_carrier Y
proof end;

theorem :: ALGSTR_4:28
for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X by Lm1;

definition
let X be set ;
func free_magma_mult X -> BinOp of (free_magma_carrier X) means :Def16: :: ALGSTR_4:def 16
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
it . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] if not X is empty
otherwise it = {} ;
correctness
consistency
for b1 being BinOp of (free_magma_carrier X) holds verum
;
existence
( ( for b1 being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b1 being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b1 being BinOp of (free_magma_carrier X) st b1 = {} ) )
;
uniqueness
for b1, b2 being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b1 = b2 ) & ( X is empty & b1 = {} & b2 = {} implies b1 = b2 ) )
;
proof end;
end;

:: deftheorem Def16 defines free_magma_mult ALGSTR_4:def 16 :
for X being set
for b2 being BinOp of (free_magma_carrier X) holds
( ( not X is empty implies ( b2 = free_magma_mult X iff for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 & m = w `2 holds
b2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) ) & ( X is empty implies ( b2 = free_magma_mult X iff b2 = {} ) ) );

:: Ch I ?7.1 Algebra I Bourbaki
definition
let X be set ;
func free_magma X -> multMagma equals :: ALGSTR_4:def 17
multMagma(# (free_magma_carrier X),(free_magma_mult X) #);
correctness
coherence
multMagma(# (free_magma_carrier X),(free_magma_mult X) #) is multMagma
;
;
end;

:: deftheorem defines free_magma ALGSTR_4:def 17 :
for X being set holds free_magma X = multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

registration
let X be set ;
cluster free_magma X -> strict ;
correctness
coherence
free_magma X is strict
;
;
end;

registration
let X be empty set ;
cluster free_magma X -> empty ;
correctness
coherence
free_magma X is empty
;
;
end;

registration
let X be non empty set ;
cluster free_magma X -> non empty ;
correctness
coherence
not free_magma X is empty
;
;
let w be Element of (free_magma X);
cluster w `2 -> natural non zero for number ;
correctness
coherence
for b1 being number st b1 = w `2 holds
( not b1 is zero & b1 is natural )
;
;
end;

theorem :: ALGSTR_4:29
for X being set
for S being Subset of X holds free_magma S is multSubmagma of free_magma X
proof end;

definition
let X be set ;
let w be Element of (free_magma X);
func length w -> Nat equals :Def18: :: ALGSTR_4:def 18
w `2 if not X is empty
otherwise 0 ;
correctness
coherence
( ( not X is empty implies w `2 is Nat ) & ( X is empty implies 0 is Nat ) )
;
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def18 defines length ALGSTR_4:def 18 :
for X being set
for w being Element of (free_magma X) holds
( ( not X is empty implies length w = w `2 ) & ( X is empty implies length w = 0 ) );

theorem Th30: :: ALGSTR_4:30
for X being set holds X = { (w `1) where w is Element of (free_magma X) : length w = 1 }
proof end;

theorem Th31: :: ALGSTR_4:31
for X being set
for v, w being Element of (free_magma X) st not X is empty holds
v * w = [[[(v `1),(w `1)],(v `2)],((length v) + (length w))]
proof end;

theorem Th32: :: ALGSTR_4:32
for X being set
for v being Element of (free_magma X) st not X is empty holds
( v = [(v `1),(v `2)] & length v >= 1 )
proof end;

theorem :: ALGSTR_4:33
for X being set
for v, w being Element of (free_magma X) holds length (v * w) = (length v) + (length w)
proof end;

theorem Th34: :: ALGSTR_4:34
for X being set
for w being Element of (free_magma X) st length w >= 2 holds
ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )
proof end;

theorem :: ALGSTR_4:35
for X being set
for v1, v2, w1, w2 being Element of (free_magma X) st v1 * v2 = w1 * w2 holds
( v1 = w1 & v2 = w2 )
proof end;

definition
let X be set ;
let n be Nat;
func canon_image (X,n) -> Function of (free_magma (X,n)),(free_magma X) means :Def19: :: ALGSTR_4:def 19
for x being set st x in dom it holds
it . x = [x,n] if n > 0
otherwise it = {} ;
correctness
consistency
for b1 being Function of (free_magma (X,n)),(free_magma X) holds verum
;
existence
( ( for b1 being Function of (free_magma (X,n)),(free_magma X) holds verum ) & ( n > 0 implies ex b1 being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( not n > 0 implies ex b1 being Function of (free_magma (X,n)),(free_magma X) st b1 = {} ) )
;
uniqueness
for b1, b2 being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( for x being set st x in dom b2 holds
b2 . x = [x,n] ) implies b1 = b2 ) & ( not n > 0 & b1 = {} & b2 = {} implies b1 = b2 ) )
;
proof end;
end;

:: deftheorem Def19 defines canon_image ALGSTR_4:def 19 :
for X being set
for n being Nat
for b3 being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 implies ( b3 = canon_image (X,n) iff for x being set st x in dom b3 holds
b3 . x = [x,n] ) ) & ( not n > 0 implies ( b3 = canon_image (X,n) iff b3 = {} ) ) );

Lm2: for X being set
for n being Nat holds canon_image (X,n) is one-to-one

proof end;

registration
let X be set ;
let n be Nat;
cluster canon_image (X,n) -> one-to-one ;
correctness
coherence
canon_image (X,n) is one-to-one
;
by Lm2;
end;

Lm3: for X being non empty set holds
( dom (canon_image (X,1)) = X & ( for x being set st x in X holds
(canon_image (X,1)) . x = [x,1] ) )

proof end;

theorem Th36: :: ALGSTR_4:36
for X being non empty set
for A being Subset of (free_magma X) st A = (canon_image (X,1)) .: X holds
free_magma X = the_submagma_generated_by A
proof end;

theorem :: ALGSTR_4:37
for X being non empty set
for R being compatible Equivalence_Relation of (free_magma X) holds (free_magma X) ./. R = the_submagma_generated_by ((nat_hom R) .: ((canon_image (X,1)) .: X))
proof end;

theorem Th38: :: ALGSTR_4:38
for X, Y being non empty set
for f being Function of X,Y holds (canon_image (Y,1)) * f is Function of X,(free_magma Y)
proof end;

definition
let X be non empty set ;
let M be non empty multMagma ;
let n, m be non zero Nat;
let f be Function of (free_magma (X,n)),M;
let g be Function of (free_magma (X,m)),M;
func [:f,g:] -> Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M means :Def20: :: ALGSTR_4:def 20
for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
it . x = (f . y) * (g . z);
existence
ex b1 being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M st
for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b1 . x = (f . y) * (g . z)
proof end;
uniqueness
for b1, b2 being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M st ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b1 . x = (f . y) * (g . z) ) & ( for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b2 . x = (f . y) * (g . z) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines [: ALGSTR_4:def 20 :
for X being non empty set
for M being non empty multMagma
for n, m being non zero Nat
for f being Function of (free_magma (X,n)),M
for g being Function of (free_magma (X,m)),M
for b7 being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M holds
( b7 = [:f,g:] iff for x being Element of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:]
for y being Element of free_magma (X,n)
for z being Element of free_magma (X,m) st y = (x `1) `1 & z = (x `1) `2 holds
b7 . x = (f . y) * (g . z) );

:: Ch I ?7.1 Pro.1 Algebra I Bourbaki
theorem Th39: :: ALGSTR_4:39
for X being non empty set
for M being non empty multMagma
for f being Function of X,M ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image (X,1)) ") )
proof end;

theorem Th40: :: ALGSTR_4:40
for X being non empty set
for M being non empty multMagma
for f being Function of X,M
for h, g being Function of (free_magma X),M st h is multiplicative & h extends f * ((canon_image (X,1)) ") & g is multiplicative & g extends f * ((canon_image (X,1)) ") holds
h = g
proof end;

theorem Th41: :: ALGSTR_4:41
for M, N being non empty multMagma
for f being Function of M,N
for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )
proof end;

theorem :: ALGSTR_4:42
for M, N being non empty multMagma
for R being compatible Equivalence_Relation of M
for g1, g2 being Function of (M ./. R),N st g1 * (nat_hom R) = g2 * (nat_hom R) holds
g1 = g2
proof end;

theorem :: ALGSTR_4:43
for M being non empty multMagma ex X being non empty set ex r being Relators of (free_magma X) ex g being Function of ((free_magma X) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )
proof end;

definition
let X, Y be non empty set ;
let f be Function of X,Y;
func free_magmaF f -> Function of (free_magma X),(free_magma Y) means :Def21: :: ALGSTR_4:def 21
( it is multiplicative & it extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") );
existence
ex b1 being Function of (free_magma X),(free_magma Y) st
( b1 is multiplicative & b1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") )
proof end;
uniqueness
for b1, b2 being Function of (free_magma X),(free_magma Y) st b1 is multiplicative & b1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") & b2 is multiplicative & b2 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines free_magmaF ALGSTR_4:def 21 :
for X, Y being non empty set
for f being Function of X,Y
for b4 being Function of (free_magma X),(free_magma Y) holds
( b4 = free_magmaF f iff ( b4 is multiplicative & b4 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") ) );

registration
let X, Y be non empty set ;
let f be Function of X,Y;
cluster free_magmaF f -> multiplicative ;
coherence
free_magmaF f is multiplicative
by Def21;
end;

theorem Th44: :: ALGSTR_4:44
for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z holds free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)
proof end;

theorem Th45: :: ALGSTR_4:45
for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g
proof end;

theorem Th46: :: ALGSTR_4:46
for X, Y being non empty set
for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))
proof end;

:: Ch I ?7.1 Pro.2 Algebra I Bourbaki
theorem :: ALGSTR_4:47
for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
free_magmaF f is one-to-one
proof end;

:: Ch I ?7.1 Pro.2 Algebra I Bourbaki
theorem :: ALGSTR_4:48
for X, Y being non empty set
for f being Function of X,Y st f is onto holds
free_magmaF f is onto
proof end;