for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for F, G being Functional_Sequence of X,ExtREAL
for K, L being ExtREAL_sequence st ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = A ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(F . n) . x <= (F . m) . x ) & ( for n being Nat holds
( G . n is_simple_func_in S & dom (G . n) = A ) ) & ( for n being Nat holds G . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(G . n) . x <= (G . m) . x ) & ( for x being Element of X st x in A holds
( F # x is convergent & G # x is convergent & lim (F # x) = lim (G # x) ) ) & ( for n being Nat holds
( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ) holds
( K is convergent & L is convergent & lim K = lim L )