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

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

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

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let f be PartFunc of X,ExtREAL; :: thesis: for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let F be Finite_Sep_Sequence of S; :: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) implies Integral (M,f) = Sum x )

assume that

A1: f is_simple_func_in S and

A2: E = dom f and

A3: M . E < +infty and

A4: F,a are_Re-presentation_of f and

A5: dom x = dom F and

A6: for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ; :: thesis: Integral (M,f) = Sum x

A7: ( max+ f is_simple_func_in S & max- f is_simple_func_in S ) by A1, Th4;

A8: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

defpred S_{1}[ Nat, ExtReal] means for x being object st x in F . $1 holds

$2 = max ((f . x),0);

A9: dom a = dom F by A4, MESFUNC3:def 1;

( dom (max+ f) = dom f & dom (max- f) = dom f ) by MESFUNC2:def 2, MESFUNC2:def 3;

then A10: ( dom (max+ f) = union (rng F) & dom (max- f) = union (rng F) ) by A4, MESFUNC3:def 1;

A11: for k being Nat st k in Seg (len a) holds

ex y being Element of ExtREAL st S_{1}[k,y]

A17: dom a1 = Seg (len a) and

A18: for k being Nat st k in Seg (len a) holds

S_{1}[k,a1 . k]
from FINSEQ_1:sch 5(A11);

A19: dom a1 = dom a by A17, FINSEQ_1:def 3;

A20: for k being Nat st k in dom F holds

for x being object st x in F . k holds

(max+ f) . x = a1 . k

defpred S_{2}[ Nat, ExtReal] means $2 = (a1 . $1) * ((M * F) . $1);

A25: for k being Nat st k in Seg (len F) holds

ex y being Element of ExtREAL st S_{2}[k,y]
;

consider x1 being FinSequence of ExtREAL such that

A26: ( dom x1 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S_{2}[k,x1 . k] ) )
from FINSEQ_1:sch 5(A25);

A27: dom x1 = dom F by A26, FINSEQ_1:def 3;

A28: dom F = Seg (len F) by FINSEQ_1:def 3;

then reconsider rx1 = x1 as FinSequence of REAL by FINSEQ_1:def 4;

A32: Sum rx1 = Sum x1 by MESFUNC3:2;

integral' (M,(max+ f)) = Sum x1

defpred S_{3}[ Nat, ExtReal] means for x being object st x in F . $1 holds

$2 = max ((- (f . x)),0);

A37: for k being Nat st k in Seg (len a) holds

ex y being Element of ExtREAL st S_{3}[k,y]

A43: dom a2 = Seg (len a) and

A44: for k being Nat st k in Seg (len a) holds

S_{3}[k,a2 . k]
from FINSEQ_1:sch 5(A37);

A45: dom a2 = dom a by A43, FINSEQ_1:def 3;

A46: for k being Nat st k in dom F holds

for x being object st x in F . k holds

(max- f) . x = a2 . k

defpred S_{4}[ Nat, ExtReal] means $2 = (a2 . $1) * ((M * F) . $1);

A51: for k being Nat st k in Seg (len F) holds

ex y being Element of ExtREAL st S_{4}[k,y]
;

consider x2 being FinSequence of ExtREAL such that

A52: ( dom x2 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S_{4}[k,x2 . k] ) )
from FINSEQ_1:sch 5(A51);

A53: dom x2 = dom F by A52, FINSEQ_1:def 3;

A54: dom F = Seg (len F) by FINSEQ_1:def 3;

then reconsider rx2 = x2 as FinSequence of REAL by FINSEQ_1:def 4;

A58: Sum rx2 = Sum x2 by MESFUNC3:2;

integral' (M,(max- f)) = Sum x2

A63: ( len rx1 = len F & len rx2 = len F ) by A26, A52, FINSEQ_1:def 3;

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by A1, A2, MESFUNC2:34, MESFUN11:54;

then Integral (M,f) = (Sum rx1) - (Sum rx2) by A36, A62, Lm1;

then A64: Integral (M,f) = Sum (rx1 - rx2) by A63, INTEGRA5:2;

len (rx1 - rx2) = len rx1 by A63, INTEGRA5:2;

