environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, FUNCT_1, SUBSET_1, XXREAL_0, ARYTM_3, RELAT_1, SETFAM_1, TARSKI, MEASURE2, ARYTM_1, SETLIM_1, NAT_1, ORDINAL2, CARD_3, CARD_1, SEQ_2, SEQFUNC, PARTFUN1, PBOOLE, RINFSUP1, MESFUNC1, XXREAL_2, ZFMISC_1, MESFUNC5, VALUED_0, COMPLEX1, REAL_1, SUPINF_2, SEQ_1, FUNCOP_1, VALUED_1, PREPOWER, NEWTON, SERIES_1, MESFUNC8, SEQ_4, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, VALUED_0, PROB_1, REAL_1, SETFAM_1, MEASURE1, KURATO_0, SETLIM_1, MEASURE2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_3, FUNCT_2, SUPINF_2, RINFSUP1, SEQFUNC, MEASURE6, VALUED_1, NAT_1, SEQ_1, SEQ_2, SEQ_4, NEWTON, PREPOWER, SERIES_1, EXTREAL1, MESFUNC1, MESFUNC5, RINFSUP2, CARD_3, FUNCOP_1;
definitions TARSKI, XXREAL_2;
theorems ABSVALUE, MEASURE1, MEASURE2, MEASURE3, NAT_1, TARSKI, PARTFUN1, FUNCT_1, FUNCT_2, KURATO_0, SUPINF_2, EXTREAL1, SETFAM_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SERIES_1, RINFSUP1, MESFUNC1, XREAL_0, PROB_1, XBOOLE_0, XBOOLE_1, MESFUNC2, XREAL_1, PREPOWER, XXREAL_0, ZFMISC_1, SETLIM_1, PROB_4, PARTFUN2, ORDINAL1, MESFUNC5, RINFSUP2, XXREAL_2, VALUED_0, FUNCOP_1, XXREAL_3, RELAT_1;
schemes FUNCT_2, SEQFUNC, PARTFUN2;
registrations SUBSET_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, FUNCT_2, RELAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, NUMBERS, VALUED_0, VALUED_1, SETLIM_1, SEQ_4, NAT_1, XXREAL_3, RELSET_1, NEWTON, SEQ_2;
constructors HIDDEN, REAL_1, NAT_1, EXTREAL1, NEWTON, PREPOWER, SERIES_1, MESFUNC1, PROB_2, MEASURE6, MEASURE3, PARTFUN3, KURATO_0, RINFSUP1, SETLIM_1, MESFUNC5, RINFSUP2, SUPINF_1, SEQFUNC, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities CARD_3, FUNCT_6, RINFSUP1, SETLIM_1, XCMPLX_0, RINFSUP2, VALUED_1, XXREAL_3;
expansions TARSKI, CARD_3, RINFSUP1, XXREAL_2;
reconsider jj = 1 as Real ;