environ
vocabularies HIDDEN, UNIALG_1, NAT_1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, SUBSET_1, FINSEQ_1, FUNCOP_1, PBOOLE, CARD_3, MSUALG_1, XXREAL_0, STRUCT_0, FINSEQ_2, PARTFUN1, CQC_SIM1, CARD_1, UNIALG_2, MARGREL1, NUMBERS, MSUALG_3, MEMBER_1, MSUHOM_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, CARD_3, FUNCOP_1, FINSEQ_1, STRUCT_0, UNIALG_1, UNIALG_2, FINSEQ_2, ALG_1, MSUALG_3, MSUALG_1, XXREAL_0;
definitions ALG_1, MSUALG_3, TARSKI;
theorems TARSKI, FINSEQ_2, MSUALG_1, UNIALG_2, MSUALG_3, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, UNIALG_1, PBOOLE, MONOID_1, CARD_3, RELAT_1, XBOOLE_0, XBOOLE_1, PARTFUN1, FINSEQ_3;
schemes ;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, XREAL_0, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, RELAT_1, PBOOLE, FINSEQ_1;
constructors HIDDEN, FINSEQOP, ALG_1, MSUALG_3, XREAL_0, RELSET_1, NAT_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities FUNCOP_1, FINSEQ_2, UNIALG_2;
expansions ALG_1, MSUALG_3, TARSKI, UNIALG_2;
Lm1:
for U1 being Universal_Algebra holds dom (signature U1) = dom the charact of U1
Lm2:
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o being OperSymbol of (MSSign U1) holds Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2
Lm3:
for U1 being Universal_Algebra
for n being Nat st n in dom the charact of U1 holds
n is OperSymbol of (MSSign U1)