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, ZFMISC_1, VALUED_0, FCONT_1, NORMSP_1, STRUCT_0, SUPINF_2, PRE_TOPC;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, VALUED_0, COMPLEX1, ZFMISC_1, SEQ_1, SEQ_2, RCOMP_1, FCONT_1, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NFCONT_1;
definitions FCONT_1;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, SEQ_2, SEQM_3, SEQ_4, PARTFUN1, XREAL_0, PARTFUN2, RCOMP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, MEMBERED, VALUED_0, NFCONT_1, NORMSP_0, NORMSP_1, RLVECT_1, LOPBAN_3, VFUNCT_1, LOPBAN_1, BHSP_1, NUMBERS;
schemes NAT_1, RECDEF_1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0, FUNCT_2, RELAT_1, FUNCT_1, STRUCT_0, VFUNCT_1;
constructors HIDDEN, REAL_1, COMPLEX1, MEMBERED, SEQ_2, RCOMP_1, RELSET_1, FCONT_1, NFCONT_1, VFUNCT_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RELAT_1, RLVECT_1;
expansions FCONT_1;