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) )

( ( 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

hence
s1 = s2
by A1, A18, A19, A20, A22, A23, A24, A25, A26, A28, A29, Th76; :: thesis: verum
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;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