let s1, s2 be Element of ExtREAL ; ( 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 )
; 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) )
hence
s1 = s2
by A1, A18, A19, A20, A22, A23, A24, A25, A26, A28, A29, Th76; verum