environ
vocabularies HIDDEN, NAT_1, PBOOLE, FUNCT_1, CARD_1, XBOOLE_0, FINSEQ_2, FINSEQ_1, RELAT_1, TARSKI, NUMBERS, SUBSET_1, UNIALG_1, UNIALG_2, MSUALG_1, FUNCOP_1, CQC_SIM1, STRUCT_0, MSUALG_2, MARGREL1, PARTFUN1, CARD_3, FUNCT_2, ZFMISC_1, EQREL_1, INCPROJ, WELLORD1, GROUP_6, LATTICES, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, CARD_3, ORDINAL1, LATTICES, LATTICE4, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0, PBOOLE, UNIALG_1, UNIALG_2, NUMBERS, FINSEQ_1, FINSEQ_2, MARGREL1, MSUALG_1, MSUALG_2;
definitions TARSKI, XBOOLE_0, MSUALG_2, PBOOLE, LATTICE4, UNIALG_1, UNIALG_2, FUNCT_2;
theorems MSUALG_1, MSUALG_2, PBOOLE, TARSKI, UNIALG_1, UNIALG_2, FUNCT_1, RELAT_1, FUNCOP_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, ZFMISC_1, CARD_3, LATTICES, MSUHOM_1, XBOOLE_0, XBOOLE_1, STRUCT_0, MARGREL1, CARD_1;
schemes FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_2, RELAT_1, PBOOLE, STRUCT_0, UNIALG_1, UNIALG_2, MSUALG_1, MSUALG_2, FINSEQ_1, MARGREL1;
constructors HIDDEN, BINOP_1, FINSEQOP, FILTER_1, UNIALG_2, LATTICE4, MSUALG_2, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities MSUALG_2, UNIALG_2, FUNCOP_1, FINSEQ_2, ORDINAL1;
expansions TARSKI, XBOOLE_0, MSUALG_2, PBOOLE, UNIALG_1, UNIALG_2, FUNCT_2;
reconsider z = 0 as Element of {0} by TARSKI:def 1;
:: Universal and Many Sorted Algebras