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