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 ;
A8: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
defpred S1[ Nat, ExtReal] means for x being object st x in F . \$1 holds
\$2 = max ((f . x),0);
A9: dom a = dom F by ;
( dom (max+ f) = dom f & dom (max- f) = dom f ) by ;
then A10: ( dom (max+ f) = union (rng F) & dom (max- f) = union (rng F) ) by ;
A11: for k being Nat st k in Seg (len a) holds
ex y being Element of ExtREAL st S1[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (len a) implies ex y being Element of ExtREAL st S1[k,y] )
assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S1[k,y]
then A12: k in dom a by FINSEQ_1:def 3;
per cases ( F . k = {} or F . k <> {} ) ;
suppose A13: F . k = {} ; :: thesis: ex y being Element of ExtREAL st S1[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 S1[k,y] by A14; :: thesis: verum
end;
suppose F . k <> {} ; :: thesis: ex y being Element of ExtREAL st S1[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)
proof
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 ;
hence max ((f . p),0) = max ((f . x),0) ; :: thesis: verum
end;
hence ex y being Element of ExtREAL st S1[k,y] by A16; :: thesis: verum
end;
end;
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
S1[k,a1 . k] from A19: dom a1 = dom a by ;
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: ( 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 ;
then x in union (rng F) by ;
then x in dom f by ;
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 ; :: thesis: verum
end;
then A24: F,a1 are_Re-presentation_of max+ f by ;
defpred S2[ 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 S2[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
S2[k,x1 . k] ) ) from A27: dom x1 = dom F by ;
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
let q be object ; :: thesis: ( q in rng x1 implies b1 in REAL )
assume q in rng x1 ; :: thesis: b1 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 ;
per cases ( a1 . p is Real or F . p = {} ) by A1, A24, A29, A27, Th4, Th12;
suppose A31: a1 . p is Real ; :: thesis: b1 in REAL
F . p c= union (rng F) by ;
then F . p c= E by ;
then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by ;
then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by ;
then (M * F) . p in REAL by ;
hence q in REAL by ; :: thesis: verum
end;
end;
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 ( dom (max+ f) = {} or dom (max+ f) <> {} ) ;
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
proof
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 ;
then F . k = {} ;
then M . (F . k) = 0 by VALUED_0:def 19;
then (M * F) . k = 0 by ;
then (a1 . k) * ((M * F) . k) = 0 ;
hence x1 . k = 0 by ; :: thesis: verum
end;
then Sum rx1 = 0 * (len rx1) by Lm2;
hence integral' (M,(max+ f)) = Sum x1 by ; :: thesis: verum
end;
suppose A35: dom (max+ f) <> {} ; :: thesis: integral' (M,(max+ f)) = Sum x1
then integral (M,(max+ f)) = Sum x1 by ;
hence integral' (M,(max+ f)) = Sum x1 by ; :: thesis: verum
end;
end;
end;
then A36: Integral (M,(max+ f)) = Sum rx1 by ;
defpred S3[ 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 S3[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (len a) implies ex y being Element of ExtREAL st S3[k,y] )
assume k in Seg (len a) ; :: thesis: ex y being Element of ExtREAL st S3[k,y]
then A38: k in dom a by FINSEQ_1:def 3;
per cases ( F . k = {} or F . k <> {} ) ;
suppose A39: F . k = {} ; :: thesis: ex y being Element of ExtREAL st S3[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 S3[k,y] by A40; :: thesis: verum
end;
suppose F . k <> {} ; :: thesis: ex y being Element of ExtREAL st S3[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)
proof
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 ;
hence max ((- (f . p)),0) = max ((- (f . x)),0) ; :: thesis: verum
end;
hence ex y being Element of ExtREAL st S3[k,y] by A42; :: thesis: verum
end;
end;
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
S3[k,a2 . k] from A45: dom a2 = dom a by ;
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: ( 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 ;
then x in union (rng F) by ;
then x in dom f by ;
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 ; :: thesis: verum
end;
A50: F,a2 are_Re-presentation_of max- f by ;
defpred S4[ 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 S4[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
S4[k,x2 . k] ) ) from A53: dom x2 = dom F by ;
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
let q be object ; :: thesis: ( q in rng x2 implies b1 in REAL )
assume q in rng x2 ; :: thesis: b1 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 ;
per cases ( a2 . p is Real or F . p = {} ) by A1, A50, A55, A53, Th4, Th12;
suppose A57: a2 . p is Real ; :: thesis: b1 in REAL
F . p c= union (rng F) by ;
then F . p c= E by ;
then ( 0 <= M . (F . p) & M . (F . p) <= M . E ) by ;
then ( 0 <= (M * F) . p & (M * F) . p <= M . E ) by ;
then (M * F) . p in REAL by ;
hence q in REAL by ; :: thesis: verum
end;
end;
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 ( dom (max- f) = {} or dom (max- f) <> {} ) ;
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
proof
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 ;
then F . k = {} ;
then M . (F . k) = 0 by VALUED_0:def 19;
then (M * F) . k = 0 by ;
then (a2 . k) * ((M * F) . k) = 0 ;
hence x2 . k = 0 by ; :: thesis: verum
end;
then Sum rx2 = 0 * (len rx2) by Lm2;
hence integral' (M,(max- f)) = Sum x2 by ; :: thesis: verum
end;
suppose A61: dom (max- f) <> {} ; :: thesis: integral' (M,(max- f)) = Sum x2
then integral (M,(max- f)) = Sum x2 by ;
hence integral' (M,(max- f)) = Sum x2 by ; :: thesis: verum
end;
end;
end;
then A62: Integral (M,(max- f)) = Sum rx2 by ;
A63: ( len rx1 = len F & len rx2 = len F ) by ;
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by ;
then Integral (M,f) = (Sum rx1) - (Sum rx2) by ;
then A64: Integral (M,f) = Sum (rx1 - rx2) by ;
len (rx1 - rx2) = len rx1 by ;
then A65: dom (rx1 - rx2) = dom x by ;
for k being object st k in dom x holds
x . k = (rx1 - rx2) . k
proof
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 ;
A68: (rx1 - rx2) . k = (rx1 . k1) - (rx2 . k1) by ;
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 <> {} ) ;
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 ;
then ( x . k = 0 & rx1 . k1 = 0 & rx2 . k1 = 0 ) by ;
hence x . k = (rx1 - rx2) . k by A68; :: thesis: verum
end;
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 ;
then p in union (rng F) by ;
then A72: p in dom f by ;
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 ;
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: x . k = (rx1 - rx2) . k
then (max- f) . p = 0 by MESFUNC2:19;
then rx2 . k1 = 0 by ;
hence x . k = (rx1 - rx2) . k by ; :: thesis: verum
end;
suppose A77: ( (max+ f) . p = 0 or (max- f) . p = - (f . p) ) ; :: thesis: x . k = (rx1 - rx2) . k
then rx1 . k1 = 0 by ;
then A78: (rx1 - rx2) . k = - (rx2 . k1) by A68;
a2 . k1 = - (f . p) by ;
then rx2 . k1 = - ((f . p) * ((M * F) . k1)) by ;
hence x . k = (rx1 - rx2) . k by ; :: thesis: verum
end;
end;
end;
end;
end;
hence Integral (M,f) = Sum x by ; :: thesis: verum