environ
vocabularies HIDDEN, NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1, FDIFF_1, SUBSET_1, LOPBAN_1, RELAT_1, RSSPACE, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, FUNCOP_1, XBOOLE_0, NDIFF_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1, FUNCOP_1, RLVECT_1, PRE_TOPC, STRUCT_0, VALUED_0, VALUED_1, SEQ_1, SEQ_2, VFUNCT_1, NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, NFCONT_1, FDIFF_1, NDIFF_1;
definitions TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_2, LOPBAN_3, PARTFUN1, PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, VALUED_0, ORDINAL1, VECTSP_1, NORMSP_0, XREAL_0;
schemes FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, MEMBERED, FDIFF_1, STRUCT_0, LOPBAN_1, NDIFF_1, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, FUNCOP_1, NAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1, NFCONT_1, NDIFF_1, VALUED_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1;
expansions TARSKI;