environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, ORDINAL1, RELAT_1, XBOOLE_0, TARSKI, AFINSQ_1, SUBSET_1, YELLOW_6, ZFMISC_1, CLASSES1, PARTFUN1, ALGSTR_0, BINOP_1, EQREL_1, MSUALG_6, STRUCT_0, GROUP_6, MSSUBFAM, FUNCT_2, SETFAM_1, REALSET1, CIRCUIT2, CARD_1, XXREAL_0, FINSEQ_1, ARYTM_1, CARD_3, ARYTM_3, NAT_1, XCMPLX_0, MCART_1, NAT_LAT, ALGSTR_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, XCMPLX_0, XFAMILY, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_6, FUNCT_2, XXREAL_0, NAT_1, CLASSES1, FINSEQ_1, CARD_3, AFINSQ_1, NAT_D, YELLOW_6, BINOP_1, STRUCT_0, ALGSTR_0, RELSET_1, GROUP_6, MCART_1, NAT_LAT, PARTFUN1, REALSET1, EQREL_1, ALG_1, GROUP_2;
definitions TARSKI;
theorems TARSKI, XBOOLE_1, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, AFINSQ_1, FINSEQ_1, XREAL_1, NAT_1, XXREAL_0, XREAL_0, ZFMISC_1, CLASSES1, CARD_3, YELLOW_6, BINOP_1, RELSET_1, MCART_1, INT_1, SUBSET_1, XBOOLE_0, NAT_LAT, FUNCT_5, GROUP_6, PARTFUN1, REALSET1, SETFAM_1, EQREL_1, OSALG_4, GROUP_2, FUNCT_6, XTUPLE_0;
schemes ORDINAL1, NAT_1, CLASSES1, FINSEQ_1, BINOP_1, FUNCT_2, EQREL_1, RELAT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, FUNCT_2, INT_1, STRUCT_0, RELSET_1, NAT_LAT, REALSET1, EQREL_1, GROUP_2, XTUPLE_0;
constructors HIDDEN, NAT_1, CLASSES1, AFINSQ_1, NAT_D, YELLOW_6, BINOP_1, RELSET_1, FACIRC_1, GROUP_6, NAT_LAT, REALSET1, EQREL_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, ALGSTR_0, CARD_1, ORDINAL1;
expansions TARSKI;
definition
let M be
multMagma ;
let R be
compatible Equivalence_Relation of
M;
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 ) );
end;
Lm1:
for X being set
for n being Nat st n > 0 holds
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X
definition
let X be
set ;
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 ) );
end;
definition
let X be
set ;
let n be
Nat;
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 ) );
end;
Lm2:
for X being set
for n being Nat holds canon_image (X,n) is one-to-one
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] ) )
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:
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)
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
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) );
definition
let X,
Y be non
empty set ;
let f be
Function of
X,
Y;
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)) ") )
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
end;