environ
vocabularies HIDDEN, FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, TARSKI, BINOP_1, SUBSET_1, MCART_1, REALSET1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_3;
definitions ;
theorems FUNCT_1, FUNCT_2, FUNCT_3, ZFMISC_1, RELAT_1, PARTFUN1;
schemes ;
registrations XBOOLE_0, FUNCT_1, RELSET_1, ZFMISC_1, FUNCT_2;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, RELSET_1, SETFAM_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1;
expansions ;