environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, REAL_1, SUBSET_1, SEQFUNC, MEASURE6, RELAT_1, FUNCT_1, PBOOLE, TARSKI, SEQ_1, ORDINAL2, RINFSUP1, MESFUNC8, CARD_1, NAT_1, MESFUNC1, ARYTM_3, SEQ_2, XXREAL_0, XXREAL_2, SETFAM_1, COMSEQ_1, COMPLEX1, VALUED_1, SUPINF_2, POWER, ARYTM_1, MESFUNC5, INTEGRA5, MESFUNC2, FINSEQ_1, MESFUNC3, INT_1, ZFMISC_1, XCMPLX_0, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0, COMPLEX1, XXREAL_0, XREAL_0, XXREAL_2, REAL_1, NAT_1, NAT_D, PROB_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, RFUNCT_3, VALUED_1, FUNCT_2, SETFAM_1, SUPINF_1, SUPINF_2, SEQ_1, SEQ_2, SEQFUNC, COMSEQ_1, COMSEQ_2, RINFSUP1, RINFSUP2, MEASURE1, MEASURE6, EXTREAL1, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, COMSEQ_3, MESFUN6C, MESFUNC8, SEQ_4, COMPLSP2;
definitions TARSKI, XBOOLE_0;
theorems MEASURE1, TARSKI, PARTFUN1, FUNCT_1, MESFUNC1, NAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_1, MESFUNC5, XXREAL_0, VALUED_1, MESFUNC6, COMPLEX1, RELAT_1, SQUARE_1, FINSEQ_1, MESFUN6C, ORDINAL1, FUNCT_2, SEQFUNC, SETFAM_1, RINFSUP1, MESFUNC7, MESFUNC8, COMSEQ_3, MESFUNC3, NUMBERS, RINFSUP2, XXREAL_2, COMPLSP2, NAT_D, FINSEQ_2, NAT_2, FINSEQ_3, RELSET_1, XXREAL_3, XREAL_0;
schemes FUNCT_2, PARTFUN2, FINSEQ_1;
registrations NAT_1, MESFUNC8, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, XCMPLX_0, PARTFUN1, FUNCT_2, RELAT_1, SEQ_2, COMSEQ_3, RELSET_1, XXREAL_3;
constructors HIDDEN, REAL_1, SQUARE_1, MEASURE6, EXTREAL1, MESFUNC2, MESFUNC3, MESFUNC5, MESFUNC6, MESFUN6C, BINOP_2, RINFSUP1, MESFUNC8, COMSEQ_2, COMSEQ_3, SUPINF_1, RINFSUP2, SEQFUNC, MESFUNC1, COMPLSP2, MATRIX_5, NAT_D, RELSET_1, SEQ_4;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MESFUNC5, COMPLEX1, RINFSUP2, XBOOLE_0, FINSEQ_1, COMPLSP2;
expansions MESFUNC5, COMPLEX1, TARSKI, XBOOLE_0;
Lm1:
for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative