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


begin

registration
let X be set ;
let f be Function of NAT,X;
let n be Nat;
clusterf | n ->  T-Sequence-like ;
correctness
coherence
f | n is T-Sequence-like ;
proofend;
end;

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

:: deftheorem Def1 defines IFXFinSequence ALGSTR_4:def_1_:_
 for X, x being set holds
( ( x is XFinSequence of implies IFXFinSequence (x,X) = x ) &amp; ( x is not XFinSequence of 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 ;
:: original:.
redefine funcf . c ->  Element of X;
correctness
coherence
f . c is Element of X;
proofend;
end;

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

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

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

scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2{ F1() ->  non empty set , F2( XFinSequence of ) ->  Element of F1(), F3() ->  Function of NAT,F1(), F4() ->  Function of NAT,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))
proofend;

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

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

:: deftheorem Def2 defines extends ALGSTR_4:def_2_:_
 for f, g being Function holds
( f extends g iff ( dom g c= dom f &amp; f tolerates g ) );

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

begin

definition
let M be multMagma ;
let R be Equivalence_Relation of M;
attrR is compatible  means :Def3: :: ALGSTR_4:def 3
 for v, v9, w, w9 being Element of M st v in Class (R,v9) &amp; 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) &amp; 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 ;
proofend;
end;

registration
let M be multMagma ;
cluster Relation-like the carrier of M -defined the carrier of M -valued total quasi_total V260() V265() 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 ;
proofend;
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) &amp; Class (R,w) = Class (R,w9) holds
Class (R,(v * w)) = Class (R,(v9 * w9)) )
proofend;

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) &amp; 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 ) &amp; ( 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) &amp; y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) &amp; ( 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 &amp; ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) &amp; y = Class (R,w) holds
b1 . (x,y) = Class (R,(v * w)) ) &amp; ( for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) &amp; y = Class (R,w) holds
b2 . (x,y) = Class (R,(v * w)) ) implies b1 = b2 ) &amp; ( M is empty &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) );
proofend;
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) &amp; y = Class (R,w) holds
b3 . (x,y) = Class (R,(v * w)) ) ) &amp; ( M is empty implies ( b3 = ClassOp R iff b3 = {} ) ) );

definition
let M be multMagma ;
let R be compatible Equivalence_Relation of M;
funcM ./. 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;
clusterM ./. R ->  strict ;
correctness
coherence
M ./. R is strict ;
;
end;

registration
let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
clusterM ./. 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)
proofend;
uniqueness
 for b1, b2 being Function of M,(M ./. R) st ( for v being Element of M holds b1 . v = Class (R,v) ) &amp; ( for v being Element of M holds b2 . v = Class (R,v) ) holds
b1 = b2
proofend;
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 ;
proofend;
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 ;
proofend;
end;

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

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 &amp; 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 &amp; r . i = [v,w] holds
v in Class (R,w)  }  is Equivalence_Relation of M;
proofend;
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 &amp; 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 &amp; r . i = [v,w] holds
v in Class (R,w) ) holds
equ_rel r c= R
proofend;

registration
let M be multMagma ;
let r be Relators of M;
cluster equ_rel r ->  compatible ;
coherence
 equ_rel r is compatible
proofend;
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 set holds
( [x,y] in it iff ( x in X &amp; y in X &amp; f . x = f . y ) );
existence
 ex b1 being Equivalence_Relation of X st
