environ
vocabularies HIDDEN, PBOOLE, RELAT_1, XBOOLE_0, FUNCT_1, SUBSET_1, CARD_3, TARSKI, STRUCT_0, MSUALG_1, UNIALG_2, FINSEQ_1, MARGREL1, PARTFUN1, FUNCT_2, ZFMISC_1, QC_LANG1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, XXREAL_2, MSUALG_2, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, SETFAM_1, FINSEQ_2, LATTICES, BINOP_1, CARD_3, PBOOLE, MSUALG_1;
definitions TARSKI, PBOOLE, LATTICES, XBOOLE_0;
theorems TARSKI, FUNCT_1, FINSEQ_1, PBOOLE, CARD_3, MSUALG_1, FUNCT_2, ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, PARTFUN1, FINSEQ_2;
schemes CLASSES1, BINOP_1, FUNCT_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, STRUCT_0, LATTICES, MSUALG_1, FINSEQ_1, FUNCT_2, PARTFUN1, RELSET_1;
constructors HIDDEN, SETFAM_1, BINOP_1, CARD_3, LATTICES, MSUALG_1, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES;
expansions TARSKI, PBOOLE, LATTICES;
Lm1:
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0
Lm2:
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra over
S;
existence
ex b1 being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2
uniqueness
for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
end;
definition
let S be non
empty non
void ManySortedSign ;
let U0 be
non-empty MSAlgebra over
S;
existence
ex b1 being BinOp of (MSSub U0) st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
end;
:: Subalgebras of a Many Sorted Algebra.
::