let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) implies integral+ (M,g) <= integral+ (M,f) )

assume that

A1: ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) and

A2: f is nonnegative and

A3: g is nonnegative and

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

g . x <= f . x ; :: thesis: integral+ (M,g) <= integral+ (M,f)

consider G being Functional_Sequence of X,ExtREAL, L being ExtREAL_sequence such that

A5: for n being Nat holds

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

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

A7: for n, m being Nat st n <= m holds

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

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

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

( G # x is convergent & lim (G # x) = g . x ) and

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

L is convergent and

A10: integral+ (M,g) = lim L by A1, A3, Def15;

consider F being Functional_Sequence of X,ExtREAL, K being ExtREAL_sequence such that

A11: for n being Nat holds

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

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

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

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

( F # x is convergent & lim (F # x) = f . x ) and

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

K is convergent and

A16: integral+ (M,f) = lim K by A1, A2, Def15;

consider A being Element of S such that

A17: A = dom f and

A18: A = dom g and

f is A -measurable and

g is A -measurable by A1;

A19: for x being Element of X st x in A holds

lim (G # x) = sup (rng (G # x))

( L is convergent & sup (rng L) = lim L )

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

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E being Element of S st

( E = dom f & E = dom g & f is E -measurable & g is E -measurable ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) implies integral+ (M,g) <= integral+ (M,f) )

assume that

A1: ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) and

A2: f is nonnegative and

A3: g is nonnegative and

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

g . x <= f . x ; :: thesis: integral+ (M,g) <= integral+ (M,f)

consider G being Functional_Sequence of X,ExtREAL, L being ExtREAL_sequence such that

A5: for n being Nat holds

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

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

A7: for n, m being Nat st n <= m holds

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

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

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

( G # x is convergent & lim (G # x) = g . x ) and

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

L is convergent and

A10: integral+ (M,g) = lim L by A1, A3, Def15;

consider F being Functional_Sequence of X,ExtREAL, K being ExtREAL_sequence such that

A11: for n being Nat holds

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

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

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

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

( F # x is convergent & lim (F # x) = f . x ) and

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

K is convergent and

A16: integral+ (M,f) = lim K by A1, A2, Def15;

consider A being Element of S such that

A17: A = dom f and

A18: A = dom g and

f is A -measurable and

g is A -measurable by A1;

A19: for x being Element of X st x in A holds

lim (G # x) = sup (rng (G # x))

proof

A23:
for n0 being Nat holds
let x be Element of X; :: thesis: ( x in A implies lim (G # x) = sup (rng (G # x)) )

assume A20: x in A ; :: thesis: lim (G # x) = sup (rng (G # x))

end;assume A20: x in A ; :: thesis: lim (G # x) = sup (rng (G # x))

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

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

hence
lim (G # x) = sup (rng (G # x))
by Th54; :: thesis: verum(G # x) . n <= (G # x) . m

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

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

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

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

hence (G # x) . n <= (G # x) . m by A18, A7, A20, A21, A22; :: thesis: verum

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

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

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

hence (G # x) . n <= (G # x) . m by A18, A7, A20, A21, A22; :: thesis: verum

( L is convergent & sup (rng L) = lim L )

proof

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

set ff = G . n0;

A24: dom (G . n0) = A by A18, A5;

A25: for x being Element of X st x in dom (G . n0) holds

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

then consider FF being ExtREAL_sequence such that

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

A29: FF is convergent and

A30: sup (rng FF) = lim FF and

integral' (M,(G . n0)) <= lim FF by A18, A5, A6, A7, A24, A25, Th75;

hence ( L is convergent & sup (rng L) = lim L ) by A29, A30; :: thesis: verum

end;set ff = G . n0;

A24: dom (G . n0) = A by A18, A5;

A25: for x being Element of X st x in dom (G . n0) holds

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

proof

G . n0 is_simple_func_in S
by A5;
let x be Element of X; :: thesis: ( x in dom (G . n0) implies ( G # x is convergent & (G . n0) . x <= lim (G # x) ) )

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

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

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

hence ( G # x is convergent & (G . n0) . x <= lim (G # x) ) by A18, A8, A19, A24, A26, A27; :: thesis: verum

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

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

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

hence ( G # x is convergent & (G . n0) . x <= lim (G # x) ) by A18, A8, A19, A24, A26, A27; :: thesis: verum

then consider FF being ExtREAL_sequence such that

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

A29: FF is convergent and

A30: sup (rng FF) = lim FF and

integral' (M,(G . n0)) <= lim FF by A18, A5, A6, A7, A24, A25, 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

thus FF . n = integral' (M,(G . n)) by A28

.= L . n by A9 ; :: thesis: verum

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

.= L . n by A9 ; :: thesis: verum

hence ( L is convergent & sup (rng L) = lim L ) by A29, A30; :: thesis: verum

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

proof

hence
integral+ (M,g) <= integral+ (M,f)
by A16, A10, A23, Th57; :: thesis: verum
let n0 be Nat; :: thesis: ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )

set gg = G . n0;

A31: G . n0 is nonnegative by A6;

A32: dom (G . n0) = A by A18, A5;

A33: for x being Element of X st x in dom (G . n0) holds

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

then consider GG being ExtREAL_sequence such that

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

A38: GG is convergent and

A39: sup (rng GG) = lim GG and

A40: integral' (M,(G . n0)) <= lim GG by A17, A11, A12, A13, A32, A31, A33, Th75;

hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A9, A38, A39, A40; :: thesis: verum

end;set gg = G . n0;

A31: G . n0 is nonnegative by A6;

A32: dom (G . n0) = A by A18, A5;

A33: for x being Element of X st x in dom (G . n0) holds

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

proof

G . n0 is_simple_func_in S
by A5;
let x be Element of X; :: thesis: ( x in dom (G . n0) implies ( F # x is convergent & (G . n0) . x <= lim (F # x) ) )

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

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

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

then (G . n0) . x <= lim (G # x) by A19, A32, A34, A35;

then A36: (G . n0) . x <= g . x by A18, A8, A32, A34;

g . x <= f . x by A1, A4, A17, A32, A34;

then g . x <= lim (F # x) by A17, A14, A32, A34;

hence ( F # x is convergent & (G . n0) . x <= lim (F # x) ) by A17, A14, A32, A34, A36, XXREAL_0:2; :: thesis: verum

end;assume A34: x in dom (G . n0) ; :: thesis: ( F # x is convergent & (G . n0) . x <= lim (F # x) )

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

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

then (G . n0) . x <= lim (G # x) by A19, A32, A34, A35;

then A36: (G . n0) . x <= g . x by A18, A8, A32, A34;

g . x <= f . x by A1, A4, A17, A32, A34;

then g . x <= lim (F # x) by A17, A14, A32, A34;

hence ( F # x is convergent & (G . n0) . x <= lim (F # x) ) by A17, A14, A32, A34, A36, XXREAL_0:2; :: thesis: verum

then consider GG being ExtREAL_sequence such that

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

A38: GG is convergent and

A39: sup (rng GG) = lim GG and

A40: integral' (M,(G . n0)) <= lim GG by A17, A11, A12, A13, A32, A31, A33, 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 A37;

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

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

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

hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A9, A38, A39, A40; :: thesis: verum