environ
vocabularies HIDDEN, NUMBERS, SEQ_1, REAL_1, XXREAL_2, CARD_1, XXREAL_0, ORDINAL2, VALUED_1, RELAT_1, RINFSUP1, FUNCT_2, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, ARYTM_3, COMPLEX1, NAT_1, SEQ_4, MEMBER_1, LOPBAN_1, NORMSP_2, REWRITE1, BHSP_3, RSSPACE3, METRIC_1, SEQ_2, NORMSP_1, PRE_TOPC, ARYTM_1, STRUCT_0, PROB_1, RCOMP_1, PCOMPS_1, NFCONT_1, CFCONT_1, FCONT_1, RLVECT_1, PARTFUN1, ZFMISC_1, CARD_3, SUPINF_2, PBOOLE, TOPS_1;
notations HIDDEN, TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, XCMPLX_0, PRE_TOPC, TOPS_1, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, CARD_3, NUMBERS, XREAL_0, RINFSUP1, XXREAL_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, XXREAL_2, RLVECT_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_0, NORMSP_1, NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2;
definitions TARSKI, RSSPACE3, XXREAL_2;
theorems TARSKI, XBOOLE_1, SEQ_1, SEQ_2, RLVECT_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_1, NORMSP_1, TBSP_1, PRE_TOPC, TOPS_1, NFCONT_1, XXREAL_0, FUNCT_1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, SEQM_3, INTEGRA2, SEQ_4, RSSPACE2, LOPBAN_1, LOPBAN_3, PROB_1, RSSPACE3, NAT_1, RELSET_1, VECTSP_1, NORMSP_0, XXREAL_2, ORDINAL1;
schemes FUNCT_2, FRAENKEL;
registrations NUMBERS, XREAL_0, XBOOLE_0, ORDINAL1, RELSET_1, STRUCT_0, MEMBERED, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1, VALUED_0, VALUED_1, SEQ_2, NORMSP_0;
constructors HIDDEN, REAL_1, COMPLEX1, TOPS_1, TBSP_1, NFCONT_1, RINFSUP1, INTEGRA2, PROB_1, NORMSP_2, RSSPACE3, LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, PCOMPS_1, COMSEQ_2, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, METRIC_1, PCOMPS_1, NORMSP_2, RSSPACE3, LOPBAN_1, RINFSUP1, CARD_3, XCMPLX_0, NORMSP_0;
expansions XXREAL_2;