environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2, ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1, COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, XXREAL_1, VALUED_1, ORDINAL4, ZFMISC_1, VALUED_0, SEQ_4, XXREAL_2, SQUARE_1, SEQM_3, FCONT_1, JGRAPH_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, ZFMISC_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, SQUARE_1, PARTFUN2, RFUNCT_1, RCOMP_1, RECDEF_1, RFUNCT_2;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN1, XREAL_0, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, MEMBERED, XXREAL_2, VALUED_0, NUMBERS;
schemes NAT_1, RECDEF_1, FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, RFUNCT_2, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, RELAT_1, RFUNCT_1, SEQ_2, FUNCT_1, ZFMISC_1;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQM_3, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, SQUARE_1, RELAT_1, VALUED_1;
expansions TARSKI, FUNCT_1;