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

correctness

coherence

f | n is Sequence-like ;

end;
let f be sequence of X;

let n be Nat;

correctness

coherence

f | n is Sequence-like ;

proof end;

definition

let X, x be set ;

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

;

end;
func IFXFinSequence (x,X) -> XFinSequence of X equals :Def1: :: ALGSTR_4:def 1

x if x is XFinSequence of X

otherwise <%> X;

correctness x if x is XFinSequence of X

otherwise <%> X;

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 b

;

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

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;

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

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

[:Y,Z:] c= the_universe_of X

proof end;

scheme :: ALGSTR_4:sch 1

FuncRecursiveUniq{ F_{1}( set ) -> set , F_{2}() -> Function, F_{3}() -> Function } :

provided

FuncRecursiveUniq{ F

provided

A1:
( dom F_{2}() = NAT & ( for n being Nat holds F_{2}() . n = F_{1}((F_{2}() | n)) ) )
and

A2: ( dom F_{3}() = NAT & ( for n being Nat holds F_{3}() . n = F_{1}((F_{3}() | n)) ) )

A2: ( dom F

proof end;

scheme :: ALGSTR_4:sch 3

FuncRecursiveUniqu2{ F_{1}() -> non empty set , F_{2}( XFinSequence of F_{1}()) -> Element of F_{1}(), F_{3}() -> sequence of F_{1}(), F_{4}() -> sequence of F_{1}() } :

provided

FuncRecursiveUniqu2{ F

provided

A1:
for n being Nat holds F_{3}() . n = F_{2}((F_{3}() | n))
and

A2: for n being Nat holds F_{4}() . n = F_{2}((F_{4}() | n))

A2: for n being Nat holds F

proof end;

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

for f, g being Function holds

( f extends g iff ( dom g c= dom f & f tolerates g ) );

registration
end;

:: Ch I ?1.6 Def.11 Algebra I Bourbaki

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

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

registration

let M be multMagma ;

existence

ex b_{1} being Equivalence_Relation of M st b_{1} is compatible ;

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

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

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;

consistency

for b_{1} being BinOp of (Class R) holds verum;

existence

( ( for b_{1} being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b_{1} 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

b_{1} . (x,y) = Class (R,(v * w)) ) & ( M is empty implies ex b_{1} being BinOp of (Class R) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = Class (R,(v * w)) ) implies b_{1} = b_{2} ) & ( M is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

end;
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 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 = {} ;

consistency

for b

existence

( ( for b

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

b

uniqueness

for b

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

b

for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds

b

proof end;

:: deftheorem Def4 defines ClassOp ALGSTR_4:def 4 :

for M being multMagma

for R being compatible Equivalence_Relation of M

for b_{3} being BinOp of (Class R) holds

( ( not M is empty implies ( b_{3} = 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

b_{3} . (x,y) = Class (R,(v * w)) ) ) & ( M is empty implies ( b_{3} = ClassOp R iff b_{3} = {} ) ) );

for M being multMagma

for R being compatible Equivalence_Relation of M

for b

( ( not M is empty implies ( b

for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds

b

:: Ch I ?1.6 Def.11 Algebra I Bourbaki

definition

let M be multMagma ;

let R be compatible Equivalence_Relation of M;

correctness

coherence

multMagma(# (Class R),(ClassOp R) #) is multMagma ;

;

end;
let R be compatible Equivalence_Relation of M;

correctness

coherence

multMagma(# (Class R),(ClassOp R) #) is multMagma ;

;

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

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;

correctness

coherence

M ./. R is strict ;

;

end;
let R be compatible Equivalence_Relation of M;

correctness

coherence

M ./. R is strict ;

;

registration

let M be non empty multMagma ;

let R be compatible Equivalence_Relation of M;

correctness

coherence

not M ./. R is empty ;

;

end;
let R be compatible Equivalence_Relation of M;

correctness

coherence

not M ./. R is empty ;

;

definition

let M be non empty multMagma ;

let R be compatible Equivalence_Relation of M;

ex b_{1} being Function of M,(M ./. R) st

for v being Element of M holds b_{1} . v = Class (R,v)

for b_{1}, b_{2} being Function of M,(M ./. R) st ( for v being Element of M holds b_{1} . v = Class (R,v) ) & ( for v being Element of M holds b_{2} . v = Class (R,v) ) holds

b_{1} = b_{2}

end;
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 for v being Element of M holds it . v = Class (R,v);

ex b

for v being Element of M holds b

proof end;

uniqueness for b

b

proof 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 b_{3} being Function of M,(M ./. R) holds

( b_{3} = nat_hom R iff for v being Element of M holds b_{3} . v = Class (R,v) );

for M being non empty multMagma

for R being compatible Equivalence_Relation of M

for b

( b

registration

let M be non empty multMagma ;

let R be compatible Equivalence_Relation of M;

correctness

coherence

nat_hom R is multiplicative ;

end;
let R be compatible Equivalence_Relation of M;

correctness

coherence

nat_hom R is multiplicative ;

proof end;

registration

let M be non empty multMagma ;

let R be compatible Equivalence_Relation of M;

correctness

coherence

nat_hom R is onto ;

end;
let R be compatible Equivalence_Relation of M;

correctness

coherence

nat_hom R is onto ;

proof end;

definition
end;

:: Ch I ?1.6 Algebra I Bourbaki

definition

let M be multMagma ;

let r be Relators of M;

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;

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

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;

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

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

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

definition

let X, Y be set ;

let f be Function of X,Y;

ex b_{1} being Equivalence_Relation of X st

for x, y being object holds

( [x,y] in b_{1} iff ( x in X & y in X & f . x = f . y ) )

for b_{1}, b_{2} being Equivalence_Relation of X st ( for x, y being object holds

( [x,y] in b_{1} iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ( x in X & y in X & f . x = f . y ) ) ) holds

b_{1} = b_{2}

end;
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 for x, y being object holds

( [x,y] in it iff ( x in X & y in X & f . x = f . y ) );

ex b

for x, y being object holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def8 defines equ_kernel ALGSTR_4:def 8 :

for X, Y being set

for f being Function of X,Y

for b_{4} being Equivalence_Relation of X holds

( b_{4} = equ_kernel f iff for x, y being object holds

( [x,y] in b_{4} iff ( x in X & y in X & f . x = f . y ) ) );

for X, Y being set

for f being Function of X,Y

for b

( b

( [x,y] in b

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

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

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 ;

ex b_{1} being multMagma st

( the carrier of b_{1} c= the carrier of M & the multF of b_{1} = the multF of M || the carrier of b_{1} )

end;
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 ( the carrier of it c= the carrier of M & the multF of it = the multF of M || the carrier of it );

ex b

( the carrier of b

proof end;

:: deftheorem Def9 defines multSubmagma ALGSTR_4:def 9 :

for M, b_{2} being multMagma holds

( b_{2} is multSubmagma of M iff ( the carrier of b_{2} c= the carrier of M & the multF of b_{2} = the multF of M || the carrier of b_{2} ) );

for M, b

( b

registration
end;

registration

let M be non empty multMagma ;

existence

not for b_{1} being multSubmagma of M holds b_{1} is empty

end;
existence

not for b

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

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

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

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

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 ;

correctness

existence

ex b_{1} being Subset of M st b_{1} is stable ;

end;
correctness

existence

ex b

proof end;

registration

let M be multMagma ;

let N be multSubmagma of M;

correctness

coherence

for b_{1} being Subset of M st b_{1} = the carrier of N holds

b_{1} is stable ;

by Th8;

end;
let N be multSubmagma of M;

correctness

coherence

for b

b

by Th8;

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

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;

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

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

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

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;

correctness

coherence

the multF of M || A is BinOp of A;

end;
let A be stable Subset of M;

correctness

coherence

the multF of M || A is BinOp of A;

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

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;

ex b_{1} being strict multSubmagma of M st

( A c= the carrier of b_{1} & ( for N being strict multSubmagma of M st A c= the carrier of N holds

b_{1} is multSubmagma of N ) )

for b_{1}, b_{2} being strict multSubmagma of M st A c= the carrier of b_{1} & ( for N being strict multSubmagma of M st A c= the carrier of N holds

b_{1} is multSubmagma of N ) & A c= the carrier of b_{2} & ( for N being strict multSubmagma of M st A c= the carrier of N holds

b_{2} is multSubmagma of N ) holds

b_{1} = b_{2}

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

ex b

( A c= the carrier of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines the_submagma_generated_by ALGSTR_4:def 12 :

for M being multMagma

for A being Subset of M

for b_{3} being strict multSubmagma of M holds

( b_{3} = the_submagma_generated_by A iff ( A c= the carrier of b_{3} & ( for N being strict multSubmagma of M st A c= the carrier of N holds

b_{3} is multSubmagma of N ) ) );

for M being multMagma

for A being Subset of M

for b

( b

b

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 )

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;

correctness

coherence

the_submagma_generated_by A is empty ;

by Th14;

end;
let A be empty Subset of M;

correctness

coherence

the_submagma_generated_by A is empty ;

by Th14;

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

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 S_{1}[ 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 S_{1}[e,u]

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

S_{1}[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))

ex b_{1} being sequence of (bool (the_universe_of (X \/ NAT))) st

( b_{1} . 0 = {} & b_{1} . 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 = [:(b_{1} . p),(b_{1} . (n - p)):] ) & b_{1} . n = Union (disjoin fs) ) ) )

for b_{1}, b_{2} being sequence of (bool (the_universe_of (X \/ NAT))) st b_{1} . 0 = {} & b_{1} . 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 = [:(b_{1} . p),(b_{1} . (n - p)):] ) & b_{1} . n = Union (disjoin fs) ) ) & b_{2} . 0 = {} & b_{2} . 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 = [:(b_{2} . p),(b_{2} . (n - p)):] ) & b_{2} . n = Union (disjoin fs) ) ) holds

b_{1} = b_{2}

end;
defpred S

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

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

S

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

ex b

( b

ex fs being FinSequence st

( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds

fs . p = [:(b

proof end;

uniqueness for b

ex fs being FinSequence st

( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds

fs . p = [:(b

ex fs being FinSequence st

( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds

fs . p = [:(b

b

proof end;

:: deftheorem Def13 defines free_magma_seq ALGSTR_4:def 13 :

for X being set

for b_{2} being sequence of (bool (the_universe_of (X \/ NAT))) holds

( b_{2} = free_magma_seq X iff ( b_{2} . 0 = {} & b_{2} . 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 = [:(b_{2} . p),(b_{2} . (n - p)):] ) & b_{2} . n = Union (disjoin fs) ) ) ) );

for X being set

for b

( b

ex fs being FinSequence st

( len fs = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds

fs . p = [:(b

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

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;

correctness

coherence

not free_magma (X,n) is empty ;

end;
let n be non zero Nat;

correctness

coherence

not free_magma (X,n) is empty ;

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

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

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

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;

definition

let X be set ;

coherence

Union (disjoin ((free_magma_seq X) | NATPLUS)) is set ;

;

end;
func free_magma_carrier X -> set equals :: ALGSTR_4:def 15

Union (disjoin ((free_magma_seq X) | NATPLUS));

correctness Union (disjoin ((free_magma_seq X) | NATPLUS));

coherence

Union (disjoin ((free_magma_seq X) | NATPLUS)) is set ;

;

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

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;

registration
end;

registration

let X be non empty set ;

correctness

coherence

not free_magma_carrier X is empty ;

by Th24;

let w be Element of free_magma_carrier X;

correctness

coherence

for b_{1} being number st b_{1} = w `2 holds

( not b_{1} is zero & b_{1} is natural );

end;
correctness

coherence

not free_magma_carrier X is empty ;

by Th24;

let w be Element of free_magma_carrier X;

correctness

coherence

for b

( not b

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

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

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 :: ALGSTR_4:28

definition

let X be set ;

consistency

for b_{1} being BinOp of (free_magma_carrier X) holds verum;

existence

( ( for b_{1} being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b_{1} 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

b_{1} . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) & ( X is empty implies ex b_{1} being BinOp of (free_magma_carrier X) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) implies b_{1} = b_{2} ) & ( X is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

end;
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 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 = {} ;

consistency

for b

existence

( ( for b

for v, w being Element of free_magma_carrier X

for n, m being Nat st n = v `2 & m = w `2 holds

b

uniqueness

for b

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

b

for n, m being Nat st n = v `2 & m = w `2 holds

b

proof end;

:: deftheorem Def16 defines free_magma_mult ALGSTR_4:def 16 :

for X being set

for b_{2} being BinOp of (free_magma_carrier X) holds

( ( not X is empty implies ( b_{2} = 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

b_{2} . (v,w) = [[[(v `1),(w `1)],(v `2)],(n + m)] ) ) & ( X is empty implies ( b_{2} = free_magma_mult X iff b_{2} = {} ) ) );

for X being set

for b

( ( not X is empty implies ( b

for n, m being Nat st n = v `2 & m = w `2 holds

b

:: Ch I ?7.1 Algebra I Bourbaki

definition

let X be set ;

coherence

multMagma(# (free_magma_carrier X),(free_magma_mult X) #) is multMagma ;

;

end;
func free_magma X -> multMagma equals :: ALGSTR_4:def 17

multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

correctness multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

coherence

multMagma(# (free_magma_carrier X),(free_magma_mult X) #) is multMagma ;

;

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

for X being set holds free_magma X = multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

registration
end;

registration
end;

registration

let X be non empty set ;

correctness

coherence

not free_magma X is empty ;

;

let w be Element of (free_magma X);

correctness

coherence

for b_{1} being number st b_{1} = w `2 holds

( not b_{1} is zero & b_{1} is natural );

;

end;
correctness

coherence

not free_magma X is empty ;

;

let w be Element of (free_magma X);

correctness

coherence

for b

( not b

;

definition

let X be set ;

let w be Element of (free_magma X);

correctness

coherence

( ( not X is empty implies w `2 is Nat ) & ( X is empty implies 0 is Nat ) );

consistency

for b_{1} being Nat holds verum;

;

end;
let w be Element of (free_magma X);

correctness

coherence

( ( not X is empty implies w `2 is Nat ) & ( X is empty implies 0 is Nat ) );

consistency

for b

;

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

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

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 )

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)

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 )

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 )

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;

consistency

for b_{1} being Function of (free_magma (X,n)),(free_magma X) holds verum;

existence

( ( for b_{1} being Function of (free_magma (X,n)),(free_magma X) holds verum ) & ( n > 0 implies ex b_{1} being Function of (free_magma (X,n)),(free_magma X) st

for x being set st x in dom b_{1} holds

b_{1} . x = [x,n] ) & ( not n > 0 implies ex b_{1} being Function of (free_magma (X,n)),(free_magma X) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} being Function of (free_magma (X,n)),(free_magma X) holds

( ( n > 0 & ( for x being set st x in dom b_{1} holds

b_{1} . x = [x,n] ) & ( for x being set st x in dom b_{2} holds

b_{2} . x = [x,n] ) implies b_{1} = b_{2} ) & ( not n > 0 & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

end;
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 for x being set st x in dom it holds

it . x = [x,n] if n > 0

otherwise it = {} ;

consistency

for b

existence

( ( for b

for x being set st x in dom b

b

uniqueness

for b

( ( n > 0 & ( for x being set st x in dom b

b

b

proof end;

:: deftheorem Def19 defines canon_image ALGSTR_4:def 19 :

for X being set

for n being Nat

for b_{3} being Function of (free_magma (X,n)),(free_magma X) holds

( ( n > 0 implies ( b_{3} = canon_image (X,n) iff for x being set st x in dom b_{3} holds

b_{3} . x = [x,n] ) ) & ( not n > 0 implies ( b_{3} = canon_image (X,n) iff b_{3} = {} ) ) );

for X being set

for n being Nat

for b

( ( n > 0 implies ( b

b

Lm2: for X being set

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

proof end;

registration
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

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

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)

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;

ex b_{1} 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

b_{1} . x = (f . y) * (g . z)

for b_{1}, b_{2} 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

b_{1} . 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

b_{2} . x = (f . y) * (g . z) ) holds

b_{1} = b_{2}

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

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof 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 b_{7} being Function of [:[:(free_magma (X,n)),(free_magma (X,m)):],{n}:],M holds

( b_{7} = [: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

b_{7} . x = (f . y) * (g . z) );

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 b

( b

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

b

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

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

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 )

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

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 )

( g is bijective & g is multiplicative )

proof end;

definition

let X, Y be non empty set ;

let f be Function of X,Y;

ex b_{1} being Function of (free_magma X),(free_magma Y) st

( b_{1} is multiplicative & b_{1} extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") )

for b_{1}, b_{2} being Function of (free_magma X),(free_magma Y) st b_{1} is multiplicative & b_{1} extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") & b_{2} is multiplicative & b_{2} extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") holds

b_{1} = b_{2}

end;
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 ( it is multiplicative & it extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{4} being Function of (free_magma X),(free_magma Y) holds

( b_{4} = free_magmaF f iff ( b_{4} is multiplicative & b_{4} extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") ) );

for X, Y being non empty set

for f being Function of X,Y

for b

( b

registration

let X, Y be non empty set ;

let f be Function of X,Y;

coherence

free_magmaF f is multiplicative by Def21;

end;
let f be Function of X,Y;

coherence

free_magmaF f is multiplicative by Def21;

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)

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

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

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

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