theorem Th51: :: MESFUN9C:51

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,REAL
for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M