then A65: dom (rx1 - rx2) = dom x by A5, A27, FINSEQ_3:29;

for k being object st k in dom x holds

x . k = (rx1 - rx2) . k

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

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

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let f be PartFunc of X,ExtREAL; :: thesis: for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let F be Finite_Sep_Sequence of S; :: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) implies Integral (M,f) = Sum x )

assume that

A1: f is_simple_func_in S and

A2: E = dom f and

A3: M . E < +infty and

A4: F,a are_Re-presentation_of f and

A5: dom x = dom F and

A6: for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ; :: thesis: Integral (M,f) = Sum x

A7: ( max+ f is_simple_func_in S & max- f is_simple_func_in S ) by A1, Th4;

A8: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;

defpred S

$2 = max ((f . x),0);

A9: dom a = dom F by A4, MESFUNC3:def 1;

( dom (max+ f) = dom f & dom (max- f) = dom f ) by MESFUNC2:def 2, MESFUNC2:def 3;

then A10: ( dom (max+ f) = union (rng F) & dom (max- f) = union (rng F) ) by A4, MESFUNC3:def 1;

A11: for k being Nat st k in Seg (len a) holds

ex y being Element of ExtREAL st S

proof

consider a1 being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len a) implies ex y being Element of ExtREAL st S_{1}[k,y] )

assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S_{1}[k,y]

then A12: k in dom a by FINSEQ_1:def 3;

end;assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S

then A12: k in dom a by FINSEQ_1:def 3;

per cases
( F . k = {} or F . k <> {} )
;

end;

suppose A13:
F . k = {}
; :: thesis: ex y being Element of ExtREAL st S_{1}[k,y]

A14:
0 is Element of ExtREAL
by XXREAL_0:def 1;

for x being object st x in F . k holds

0 = max ((f . x),0) by A13;

hence ex y being Element of ExtREAL st S_{1}[k,y]
by A14; :: thesis: verum

end;for x being object st x in F . k holds

0 = max ((f . x),0) by A13;

hence ex y being Element of ExtREAL st S

suppose
F . k <> {}
; :: thesis: ex y being Element of ExtREAL st S_{1}[k,y]

then consider p being object such that

A15: p in F . k by XBOOLE_0:def 1;

A16: max ((f . p),0) is Element of ExtREAL by XXREAL_0:def 1;

for x being object st x in F . k holds

max ((f . p),0) = max ((f . x),0)_{1}[k,y]
by A16; :: thesis: verum

end;A15: p in F . k by XBOOLE_0:def 1;

A16: max ((f . p),0) is Element of ExtREAL by XXREAL_0:def 1;

for x being object st x in F . k holds

max ((f . p),0) = max ((f . x),0)

proof

hence
ex y being Element of ExtREAL st S
let x be object ; :: thesis: ( x in F . k implies max ((f . p),0) = max ((f . x),0) )

assume x in F . k ; :: thesis: max ((f . p),0) = max ((f . x),0)

then ( f . x = a . k & f . p = a . k ) by A4, A15, A9, A12, MESFUNC3:def 1;

hence max ((f . p),0) = max ((f . x),0) ; :: thesis: verum

end;assume x in F . k ; :: thesis: max ((f . p),0) = max ((f . x),0)

then ( f . x = a . k & f . p = a . k ) by A4, A15, A9, A12, MESFUNC3:def 1;

hence max ((f . p),0) = max ((f . x),0) ; :: thesis: verum

A17: dom a1 = Seg (len a) and

A18: for k being Nat st k in Seg (len a) holds

S

A19: dom a1 = dom a by A17, FINSEQ_1:def 3;

A20: for k being Nat st k in dom F holds

for x being object st x in F . k holds

(max+ f) . x = a1 . k

proof

then A24:
F,a1 are_Re-presentation_of max+ f
by A10, A9, A19, MESFUNC3:def 1;
let k be Nat; :: thesis: ( k in dom F implies for x being object st x in F . k holds

(max+ f) . x = a1 . k )

assume A21: k in dom F ; :: thesis: for x being object st x in F . k holds

(max+ f) . x = a1 . k

