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