environ
vocabularies HIDDEN, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, PBOOLE, MEMBER_1, MSUALG_3, FUNCT_2, FUNCT_6, PZFMISC1, SUBSET_1, REALSET1, STRUCT_0, MSUALG_1, MSUALG_2, UNIALG_2, PARTFUN1, PRALG_2, CARD_3, RLVECT_2, PRELAMB, MSAFREE, FINSET_1, MSAFREE2, MSUALG_6, MARGREL1, NAT_1, GROUP_6, CLOSURE2, ZFMISC_1, FINSEQ_1, CARD_1, PRALG_3, FUNCT_4, FUNCOP_1, NUMBERS, ZF_LANG, MCART_1, ZF_MODEL, WELLORD1, MSUALG_4, EQUATION, AFINSQ_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, STRUCT_0, FUNCT_2, MCART_1, FINSET_1, FINSEQ_1, FINSEQ_2, FUNCT_4, FUNCT_6, PZFMISC1, CARD_3, AFINSQ_1, MSUALG_1, PRALG_2, FUNCOP_1, MSUALG_2, PRALG_3, MSUALG_3, MSUALG_4, MSAFREE, MSAFREE2, CLOSURE2, MSUALG_6;
definitions TARSKI, PBOOLE, PRALG_2, MSUALG_2, MSUALG_3, FINSET_1, MSAFREE, MSAFREE2, XBOOLE_0, PZFMISC1;
theorems MSUALG_1, EXTENS_1, MSAFREE2, MSSCYC_1, CARD_3, FUNCT_4, FUNCOP_1, FUNCT_1, FUNCT_2, MCART_1, MSAFREE, FINSEQ_1, CLOSURE2, FINSET_1, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_9, PBOOLE, PARTFUN1, MSUALG_6, MSSUBFAM, INSTALG1, PRALG_2, PRALG_3, RELAT_1, TARSKI, ZFMISC_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCT_6, FINSEQ_2, AFINSQ_1, CARD_1;
schemes MSSUBFAM, PBOOLE, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_1, STRUCT_0, MSUALG_1, MSUALG_2, RELAT_1, FUNCT_1, PRALG_2, MSUALG_3, MSAFREE, MSUALG_4, EXTENS_1, CLOSURE2, MSUALG_6, PRALG_3, MSUALG_9, MSSUBFAM, PBOOLE, AUTALG_1, AFINSQ_1;
constructors HIDDEN, FUNCT_4, PZFMISC1, MSUALG_3, MSAFREE2, CLOSURE2, MSUALG_6, PRALG_3, RELSET_1, XTUPLE_0, NUMBERS, AFINSQ_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities PRALG_2, MSUALG_1;
expansions TARSKI, PBOOLE, MSUALG_2, MSUALG_3, MSAFREE, XBOOLE_0, PZFMISC1;
Lm1:
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e