let x be object ; :: thesis: ( x in F . k implies (max+ f) . x = a1 . k )

assume A22: x in F . k ; :: thesis: (max+ f) . x = a1 . k

F . k in rng F by A21, FUNCT_1:3;

then x in union (rng F) by A22, TARSKI:def 4;

then x in dom f by A4, MESFUNC3:def 1;

then A23: x in dom (max+ f) by MESFUNC2:def 2;

a1 . k = max ((f . x),0) by A22, A21, A9, A19, A17, A18;

hence (max+ f) . x = a1 . k by A23, MESFUNC2:def 2; :: thesis: verum

end;(max+ f) . x = a1 . k )

assume A21: k in dom F ; :: thesis: for x being object st x in F . k holds

(max+ f) . x = a1 . k

let x be object ; :: thesis: ( x in F . k implies (max+ f) . x = a1 . k )

assume A22: x in F . k ; :: thesis: (max+ f) . x = a1 . k

F . k in rng F by A21, FUNCT_1:3;

then x in union (rng F) by A22, TARSKI:def 4;

then x in dom f by A4, MESFUNC3:def 1;

then A23: x in dom (max+ f) by MESFUNC2:def 2;

a1 . k = max ((f . x),0) by A22, A21, A9, A19, A17, A18;

hence (max+ f) . x = a1 . k by A23, MESFUNC2:def 2; :: thesis: verum

defpred S

A25: for k being Nat st k in Seg (len F) holds

ex y being Element of ExtREAL st S

consider x1 being FinSequence of ExtREAL such that

A26: ( dom x1 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S

A27: dom x1 = dom F by A26, FINSEQ_1:def 3;

A28: dom F = Seg (len F) by FINSEQ_1:def 3;

now :: thesis: for q being object st q in rng x1 holds

q in REAL

then
rng x1 c= REAL
;q in REAL

let q be object ; :: thesis: ( q in rng x1 implies b_{1} in REAL )

assume q in rng x1 ; :: thesis: b_{1} in REAL

then consider p being Element of NAT such that

A29: ( p in dom x1 & q = x1 . p ) by PARTFUN1:3;

A30: q = (a1 . p) * ((M * F) . p) by A26, A29;

end;assume q in rng x1 ; :: thesis: b

then consider p being Element of NAT such that

A29: ( p in dom x1 & q = x1 . p ) by PARTFUN1:3;

A30: q = (a1 . p) * ((M * F) . p) by A26, A29;

per cases
( a1 . p is Real or F . p = {} )
by A1, A24, A29, A27, Th4, Th12;

end;

suppose A31:
a1 . p is Real
; :: thesis: b_{1} in REAL

F . p c= union (rng F)
by A29, A27, FUNCT_1:3, ZFMISC_1:74;

then F . p c= E by A2, A4, MESFUNC3:def 1;

then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by SUPINF_2:51, MEASURE1:31;

then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by A29, A27, FUNCT_1:13;

then (M * F) . p in REAL by A3, XXREAL_0:14;

hence q in REAL by A30, A31, XREAL_0:def 1; :: thesis: verum

end;then F . p c= E by A2, A4, MESFUNC3:def 1;

then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by SUPINF_2:51, MEASURE1:31;

then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by A29, A27, FUNCT_1:13;

then (M * F) . p in REAL by A3, XXREAL_0:14;

hence q in REAL by A30, A31, XREAL_0:def 1; :: thesis: verum

then reconsider rx1 = x1 as FinSequence of REAL by FINSEQ_1:def 4;

A32: Sum rx1 = Sum x1 by MESFUNC3:2;

integral' (M,(max+ f)) = Sum x1

proof
end;

then A36:
Integral (M,(max+ f)) = Sum rx1
by A7, A8, A32, MESFUNC5:89;per cases
( dom (max+ f) = {} or dom (max+ f) <> {} )
;

end;

suppose A33:
dom (max+ f) = {}
; :: thesis: integral' (M,(max+ f)) = Sum x1

for k being Nat st k in dom x1 holds

x1 . k = 0

hence integral' (M,(max+ f)) = Sum x1 by A33, A32, MESFUNC5:def 14; :: thesis: verum

end;x1 . k = 0

proof

then
Sum rx1 = 0 * (len rx1)
by Lm2;
let k be Nat; :: thesis: ( k in dom x1 implies x1 . k = 0 )

assume A34: k in dom x1 ; :: thesis: x1 . k = 0

then F . k c= {} by A10, A27, A33, FUNCT_1:3, ZFMISC_1:74;

then F . k = {} ;

then M . (F . k) = 0 by VALUED_0:def 19;

then (M * F) . k = 0 by A27, A34, FUNCT_1:13;

then (a1 . k) * ((M * F) . k) = 0 ;

hence x1 . k = 0 by A26, A34; :: thesis: verum

end;assume A34: k in dom x1 ; :: thesis: x1 . k = 0

then F . k c= {} by A10, A27, A33, FUNCT_1:3, ZFMISC_1:74;

then F . k = {} ;

then M . (F . k) = 0 by VALUED_0:def 19;

then (M * F) . k = 0 by A27, A34, FUNCT_1:13;

then (a1 . k) * ((M * F) . k) = 0 ;

hence x1 . k = 0 by A26, A34; :: thesis: verum

hence integral' (M,(max+ f)) = Sum x1 by A33, A32, MESFUNC5:def 14; :: thesis: verum

defpred S

$2 = max ((- (f . x)),0);

A37: for k being Nat st k in Seg (len a) holds

ex y being Element of ExtREAL st S

proof

consider a2 being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg (len a) implies ex y being Element of ExtREAL st S_{3}[k,y] )

assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S_{3}[k,y]

then A38: k in dom a by FINSEQ_1:def 3;

end;assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S

then A38: k in dom a by FINSEQ_1:def 3;

per cases
( F . k = {} or F . k <> {} )
;

end;

suppose A39:
F . k = {}
; :: thesis: ex y being Element of ExtREAL st S_{3}[k,y]

A40:
0 is Element of ExtREAL
by XXREAL_0:def 1;

for x being object st x in F . k holds

0 = max ((- (f . x)),0) by A39;

hence ex y being Element of ExtREAL st S_{3}[k,y]
by A40; :: thesis: verum

end;for x being object st x in F . k holds

0 = max ((- (f . x)),0) by A39;

hence ex y being Element of ExtREAL st S

suppose
F . k <> {}
; :: thesis: ex y being Element of ExtREAL st S_{3}[k,y]

then consider p being object such that

A41: p in F . k by XBOOLE_0:def 1;

A42: max ((- (f . p)),0) is Element of ExtREAL by XXREAL_0:def 1;

for x being object st x in F . k holds

max ((- (f . p)),0) = max ((- (f . x)),0)_{3}[k,y]
by A42; :: thesis: verum

end;A41: p in F . k by XBOOLE_0:def 1;

A42: max ((- (f . p)),0) is Element of ExtREAL by XXREAL_0:def 1;

for x being object st x in F . k holds

max ((- (f . p)),0) = max ((- (f . x)),0)

proof

hence
ex y being Element of ExtREAL st S
let x be object ; :: thesis: ( x in F . k implies max ((- (f . p)),0) = max ((- (f . x)),0) )

assume x in F . k ; :: thesis: max ((- (f . p)),0) = max ((- (f . x)),0)

then ( f . x = a . k & f . p = a . k ) by A9, A38, A41, A4, MESFUNC3:def 1;

hence max ((- (f . p)),0) = max ((- (f . x)),0) ; :: thesis: verum

end;assume x in F . k ; :: thesis: max ((- (f . p)),0) = max ((- (f . x)),0)

then ( f . x = a . k & f . p = a . k ) by A9, A38, A41, A4, MESFUNC3:def 1;

hence max ((- (f . p)),0) = max ((- (f . x)),0) ; :: thesis: verum

A43: dom a2 = Seg (len a) and

A44: for k being Nat st k in Seg (len a) holds

S

A45: dom a2 = dom a by A43, FINSEQ_1:def 3;

A46: for k being Nat st k in dom F holds

for x being object st x in F . k holds

(max- f) . x = a2 . k

