let X be non empty set ; :: thesis: 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 )

let S be SigmaField of X; :: thesis: 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 )

let M be sigma_Measure of S; :: thesis: 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 )

let A be Element of S; :: thesis: 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 )

let F, G be Functional_Sequence of X,ExtREAL; :: thesis: 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 )

let K, L be ExtREAL_sequence; :: thesis: ( ( 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)) ) ) implies ( K is convergent & L is convergent & lim K = lim L ) )

assume that

A1: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = A ) and

A2: for n being Nat holds F . n is nonnegative and

A3: 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 and

A4: for n being Nat holds

( G . n is_simple_func_in S & dom (G . n) = A ) and

A5: for n being Nat holds G . n is nonnegative and

A6: 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 and

A7: 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) ) and

A8: for n being Nat holds

( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ; :: thesis: ( K is convergent & L is convergent & lim K = lim L )

A9: for n0 being Nat holds

( L is convergent & sup (rng L) = lim L & K . n0 <= lim L )

( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )

A35: lim K <= lim L by A22, A9, Th57;

lim L <= lim K by A22, A9, Th57;

hence lim K = lim L by A35, XXREAL_0:1; :: thesis: verum

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 )

let S be SigmaField of X; :: thesis: 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 )

let M be sigma_Measure of S; :: thesis: 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 )

let A be Element of S; :: thesis: 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 )

let F, G be Functional_Sequence of X,ExtREAL; :: thesis: 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 )

let K, L be ExtREAL_sequence; :: thesis: ( ( 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)) ) ) implies ( K is convergent & L is convergent & lim K = lim L ) )

assume that

A1: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = A ) and

A2: for n being Nat holds F . n is nonnegative and

A3: 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 and

A4: for n being Nat holds

( G . n is_simple_func_in S & dom (G . n) = A ) and

A5: for n being Nat holds G . n is nonnegative and

A6: 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 and

A7: 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) ) and

A8: for n being Nat holds

( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ; :: thesis: ( K is convergent & L is convergent & lim K = lim L )

A9: for n0 being Nat holds

( L is convergent & sup (rng L) = lim L & K . n0 <= lim L )

proof

A22:
for n0 being Nat holds
let n0 be Nat; :: thesis: ( L is convergent & sup (rng L) = lim L & K . n0 <= lim L )

reconsider f = F . n0 as PartFunc of X,ExtREAL ;

A10: f is_simple_func_in S by A1;

A11: f is nonnegative by A2;

A12: for x being Element of X st x in dom f holds

( G # x is convergent & f . x <= lim (G # x) )

then consider FF being ExtREAL_sequence such that

A18: for n being Nat holds FF . n = integral' (M,(G . n)) and

A19: FF is convergent and

A20: sup (rng FF) = lim FF and

A21: integral' (M,f) <= lim FF by A4, A5, A6, A12, A10, A11, Th75;

hence ( L is convergent & sup (rng L) = lim L & K . n0 <= lim L ) by A8, A19, A20, A21; :: thesis: verum

end;reconsider f = F . n0 as PartFunc of X,ExtREAL ;

A10: f is_simple_func_in S by A1;

A11: f is nonnegative by A2;

A12: for x being Element of X st x in dom f holds

( G # x is convergent & f . x <= lim (G # x) )

proof

dom f = A
by A1;
let x be Element of X; :: thesis: ( x in dom f implies ( G # x is convergent & f . x <= lim (G # x) ) )

A13: (F # x) . n0 <= sup (rng (F # x)) by Th56;

assume x in dom f ; :: thesis: ( G # x is convergent & f . x <= lim (G # x) )

then A14: x in A by A1;

f . x = (F # x) . n0 by Def13;

hence ( G # x is convergent & f . x <= lim (G # x) ) by A7, A14, A17, A13; :: thesis: verum

end;A13: (F # x) . n0 <= sup (rng (F # x)) by Th56;

assume x in dom f ; :: thesis: ( G # x is convergent & f . x <= lim (G # x) )

then A14: x in A by A1;

now :: thesis: for n, m being Nat st n <= m holds

(F # x) . n <= (F # x) . m

then A17:
lim (F # x) = sup (rng (F # x))
by Th54;(F # x) . n <= (F # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F # x) . n <= (F # x) . m )

assume A15: n <= m ; :: thesis: (F # x) . n <= (F # x) . m

A16: (F # x) . m = (F . m) . x by Def13;

(F # x) . n = (F . n) . x by Def13;

hence (F # x) . n <= (F # x) . m by A3, A14, A15, A16; :: thesis: verum

end;assume A15: n <= m ; :: thesis: (F # x) . n <= (F # x) . m

A16: (F # x) . m = (F . m) . x by Def13;

(F # x) . n = (F . n) . x by Def13;

hence (F # x) . n <= (F # x) . m by A3, A14, A15, A16; :: thesis: verum

f . x = (F # x) . n0 by Def13;

hence ( G # x is convergent & f . x <= lim (G # x) ) by A7, A14, A17, A13; :: thesis: verum

then consider FF being ExtREAL_sequence such that

A18: for n being Nat holds FF . n = integral' (M,(G . n)) and

A19: FF is convergent and

A20: sup (rng FF) = lim FF and

A21: integral' (M,f) <= lim FF by A4, A5, A6, A12, A10, A11, Th75;

now :: thesis: for n being Element of NAT holds FF . n = L . n

then
FF = L
by FUNCT_2:63;let n be Element of NAT ; :: thesis: FF . n = L . n

FF . n = integral' (M,(G . n)) by A18;

hence FF . n = L . n by A8; :: thesis: verum

end;FF . n = integral' (M,(G . n)) by A18;

hence FF . n = L . n by A8; :: thesis: verum

hence ( L is convergent & sup (rng L) = lim L & K . n0 <= lim L ) by A8, A19, A20, A21; :: thesis: verum

( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )

proof

hence
( K is convergent & L is convergent )
by A9; :: thesis: lim K = lim L
let n0 be Nat; :: thesis: ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )

reconsider g = G . n0 as PartFunc of X,ExtREAL ;

A23: g is_simple_func_in S by A4;

A24: g is nonnegative by A5;

A25: for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) )

then consider GG being ExtREAL_sequence such that

A31: for n being Nat holds GG . n = integral' (M,(F . n)) and

A32: GG is convergent and

A33: sup (rng GG) = lim GG and

A34: integral' (M,g) <= lim GG by A1, A2, A3, A25, A23, A24, Th75;

hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A8, A32, A33, A34; :: thesis: verum

end;reconsider g = G . n0 as PartFunc of X,ExtREAL ;

A23: g is_simple_func_in S by A4;

A24: g is nonnegative by A5;

A25: for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) )

proof

dom g = A
by A4;
let x be Element of X; :: thesis: ( x in dom g implies ( F # x is convergent & g . x <= lim (F # x) ) )

A26: (G # x) . n0 <= sup (rng (G # x)) by Th56;

assume x in dom g ; :: thesis: ( F # x is convergent & g . x <= lim (F # x) )

then A27: x in A by A4;

g . x = (G # x) . n0 by Def13;

hence ( F # x is convergent & g . x <= lim (F # x) ) by A7, A27, A30, A26; :: thesis: verum

end;A26: (G # x) . n0 <= sup (rng (G # x)) by Th56;

assume x in dom g ; :: thesis: ( F # x is convergent & g . x <= lim (F # x) )

then A27: x in A by A4;

now :: thesis: for n, m being Nat st n <= m holds

(G # x) . n <= (G # x) . m

then A30:
lim (G # x) = sup (rng (G # x))
by Th54;(G # x) . n <= (G # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (G # x) . n <= (G # x) . m )

assume A28: n <= m ; :: thesis: (G # x) . n <= (G # x) . m

A29: (G # x) . m = (G . m) . x by Def13;

(G # x) . n = (G . n) . x by Def13;

hence (G # x) . n <= (G # x) . m by A6, A27, A28, A29; :: thesis: verum

end;assume A28: n <= m ; :: thesis: (G # x) . n <= (G # x) . m

A29: (G # x) . m = (G . m) . x by Def13;

(G # x) . n = (G . n) . x by Def13;

hence (G # x) . n <= (G # x) . m by A6, A27, A28, A29; :: thesis: verum

g . x = (G # x) . n0 by Def13;

hence ( F # x is convergent & g . x <= lim (F # x) ) by A7, A27, A30, A26; :: thesis: verum

then consider GG being ExtREAL_sequence such that

A31: for n being Nat holds GG . n = integral' (M,(F . n)) and

A32: GG is convergent and

A33: sup (rng GG) = lim GG and

A34: integral' (M,g) <= lim GG by A1, A2, A3, A25, A23, A24, Th75;

now :: thesis: for n being Element of NAT holds GG . n = K . n

then
GG = K
by FUNCT_2:63;let n be Element of NAT ; :: thesis: GG . n = K . n

GG . n = integral' (M,(F . n)) by A31;

hence GG . n = K . n by A8; :: thesis: verum

end;GG . n = integral' (M,(F . n)) by A31;

hence GG . n = K . n by A8; :: thesis: verum

hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A8, A32, A33, A34; :: thesis: verum

A35: lim K <= lim L by A22, A9, Th57;

lim L <= lim K by A22, A9, Th57;

hence lim K = lim L by A35, XXREAL_0:1; :: thesis: verum