environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, RCOMP_1, XBOOLE_0, RELAT_1, TARSKI, SEQ_2, LIMFUNC1, FUNCT_1, XXREAL_0, ORDINAL2, CARD_1, PROB_1, XXREAL_1, ARYTM_1, ARYTM_3, COMPLEX1, FCONT_1, FUNCT_2, VALUED_0, SEQM_3, NAT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, PROB_1, REAL_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, LIMFUNC1, XXREAL_0, RFUNCT_2;
definitions TARSKI, RCOMP_1;
theorems FUNCT_1, NAT_1, SEQ_2, SEQ_4, ABSVALUE, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_2, FCONT_1, SUBSET_1, FCONT_2, TARSKI, FUNCT_2, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1, XXREAL_2, VALUED_0, ORDINAL1, SEQ_1;
schemes SEQ_1, FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RFUNCT_2, VALUED_1, FUNCT_2, VALUED_0, XXREAL_2, RELAT_1, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, REAL_1, COMPLEX1, NAT_1, SEQ_2, PROB_1, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, LIMFUNC1, VALUED_1, XXREAL_2, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RCOMP_1, XBOOLE_0, SUBSET_1, PROB_1, LIMFUNC1;
expansions TARSKI, RCOMP_1;