environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, XCMPLX_0, CLVECT_1, NORMSP_1, NAT_1, ARYTM_1, ARYTM_3, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, STRUCT_0, PRE_TOPC, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, XBOOLE_0, VALUED_1, CFCONT_1, COMSEQ_1, SEQ_1, SEQ_4, NFCONT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2, FUNCT_2, PRE_TOPC, XREAL_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, RLVECT_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, VFUNCT_1, COMSEQ_1, CFCONT_1, RCOMP_1, COMSEQ_2, STRUCT_0, VFUNCT_2, CLVECT_1, NFCONT_1, XXREAL_0, NORMSP_0, NORMSP_1;
definitions TARSKI, NFCONT_1;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1, RCOMP_1, SEQ_2, RELAT_1, FUNCT_1, VFUNCT_1, LOPBAN_1, FUNCT_2, SEQ_4, NORMSP_1, PARTFUN1, PARTFUN2, CLVECT_1, COMSEQ_2, VFUNCT_2, NFCONT_1, CLOPBAN1, CFCONT_1, COMPLEX1, XREAL_1, XXREAL_0, BHSP_1, VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0, VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2, XCMPLX_0;
constructors HIDDEN, REAL_1, SEQ_4, RCOMP_1, PARTFUN2, COMSEQ_2, COMSEQ_3, CFCONT_1, NFCONT_1, VFUNCT_2, SEQ_2, RELSET_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RELAT_1;
expansions TARSKI, NFCONT_1;