environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, MSUALG_1, ALTCAT_1, MSALIMIT, SUBSET_1, FUNCT_1, CAT_1, RELAT_1, PBOOLE, ZFMISC_1, MCART_1, PUA2MSS1, RELAT_2, BINOP_1, TARSKI, MSUALG_6, FUNCT_2, PARTFUN1, NUMBERS, CARD_3, FUNCOP_1, PZFMISC1, MARGREL1, MEMBER_1, FUNCT_6, FINSEQ_4, MSUALG_3, MSINST_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1, STRUCT_0, FUNCT_2, RELSET_1, PARTFUN1, FINSEQ_2, CARD_3, BINOP_1, MULTOP_1, FUNCT_6, FUNCOP_1, PBOOLE, PZFMISC1, PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, PRALG_2, PUA2MSS1, MSUALG_6, MSALIMIT;
definitions ALTCAT_1, MSUALG_3, PBOOLE, TARSKI;
theorems XBOOLE_0, ALTCAT_1, ALTCAT_2, AUTALG_1, CARD_3, CLOSURE1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_6, FUNCTOR0, MCART_1, MSSUBFAM, MSUALG_1, MSUALG_3, MSUALG_6, MSALIMIT, MULTOP_1, PARTFUN1, PBOOLE, PRALG_2, PUA2MSS1, RELAT_1, TARSKI, ZFMISC_1, PRALG_1, XBOOLE_1, PZFMISC1, FINSEQ_2, XTUPLE_0;
schemes ALTCAT_1, MSSUBFAM, TARSKI, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCOP_1, RELAT_1, STRUCT_0, MSUALG_1, ALTCAT_1, MSUALG_6, MSALIMIT, MSSUBFAM, PBOOLE, FINSEQ_1, XTUPLE_0;
constructors HIDDEN, PZFMISC1, MSUALG_3, ALTCAT_1, PUA2MSS1, CLOSURE1, MSUALG_6, MSALIMIT, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities ALTCAT_1, TARSKI, BINOP_1;
expansions MSUALG_3, TARSKI;
definition
let A be non
empty set ;
func MSSCat A -> non
empty strict AltCatStr means :
Def1:
( the
carrier of
it = MSS_set A & ( for
i,
j being
Element of
MSS_set A holds the
Arrows of
it . (
i,
j)
= MSS_morph (
i,
j) ) & ( for
i,
j,
k being
Object of
it st
i in MSS_set A &
j in MSS_set A &
k in MSS_set A holds
for
f1,
f2,
g1,
g2 being
Function st
[f1,f2] in the
Arrows of
it . (
i,
j) &
[g1,g2] in the
Arrows of
it . (
j,
k) holds
( the Comp of it . (i,j,k)) . (
[g1,g2],
[f1,f2])
= [(g1 * f1),(g2 * f2)] ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) )
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b1 . (i,j) & [g1,g2] in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) holds
b1 = b2
end;
::
deftheorem Def1 defines
MSSCat MSINST_1:def 1 :
for A being non empty set
for b2 being non empty strict AltCatStr holds
( b2 = MSSCat A iff ( the carrier of b2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b2 . (i,j) & [g1,g2] in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );
definition
let S be non
empty non
void ManySortedSign ;
let A be non
empty set ;
let i,
j be
set ;
assume that A1:
i in MSAlg_set (
S,
A)
and A2:
j in MSAlg_set (
S,
A)
;
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds
( x in b2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) holds
b1 = b2
end;
definition
let S be non
empty non
void ManySortedSign ;
let A be non
empty set ;
func MSAlgCat (
S,
A)
-> non
empty strict AltCatStr means :
Def4:
( the
carrier of
it = MSAlg_set (
S,
A) & ( for
i,
j being
Element of
MSAlg_set (
S,
A) holds the
Arrows of
it . (
i,
j)
= MSAlg_morph (
S,
A,
i,
j) ) & ( for
i,
j,
k being
Object of
it for
f,
g being
Function-yielding Function st
f in the
Arrows of
it . (
i,
j) &
g in the
Arrows of
it . (
j,
k) holds
( the Comp of it . (i,j,k)) . (
g,
f)
= g ** f ) );
existence
ex b1 being non empty strict AltCatStr st
( the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) )
uniqueness
for b1, b2 being non empty strict AltCatStr st the carrier of b1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b1
for f, g being Function-yielding Function st f in the Arrows of b1 . (i,j) & g in the Arrows of b1 . (j,k) holds
( the Comp of b1 . (i,j,k)) . (g,f) = g ** f ) & the carrier of b2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b2
for f, g being Function-yielding Function st f in the Arrows of b2 . (i,j) & g in the Arrows of b2 . (j,k) holds
( the Comp of b2 . (i,j,k)) . (g,f) = g ** f ) holds
b1 = b2
end;
::
deftheorem Def4 defines
MSAlgCat MSINST_1:def 4 :
for S being non empty non void ManySortedSign
for A being non empty set
for b3 being non empty strict AltCatStr holds
( b3 = MSAlgCat (S,A) iff ( the carrier of b3 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b3 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b3
for f, g being Function-yielding Function st f in the Arrows of b3 . (i,j) & g in the Arrows of b3 . (j,k) holds
( the Comp of b3 . (i,j,k)) . (g,f) = g ** f ) ) );