proof

A50:
F,a2 are_Re-presentation_of max- f
by A10, A9, A45, A46, MESFUNC3:def 1;
let k be Nat; :: thesis: ( k in dom F implies for x being object st x in F . k holds

(max- f) . x = a2 . k )

assume A47: k in dom F ; :: thesis: for x being object st x in F . k holds

(max- f) . x = a2 . k

let x be object ; :: thesis: ( x in F . k implies (max- f) . x = a2 . k )

assume A48: x in F . k ; :: thesis: (max- f) . x = a2 . k

F . k in rng F by A47, FUNCT_1:3;

then x in union (rng F) by A48, TARSKI:def 4;

then x in dom f by A4, MESFUNC3:def 1;

then A49: x in dom (max- f) by MESFUNC2:def 3;

a2 . k = max ((- (f . x)),0) by A48, A47, A9, A45, A43, A44;

hence (max- f) . x = a2 . k by A49, MESFUNC2:def 3; :: thesis: verum

end;(max- f) . x = a2 . k )

assume A47: k in dom F ; :: thesis: for x being object st x in F . k holds

(max- f) . x = a2 . k

let x be object ; :: thesis: ( x in F . k implies (max- f) . x = a2 . k )

assume A48: x in F . k ; :: thesis: (max- f) . x = a2 . k

F . k in rng F by A47, FUNCT_1:3;

then x in union (rng F) by A48, TARSKI:def 4;

then x in dom f by A4, MESFUNC3:def 1;

then A49: x in dom (max- f) by MESFUNC2:def 3;

a2 . k = max ((- (f . x)),0) by A48, A47, A9, A45, A43, A44;

hence (max- f) . x = a2 . k by A49, MESFUNC2:def 3; :: thesis: verum

defpred S

A51: for k being Nat st k in Seg (len F) holds

ex y being Element of ExtREAL st S

consider x2 being FinSequence of ExtREAL such that

A52: ( dom x2 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S

A53: dom x2 = dom F by A52, FINSEQ_1:def 3;

A54: dom F = Seg (len F) by FINSEQ_1:def 3;

now :: thesis: for q being object st q in rng x2 holds

q in REAL

then
rng x2 c= REAL
;q in REAL

let q be object ; :: thesis: ( q in rng x2 implies b_{1} in REAL )

assume q in rng x2 ; :: thesis: b_{1} in REAL

then consider p being Element of NAT such that

A55: ( p in dom x2 & q = x2 . p ) by PARTFUN1:3;

reconsider p = p as Nat ;

A56: q = (a2 . p) * ((M * F) . p) by A55, A52;

end;assume q in rng x2 ; :: thesis: b

then consider p being Element of NAT such that

A55: ( p in dom x2 & q = x2 . p ) by PARTFUN1:3;

reconsider p = p as Nat ;

A56: q = (a2 . p) * ((M * F) . p) by A55, A52;

per cases
( a2 . p is Real or F . p = {} )
by A1, A50, A55, A53, Th4, Th12;

end;

suppose A57:
a2 . p is Real
; :: thesis: b_{1} in REAL

F . p c= union (rng F)
by A55, A53, FUNCT_1:3, ZFMISC_1:74;

then F . p c= E by A2, A4, MESFUNC3:def 1;

then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by SUPINF_2:51, MEASURE1:31;

then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by A55, A53, FUNCT_1:13;

then (M * F) . p in REAL by A3, XXREAL_0:14;

hence q in REAL by A56, A57, XREAL_0:def 1; :: thesis: verum

end;then F . p c= E by A2, A4, MESFUNC3:def 1;

then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by SUPINF_2:51, MEASURE1:31;

then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by A55, A53, FUNCT_1:13;

then (M * F) . p in REAL by A3, XXREAL_0:14;

hence q in REAL by A56, A57, XREAL_0:def 1; :: thesis: verum

then reconsider rx2 = x2 as FinSequence of REAL by FINSEQ_1:def 4;

A58: Sum rx2 = Sum x2 by MESFUNC3:2;

integral' (M,(max- f)) = Sum x2

proof
end;

then A62:
Integral (M,(max- f)) = Sum rx2
by A7, A8, A58, MESFUNC5:89;per cases
( dom (max- f) = {} or dom (max- f) <> {} )
;

end;

suppose A59:
dom (max- f) = {}
; :: thesis: integral' (M,(max- f)) = Sum x2

for k being Nat st k in dom x2 holds

x2 . k = 0

hence integral' (M,(max- f)) = Sum x2 by A59, A58, MESFUNC5:def 14; :: thesis: verum

end;x2 . k = 0

proof

then
Sum rx2 = 0 * (len rx2)
by Lm2;
let k be Nat; :: thesis: ( k in dom x2 implies x2 . k = 0 )

assume A60: k in dom x2 ; :: thesis: x2 . k = 0

then F . k c= {} by A10, A59, A53, FUNCT_1:3, ZFMISC_1:74;

then F . k = {} ;

then M . (F . k) = 0 by VALUED_0:def 19;

then (M * F) . k = 0 by A53, A60, FUNCT_1:13;

then (a2 . k) * ((M * F) . k) = 0 ;

hence x2 . k = 0 by A60, A52; :: thesis: verum

end;assume A60: k in dom x2 ; :: thesis: x2 . k = 0

then F . k c= {} by A10, A59, A53, FUNCT_1:3, ZFMISC_1:74;

then F . k = {} ;

then M . (F . k) = 0 by VALUED_0:def 19;

then (M * F) . k = 0 by A53, A60, FUNCT_1:13;

then (a2 . k) * ((M * F) . k) = 0 ;

hence x2 . k = 0 by A60, A52; :: thesis: verum

hence integral' (M,(max- f)) = Sum x2 by A59, A58, MESFUNC5:def 14; :: thesis: verum

A63: ( len rx1 = len F & len rx2 = len F ) by A26, A52, FINSEQ_1:def 3;

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by A1, A2, MESFUNC2:34, MESFUN11:54;

then Integral (M,f) = (Sum rx1) - (Sum rx2) by A36, A62, Lm1;

then A64: Integral (M,f) = Sum (rx1 - rx2) by A63, INTEGRA5:2;

len (rx1 - rx2) = len rx1 by A63, INTEGRA5:2;

then A65: dom (rx1 - rx2) = dom x by A5, A27, FINSEQ_3:29;

for k being object st k in dom x holds

x . k = (rx1 - rx2) . k

proof

hence
Integral (M,f) = Sum x
by A64, A65, FUNCT_1:2, MESFUNC3:2; :: thesis: verum
let k be object ; :: thesis: ( k in dom x implies x . k = (rx1 - rx2) . k )

assume A66: k in dom x ; :: thesis: x . k = (rx1 - rx2) . k

then reconsider k1 = k as Nat ;

A67: x . k = (a . k1) * ((M * F) . k1) by A6, A66;

A68: (rx1 - rx2) . k = (rx1 . k1) - (rx2 . k1) by A65, A66, VALUED_1:13;

A69: ( rx1 . k1 = (a1 . k1) * ((M * F) . k1) & rx2 . k1 = (a2 . k1) * ((M * F) . k1) ) by A5, A26, A28, A52, A66;

end;assume A66: k in dom x ; :: thesis: x . k = (rx1 - rx2) . k

then reconsider k1 = k as Nat ;

A67: x . k = (a . k1) * ((M * F) . k1) by A6, A66;

A68: (rx1 - rx2) . k = (rx1 . k1) - (rx2 . k1) by A65, A66, VALUED_1:13;

A69: ( rx1 . k1 = (a1 . k1) * ((M * F) . k1) & rx2 . k1 = (a2 . k1) * ((M * F) . k1) ) by A5, A26, A28, A52, A66;

per cases
( F . k1 = {} or F . k1 <> {} )
;

end;

suppose
F . k1 = {}
; :: thesis: x . k = (rx1 - rx2) . k

then
M . (F . k1) = 0
by VALUED_0:def 19;

then (M * F) . k1 = 0 by A5, A66, FUNCT_1:13;

then ( x . k = 0 & rx1 . k1 = 0 & rx2 . k1 = 0 ) by A67, A69;

hence x . k = (rx1 - rx2) . k by A68; :: thesis: verum

end;then (M * F) . k1 = 0 by A5, A66, FUNCT_1:13;

then ( x . k = 0 & rx1 . k1 = 0 & rx2 . k1 = 0 ) by A67, A69;

hence x . k = (rx1 - rx2) . k by A68; :: thesis: verum

suppose A70:
F . k1 <> {}
; :: thesis: x . k = (rx1 - rx2) . k

then consider p being object such that

A71: p in F . k1 by XBOOLE_0:def 1;

F . k1 in rng F by A5, A66, FUNCT_1:3;

then p in union (rng F) by A71, TARSKI:def 4;

then A72: p in dom f by A4, MESFUNC3:def 1;

then A73: ( (max- f) . p = 0 implies (max+ f) . p = f . p ) by MESFUNC2:22;

reconsider p = p as Element of X by A71;

a . k1 is Real by A1, A4, A5, A66, A70, Th12;

then reconsider r = f . p as Real by A4, A5, A66, A71, MESFUNC3:def 1;

A74: ( a1 . k1 = (max+ f) . p & a2 . k1 = (max- f) . p ) by A5, A66, A71, A20, A46;

A75: ( (max- f) . p = - (f . p) implies (max+ f) . p = 0 ) by MESFUNC2:21;

end;A71: p in F . k1 by XBOOLE_0:def 1;

F . k1 in rng F by A5, A66, FUNCT_1:3;

then p in union (rng F) by A71, TARSKI:def 4;

then A72: p in dom f by A4, MESFUNC3:def 1;

then A73: ( (max- f) . p = 0 implies (max+ f) . p = f . p ) by MESFUNC2:22;

reconsider p = p as Element of X by A71;

a . k1 is Real by A1, A4, A5, A66, A70, Th12;

then reconsider r = f . p as Real by A4, A5, A66, A71, MESFUNC3:def 1;

A74: ( a1 . k1 = (max+ f) . p & a2 . k1 = (max- f) . p ) by A5, A66, A71, A20, A46;

A75: ( (max- f) . p = - (f . p) implies (max+ f) . p = 0 ) by MESFUNC2:21;

per cases
( (max+ f) . p = f . p or (max- f) . p = 0 or (max+ f) . p = 0 or (max- f) . p = - (f . p) )
by MESFUNC2:18;

end;

suppose A76:
( (max+ f) . p = f . p or (max- f) . p = 0 )
; :: thesis: x . k = (rx1 - rx2) . k

then
(max- f) . p = 0
by MESFUNC2:19;

then rx2 . k1 = 0 by A69, A74;

hence x . k = (rx1 - rx2) . k by A4, A5, A67, A68, A69, A74, A76, A66, A71, A73, MESFUNC3:def 1; :: thesis: verum

end;then rx2 . k1 = 0 by A69, A74;

hence x . k = (rx1 - rx2) . k by A4, A5, A67, A68, A69, A74, A76, A66, A71, A73, MESFUNC3:def 1; :: thesis: verum

suppose A77:
( (max+ f) . p = 0 or (max- f) . p = - (f . p) )
; :: thesis: x . k = (rx1 - rx2) . k

then
rx1 . k1 = 0
by A69, A74, A75;

then A78: (rx1 - rx2) . k = - (rx2 . k1) by A68;

a2 . k1 = - (f . p) by A74, A72, A77, MESFUNC2:20;

then rx2 . k1 = - ((f . p) * ((M * F) . k1)) by A69, XXREAL_3:92;

hence x . k = (rx1 - rx2) . k by A4, A5, A78, A67, A66, A71, MESFUNC3:def 1; :: thesis: verum

end;then A78: (rx1 - rx2) . k = - (rx2 . k1) by A68;

a2 . k1 = - (f . p) by A74, A72, A77, MESFUNC2:20;

then rx2 . k1 = - ((f . p) * ((M * F) . k1)) by A69, XXREAL_3:92;

hence x . k = (rx1 - rx2) . k by A4, A5, A78, A67, A66, A71, MESFUNC3:def 1; :: thesis: verum