for x, y being set holds
( [x,y] in b1 iff ( x in X &amp; y in X &amp; f . x = f . y ) )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of X st ( for x, y being set holds
( [x,y] in b1 iff ( x in X &amp; y in X &amp; f . x = f . y ) ) ) &amp; ( for x, y being set holds
( [x,y] in b2 iff ( x in X &amp; y in X &amp; f . x = f . y ) ) ) holds
b1 = b2
proofend;
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 set holds
( [x,y] in b4 iff ( x in X &amp; y in X &amp; 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
proofend;

theorem Th5: :: ALGSTR_4:5
for N, M 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
proofend;

begin

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 &amp; 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 &amp; the multF of b1 = the multF of M || the carrier of b1 )
proofend;
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 &amp; 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
proofend;
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
proofend;
end;

theorem Th6: :: ALGSTR_4:6
for M being multMagma
for N, K being multSubmagma of M st N is multSubmagma of K &amp; K is multSubmagma of N holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of K, the multF of K #)
proofend;

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

definition
let M be multMagma ;
let A be Subset of M;
attrA is stable  means :Def10: :: ALGSTR_4:def 10
 for v, w being Element of M st v in A &amp; 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 &amp; 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 ;
proofend;
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
proofend;

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

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

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

theorem Th12: :: ALGSTR_4:12
for N, M 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
proofend;

theorem :: ALGSTR_4:13
for N, M being non empty multMagma
for f, g being Function of M,N st f is multiplicative &amp; g is multiplicative holds
{  v where v is Element of M : f . v = g . v  }  is stable Subset of M
proofend;

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

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 &amp; ( 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 &amp; ( for N being strict multSubmagma of M st A c= the carrier of N holds
b1 is multSubmagma of N ) )
proofend;
uniqueness
 for b1, b2 being strict multSubmagma of M st A c= the carrier of b1 &amp; ( for N being strict multSubmagma of M st A c= the carrier of N holds
b1 is multSubmagma of N ) &amp; A c= the carrier of b2 &amp; ( for N being strict multSubmagma of M st A c= the carrier of N holds
b2 is multSubmagma of N ) holds
b1 = b2
proofend;
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 &amp; ( 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 )
proofend;

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;

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

begin

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

:: deftheorem Def13 defines free_magma_seq ALGSTR_4:def_13_:_
 for X being set
for b2 being Function of NAT,(bool (the_universe_of (X \/ NAT))) holds
( b2 = free_magma_seq X iff ( b2 . 0 = {} &amp; b2 . 1 = X &amp; ( for n being Nat st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 &amp; ( for p being Nat st p >= 1 &amp; p <= n - 1 holds
fs . p = [:(b2 . p),(b2 . (n - p)):] ) &amp; 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 ;
proofend;
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}:]
proofend;

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

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 &amp; ( for p being Nat st p >= 1 &amp; p <= n - 1 holds
fs . p = [:(free_magma (X,p)),(free_magma (X,(n -' p))):] ) &amp; free_magma (X,n) = Union (disjoin fs) )
proofend;

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

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

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

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

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

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;
clusterw `2  ->  non zero natural for number ;
correctness
coherence
for b1 being number st b1 = w `2 holds
( not b1 is empty &amp; b1 is natural );
proofend;
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)}:]
proofend;

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

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

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 &amp; 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 ) &amp; ( 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 &amp; m = w `2 holds
b1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) &amp; ( 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 &amp; ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 &amp; m = w `2 holds
b1 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) &amp; ( for v, w being Element of free_magma_carrier X
for n, m being Nat st n = v `2 &amp; m = w `2 holds
b2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b1 = b2 ) &amp; ( X is empty &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) );
proofend;
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 &amp; m = w `2 holds
b2 . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) ) &amp; ( X is empty implies ( b2 = free_magma_mult X iff b2 = {} ) ) );

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);
clusterw `2  ->  non zero natural for number ;
correctness
coherence
for b1 being number st b1 = w `2 holds
( not b1 is empty &amp; 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
proofend;

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 ) &amp; ( 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 ) &amp; ( 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  }
proofend;

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))]
proofend;

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)] &amp; length v >= 1 )
proofend;

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

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 &amp; length w1 < length w &amp; length w2 < length w )
proofend;

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 &amp; v2 = w2 )
proofend;

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 ) &amp; ( 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] ) &amp; ( 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 &amp; ( for x being set st x in dom b1 holds
b1 . x = [x,n] ) &amp; ( for x being set st x in dom b2 holds
b2 . x = [x,n] ) implies b1 = b2 ) &amp; ( not n > 0 &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) );
proofend;
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] ) ) &amp; ( 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
proofend;

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 &amp; ( for x being set st x in X holds
(canon_image (X,1)) . x = [x,1] ) )
proofend;

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

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

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

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 &amp; 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 &amp; z = (x `1) `2 holds
b1 . x = (f . y) * (g . z)
proofend;
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 &amp; z = (x `1) `2 holds
b1 . x = (f . y) * (g . z) ) &amp; ( 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 &amp; z = (x `1) `2 holds
b2 . x = (f . y) * (g . z) ) holds
b1 = b2
proofend;
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 &amp; z = (x `1) `2 holds
b7 . x = (f . y) * (g . z) );

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 &amp; h extends f * ((canon_image (X,1)) ") )
proofend;

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 &amp; h extends f * ((canon_image (X,1)) ") &amp; g is multiplicative &amp; g extends f * ((canon_image (X,1)) ") holds
h = g
proofend;

theorem Th41: :: ALGSTR_4:41
for N, M 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 &amp; the carrier of H = rng f &amp; R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) &amp; g is bijective &amp; g is multiplicative )
proofend;

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

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 &amp; g is multiplicative )
proofend;

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 &amp; 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 &amp; b1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") )
proofend;
uniqueness
 for b1, b2 being Function of (free_magma X),(free_magma Y) st b1 is multiplicative &amp; b1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") &amp; b2 is multiplicative &amp; b2 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") holds
b1 = b2
proofend;
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 &amp; 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)
proofend;

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

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

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

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