let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
let a, x be FinSequence of ExtREAL ; :: thesis:
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:
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₁[ 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₁[k,y]

proof

let k be Nat; :: thesis:
assume k in Seg (len a) ; :: thesis:
then A12: k in dom a by FINSEQ_1:def 3;

per cases ;

suppose A13: F . k = {} ; :: thesis:

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₁[k,y] by A14; :: thesis:

end;

suppose F . k <> {} ; :: thesis:

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)

proof

let x be object ; :: thesis:
assume x in F . k ; :: thesis:
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:

end;

hence ex y being Element of ExtREAL st S₁[k,y] by A16; :: thesis:

end;

consider a1 being FinSequence of ExtREAL such that
A17: dom a1 = Seg (len a) and
A18: for k being Nat st k in Seg (len a) holds
S₁[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

proof

let k be Nat; :: thesis:
assume A21: k in dom F ; :: thesis:
let x be object ; :: thesis:
assume A22: x in F . k ; :: thesis:
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:

end;

then A24: F,a1 are_Re-presentation_of max+ f by A10, A9, A19, MESFUNC3:def 1;
defpred S₂[ 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₂[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₂[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;

now :: thesis:

let q be object ; :: thesis:
assume q in rng x1 ; :: thesis:
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 by A1, A24, A29, A27, Th4, Th12;

suppose A31: a1 . p is Real ; :: thesis:

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:

end;

suppose F . p = {} ; :: thesis:

then M . (F . p) = 0 by VALUED_0:def 19;
then (M * F) . p = 0 by A29, A27, FUNCT_1:13;
hence q in REAL by A30, XREAL_0:def 1; :: thesis:

end;

then rng x1 c= REAL ;
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

per cases ;

suppose A33: dom (max+ f) = {} ; :: thesis:

for k being Nat st k in dom x1 holds
x1 . k = 0

proof

let k be Nat; :: thesis:
assume A34: k in dom x1 ; :: thesis:
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:

end;

then Sum rx1 = 0 * (len rx1) by Lm2;
hence integral' (M,(max+ f)) = Sum x1 by A33, A32, MESFUNC5:def 14; :: thesis:

end;

suppose A35: dom (max+ f) <> {} ; :: thesis:

then integral (M,(max+ f)) = Sum x1 by A7, A10, A9, A19, A20, A26, A28, A8, MESFUNC3:def 1, MESFUNC4:3;
hence integral' (M,(max+ f)) = Sum x1 by A35, MESFUNC5:def 14; :: thesis:

end;

then A36: Integral (M,(max+ f)) = Sum rx1 by A7, A8, A32, MESFUNC5:89;
defpred S₃[ 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₃[k,y]

proof

let k be Nat; :: thesis:
assume k in Seg (len a) ; :: thesis:
then A38: k in dom a by FINSEQ_1:def 3;

per cases ;

suppose A39: F . k = {} ; :: thesis:

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₃[k,y] by A40; :: thesis:

end;

suppose F . k <> {} ; :: thesis:

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)

proof

let x be object ; :: thesis:
assume x in F . k ; :: thesis:
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:

end;

hence ex y being Element of ExtREAL st S₃[k,y] by A42; :: thesis:

end;

consider a2 being FinSequence of ExtREAL such that
A43: dom a2 = Seg (len a) and
A44: for k being Nat st k in Seg (len a) holds
S₃[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

proof

let k be Nat; :: thesis:
assume A47: k in dom F ; :: thesis:
let x be object ; :: thesis:
assume A48: x in F . k ; :: thesis:
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:

end;

A50: F,a2 are_Re-presentation_of max- f by A10, A9, A45, A46, MESFUNC3:def 1;
defpred S₄[ 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₄[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₄[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;

now :: thesis:

let q be object ; :: thesis:
assume q in rng x2 ; :: thesis:
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 by A1, A50, A55, A53, Th4, Th12;

suppose A57: a2 . p is Real ; :: thesis:

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:

end;

suppose F . p = {} ; :: thesis:

then M . (F . p) = 0 by VALUED_0:def 19;
then (M * F) . p = 0 by A55, A53, FUNCT_1:13;
hence q in REAL by A56, XREAL_0:def 1; :: thesis:

end;

then rng x2 c= REAL ;
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

per cases ;

suppose A59: dom (max- f) = {} ; :: thesis:

for k being Nat st k in dom x2 holds
x2 . k = 0

proof

let k be Nat; :: thesis:
assume A60: k in dom x2 ; :: thesis:
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:

end;

then Sum rx2 = 0 * (len rx2) by Lm2;
hence integral' (M,(max- f)) = Sum x2 by A59, A58, MESFUNC5:def 14; :: thesis:

end;

suppose A61: dom (max- f) <> {} ; :: thesis:

then integral (M,(max- f)) = Sum x2 by A7, A52, A54, A8, A10, A9, A45, A46, MESFUNC3:def 1, MESFUNC4:3;
hence integral' (M,(max- f)) = Sum x2 by A61, MESFUNC5:def 14; :: thesis:

end;

then A62: Integral (M,(max- f)) = Sum rx2 by A7, A8, A58, MESFUNC5:89;
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

let k be object ; :: thesis:
assume A66: k in dom x ; :: thesis:
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 ;

suppose F . k1 = {} ; :: thesis:

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:

end;

suppose A70: F . k1 <> {} ; :: thesis:

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;

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

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

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:

end;

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

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:

end;

hence Integral (M,f) = Sum x by A64, A65, FUNCT_1:2, MESFUNC3:2; :: thesis: