let s1, s2 be Element of ExtREAL ; :: thesis: ( ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( 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 dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & s1 = lim K ) & ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( 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 dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & s2 = lim K ) implies s1 = s2 )
assume that
A16: ex F1 being Functional_Sequence of X,ExtREAL ex K1 being ExtREAL_sequence st
( ( for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) ) & ( for n being Nat holds F1 . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F1 . n) . x <= (F1 . m) . x ) & ( for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) ) & ( for n being Nat holds K1 . n = integral' (M,(F1 . n)) ) & K1 is convergent & s1 = lim K1 ) and
A17: ex F2 being Functional_Sequence of X,ExtREAL ex K2 being ExtREAL_sequence st
( ( for n being Nat holds
( F2 . n is_simple_func_in S & dom (F2 . n) = dom f ) ) & ( for n being Nat holds F2 . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F2 . n) . x <= (F2 . m) . x ) & ( for x being Element of X st x in dom f holds
( F2 # x is convergent & lim (F2 # x) = f . x ) ) & ( for n being Nat holds K2 . n = integral' (M,(F2 . n)) ) & K2 is convergent & s2 = lim K2 ) ; :: thesis: s1 = s2
consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that
A18: for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and
A19: for n being Nat holds F1 . n is nonnegative and
A20: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F1 . n) . x <= (F1 . m) . x and
A21: for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) and
A22: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and
K1 is convergent and
A23: s1 = lim K1 by A16;
consider F2 being Functional_Sequence of X,ExtREAL, K2 being ExtREAL_sequence such that
A24: for n being Nat holds
( F2 . n is_simple_func_in S & dom (F2 . n) = dom f ) and
A25: for n being Nat holds F2 . n is nonnegative and
A26: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F2 . n) . x <= (F2 . m) . x and
A27: for x being Element of X st x in dom f holds
( F2 # x is convergent & lim (F2 # x) = f . x ) and
A28: for n being Nat holds K2 . n = integral' (M,(F2 . n)) and
K2 is convergent and
A29: s2 = lim K2 by A17;
for x being Element of X st x in dom f holds
( F1 # x is convergent & F2 # x is convergent & lim (F1 # x) = lim (F2 # x) )

proof

let x be Element of X; :: thesis: ( x in dom f implies ( F1 # x is convergent & F2 # x is convergent & lim (F1 # x) = lim (F2 # x) ) )
assume A30: x in dom f ; :: thesis: ( F1 # x is convergent & F2 # x is convergent & lim (F1 # x) = lim (F2 # x) )
then lim (F1 # x) = f . x by A21
.= lim (F2 # x) by A27, A30 ;
hence ( F1 # x is convergent & F2 # x is convergent & lim (F1 # x) = lim (F2 # x) ) by A21, A27, A30; :: thesis: verum

end;

hence s1 = s2 by A1, A18, A19, A20, A22, A23, A24, A25, A26, A28, A29, Th76; :: thesis: verum