environ
vocabularies HIDDEN, MSUALG_1, GLIB_000, SUBSET_1, XBOOLE_0, UNIALG_2, STRUCT_0, RELAT_1, TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FINSEQ_1, MARGREL1, NAT_1, PARTFUN1, PRELAMB, MSAFREE, MSUALG_3, TREES_4, REALSET1, MSUALG_2, FINSET_1, PRALG_1, CARD_1, TREES_2, DTCONSTR, TREES_3, ZFMISC_1, LANG1, TDGROUP, TREES_1, MSAFREE2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, CARD_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FINSEQ_1, FUNCT_2, CARD_3, TREES_1, TREES_2, TREES_3, TREES_4, PBOOLE, STRUCT_0, MSUALG_1, FINSEQ_2, MSAFREE, MSUALG_2, FUNCOP_1, DTCONSTR, LANG1, PRE_POLY, RELSET_1, MSUALG_3;
definitions TARSKI, FINSET_1, MSUALG_2, FUNCT_1, PBOOLE;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, TREES_3, TREES_4, SUBSET_1, CARD_3, FUNCOP_1, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, CARD_2, CARD_1, DTCONSTR, LANG1, PRE_CIRC, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FINSET_1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes DOMAIN_1, PBOOLE, MSAFREE1, FUNCT_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, TREES_1, CARD_3, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, RELAT_1, MSUALG_1, MSUALG_2, MSAFREE, ORDINAL1, PBOOLE, FINSEQ_1;
constructors HIDDEN, XXREAL_0, NAT_1, MSUALG_3, MSAFREE, SEQ_4, RELSET_1, PRE_POLY, FINSEQ_2, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET;
equalities MSUALG_1, FUNCOP_1;
expansions MSUALG_1, FINSET_1, MSUALG_2, PBOOLE;
definition
let S be non
empty non
void ManySortedSign ;
let MSA be
non-empty MSAlgebra over
S;
existence
ex b1 being ManySortedFunction of (FreeEnv MSA),MSA st
( b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b1 . s) . y = x ) )
uniqueness
for b1, b2 being ManySortedFunction of (FreeEnv MSA),MSA st b1 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b1 . s) . y = x ) & b2 is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b2 . s) . y = x ) holds
b1 = b2
end;
:: Many Sorted Signatures
::---------------------------------------------------------------------------