environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, SUBSET_1, SEQFUNC, SEQ_1, PARTFUN1, NAT_1, REALSET1, FUNCT_1, RELAT_1, PBOOLE, SEQ_2, MEASURE6, MESFUNC5, MESFUNC8, TARSKI, CARD_1, ORDINAL2, MESFUNC1, SERIES_1, ARYTM_3, XXREAL_0, MSSUBFAM, SETFAM_1, CARD_3, MESFUNC2, INTEGRA5, COMPLEX1, COMSEQ_1, XCMPLX_0, VALUED_1, ARYTM_1, RINFSUP1, XXREAL_2, SUPINF_2, VALUED_0, MESFUN10, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, RELAT_1, VALUED_1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, NAT_1, PROB_1, SETFAM_1, SUPINF_2, MESFUNC9, SEQ_1, SEQ_2, SEQFUNC, SERIES_1, MEASURE1, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2, MESFUNC6, MESFUN6C, MESFUN10, MESFUNC8, MESFUN7C, MESFUNC5, COMSEQ_1, COMSEQ_2, COMSEQ_3, RINFSUP2, XXREAL_2;
definitions FUNCT_2, MESFUNC8;
theorems TARSKI, PARTFUN1, FUNCT_1, EXTREAL1, MESFUNC1, XBOOLE_0, MESFUNC2, XXREAL_0, MESFUNC5, NAT_1, RELAT_1, FUNCT_2, COMPLEX1, MESFUN10, XCMPLX_0, MESFUNC6, SEQFUNC, ORDINAL1, MESFUNC8, RINFSUP2, RELSET_1, MESFUN7C, SERIES_1, VALUED_1, COMSEQ_3, MESFUN6C, XXREAL_2, MESFUNC9;
schemes FUNCT_2, NAT_1, RECDEF_1, SEQFUNC;
registrations XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, COMSEQ_3, FUNCT_2, XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0, MESFUNC8, VALUED_0, MESFUN7C, RELSET_1, XXREAL_3, NAT_1;
constructors HIDDEN, REAL_1, EXTREAL1, SUPINF_1, MESFUNC9, MESFUN10, SEQFUNC, COMSEQ_2, COMSEQ_3, MESFUNC1, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, MESFUN6C, MESFUN7C, RINFSUP2, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities MESFUNC5, SERIES_1, VALUED_1, RINFSUP2, MESFUN7C, MESFUNC6;
expansions FUNCT_2, MESFUNC5, SERIES_1, MESFUN7C, MESFUNC6, MESFUNC8;
Lm1:
for X being non empty set
for D being set
for F being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )
Lm2:
for X being non empty set
for S being SigmaField of X
for E being Element of S
for m being Nat
for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is_measurable_on E ) holds
( (Re F) . m is_measurable_on E & (Im F) . m is_measurable_on E )