let Omega be non empty finite set ; :: thesis: for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being Function of Omega,REAL
for x being FinSequence of ExtREAL
for s being FinSequence of Omega st M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ) holds
Integral (M,f) = Sum x
let M be sigma_Measure of (Trivial-SigmaField Omega); :: thesis: for f being Function of Omega,REAL
for x being FinSequence of ExtREAL
for s being FinSequence of Omega st M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ) holds
Integral (M,f) = Sum x
let f be Function of Omega,REAL; :: thesis: for x being FinSequence of ExtREAL
for s being FinSequence of Omega st M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ) holds
Integral (M,f) = Sum x
let x be FinSequence of ExtREAL ; :: thesis: for s being FinSequence of Omega st M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ) holds
Integral (M,f) = Sum x
let s be FinSequence of Omega; :: thesis: ( M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ) implies Integral (M,f) = Sum x )
assume that
A1: M . Omega < +infty and
A2: len x = card Omega and
A3: s is one-to-one and
A4: rng s = Omega and
A5: len s = card Omega and
A6: for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (M . {(s . n)}) ; :: thesis: Integral (M,f) = Sum x
set Sigma = Trivial-SigmaField Omega;
consider F being Finite_Sep_Sequence of Trivial-SigmaField Omega, a being FinSequence of REAL such that
A7: dom f = union (rng F) and
dom a = dom s and
A8: dom F = dom s and
A9: for k being Nat st k in dom F holds
F . k = {(s . k)} and
for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y by A3, A4, Th9;
A10: dom x = Seg (len s) by A2, A5, FINSEQ_1:def 3
.= dom F by A8, FINSEQ_1:def 3 ;
set fm = max- f;
set fp = max+ f;
A11: dom f = Omega by FUNCT_2:def 1;
then dom (max+ f) = Omega by RFUNCT_3:def 10;
then A12: max+ f is_integrable_on M by A1, Lm5, Th6;
A13: for n being Nat st n in dom s holds
M . {(s . n)} in REAL
proof
let n be Nat; :: thesis: ( n in dom s implies M . {(s . n)} in REAL )
assume n in dom s ; :: thesis: M . {(s . n)} in REAL
then s . n in rng s by FUNCT_1:3;
then {(s . n)} c= Omega by ZFMISC_1:31;
hence M . {(s . n)} in REAL by A1, A4, Lm7; :: thesis: verum
end;
now :: thesis: for y being object st y in rng x holds
y in REAL
let y be object ; :: thesis: ( y in rng x implies y in REAL )
assume y in rng x ; :: thesis: y in REAL
then consider n being Element of NAT such that
A14: n in dom x and
A15: y = x . n by PARTFUN1:3;
reconsider z = M . {(s . n)} as Element of REAL by A8, A10, A13, A14;
reconsider w = f . (s . n) as Element of REAL by XREAL_0:def 1;
x . n = (f . (s . n)) * (M . {(s . n)}) by A6, A14
.= w * z by EXTREAL1:1 ;
hence y in REAL by A15; :: thesis: verum
end;
then rng x c= REAL ;
then reconsider x1 = x as FinSequence of REAL by FINSEQ_1:def 4;
A16: ( max- f is_simple_func_in Trivial-SigmaField Omega & max- f is nonnegative ) by Th6, MESFUNC6:61;
defpred S1[ Nat, set ] means for x being object st x in F . $1 holds
$2 = (max+ f) . x;
set L = len F;
A17: dom F = Seg (len F) by FINSEQ_1:def 3;
A18: for k being Nat st k in Seg (len F) holds
ex y being Element of REAL st S1[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of REAL st S1[k,y] )
assume A19: k in Seg (len F) ; :: thesis: ex y being Element of REAL st S1[k,y]
reconsider fpsk = (max+ f) . (s . k) as Element of REAL by XREAL_0:def 1;
take fpsk ; :: thesis: S1[k,fpsk]
F . k = {(s . k)} by A9, A17, A19;
hence S1[k,fpsk] by TARSKI:def 1; :: thesis: verum
end;
consider ap being FinSequence of REAL such that
A20: ( dom ap = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,ap . k] ) ) from FINSEQ_1:sch 5(A18);
 defpred S2[ Nat, set ] means for x being object st x in F . $1 holds
$2 = (max- f) . x;
A21: for k being Nat st k in Seg (len F) holds
ex y being Element of REAL st S2[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of REAL st S2[k,y] )
assume A22: k in Seg (len F) ; :: thesis: ex y being Element of REAL st S2[k,y]
reconsider fmsk = (max- f) . (s . k) as Element of REAL by XREAL_0:def 1;
take fmsk ; :: thesis: S2[k,fmsk]
F . k = {(s . k)} by A9, A17, A22;
hence S2[k,fmsk] by TARSKI:def 1; :: thesis: verum
end;
consider am being FinSequence of REAL such that
A23: ( dom am = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S2[k,am . k] ) ) from FINSEQ_1:sch 5(A21);
 A24: dom (max- f) = dom f by RFUNCT_3:def 11;
then A25: max- f is Function of Omega,REAL by A11, FUNCT_2:def 1;
then M . (dom ((- 1) (#) (max- f))) < +infty by A1, FUNCT_2:def 1;
then (- 1) (#) (max- f) is_integrable_on M by A25, Lm5, Th6;
then consider E being Element of Trivial-SigmaField Omega such that
A26: E = (dom (max+ f)) /\ (dom ((- 1) (#) (max- f))) and
A27: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,((max+ f) | E))) + (Integral (M,(((- 1) (#) (max- f)) | E))) by A12, MESFUNC6:101;
A28: (- jj) * (Integral (M,(max- f))) = (- jj) * (Integral (M,(max- f)))
.= - (1 * (Integral (M,(max- f)))) by XXREAL_3:92
.= - (Integral (M,(max- f))) by XXREAL_3:81 ;
defpred S3[ Nat, set ] means $2 = (ap . $1) * ((M * F) . $1);
A29: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S3[k,x] ;
consider xp being FinSequence of ExtREAL such that
A30: ( dom xp = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S3[k,xp . k] ) ) from FINSEQ_1:sch 5(A29);
 A31: dom xp = dom F by A30, FINSEQ_1:def 3;
A32: for n being Nat st n in dom xp holds
xp . n = ((max+ f) . (s . n)) * (M . {(s . n)})
proof
let n be Nat; :: thesis: ( n in dom xp implies xp . n = ((max+ f) . (s . n)) * (M . {(s . n)}) )
assume A33: n in dom xp ; :: thesis: xp . n = ((max+ f) . (s . n)) * (M . {(s . n)})
then A34: (M * F) . n = M . (F . n) by A31, FUNCT_1:13
.= M . {(s . n)} by A9, A31, A33 ;
F . n = {(s . n)} by A9, A31, A33;
then A35: s . n in F . n by TARSKI:def 1;
thus xp . n = (ap . n) * ((M * F) . n) by A30, A33
.= ((max+ f) . (s . n)) * (M . {(s . n)}) by A20, A30, A33, A35, A34 ; :: thesis: verum
end;
now :: thesis: for y being object st y in rng xp holds
y in REAL
let y be object ; :: thesis: ( y in rng xp implies y in REAL )
assume y in rng xp ; :: thesis: y in REAL
then consider n being Element of NAT such that
A36: n in dom xp and
A37: y = xp . n by PARTFUN1:3;
reconsider z = M . {(s . n)} as Element of REAL by A8, A31, A13, A36;
reconsider w = (max+ f) . (s . n) as Element of REAL by XREAL_0:def 1;
xp . n = ((max+ f) . (s . n)) * (M . {(s . n)}) by A32, A36
.= w * z by EXTREAL1:1 ;
hence y in REAL by A37; :: thesis: verum
end;
then rng xp c= REAL ;
then reconsider xp1 = xp as FinSequence of REAL by FINSEQ_1:def 4;
defpred S4[ Nat, set ] means $2 = (am . $1) * ((M * F) . $1);
A38: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S4[k,x] ;
consider xm being FinSequence of ExtREAL such that
A39: ( dom xm = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S4[k,xm . k] ) ) from FINSEQ_1:sch 5(A38);
 A40: dom xm = dom F by A39, FINSEQ_1:def 3;
A41: for n being Nat st n in dom xm holds
xm . n = ((max- f) . (s . n)) * (M . {(s . n)})
proof
let n be Nat; :: thesis: ( n in dom xm implies xm . n = ((max- f) . (s . n)) * (M . {(s . n)}) )
assume A42: n in dom xm ; :: thesis: xm . n = ((max- f) . (s . n)) * (M . {(s . n)})
then A43: (M * F) . n = M . (F . n) by A40, FUNCT_1:13
.= M . {(s . n)} by A9, A40, A42 ;
F . n = {(s . n)} by A9, A40, A42;
then A44: s . n in F . n by TARSKI:def 1;
thus xm . n = (am . n) * ((M * F) . n) by A39, A42
.= ((max- f) . (s . n)) * (M . {(s . n)}) by A23, A39, A42, A44, A43 ; :: thesis: verum
end;
now :: thesis: for y being object st y in rng xm holds
y in REAL
let y be object ; :: thesis: ( y in rng xm implies y in REAL )
assume y in rng xm ; :: thesis: y in REAL
then consider n being Element of NAT such that
A45: n in dom xm and
A46: y = xm . n by PARTFUN1:3;
reconsider z = M . {(s . n)} as Element of REAL by A8, A40, A13, A45;
reconsider w = (max- f) . (s . n) as Element of REAL by XREAL_0:def 1;
xm . n = ((max- f) . (s . n)) * (M . {(s . n)}) by A41, A45
.= w * z by EXTREAL1:1 ;
hence y in REAL by A46; :: thesis: verum
end;
then rng xm c= REAL ;
then reconsider xm1 = xm as FinSequence of REAL by FINSEQ_1:def 4;
A47: ( Sum xp = Sum xp1 & Sum xm = Sum xm1 ) by MESFUNC3:2;
A48: for k being Nat st k in dom x1 holds
(xp1 - xm1) . k = x1 . k
proof
let k be Nat; :: thesis: ( k in dom x1 implies (xp1 - xm1) . k = x1 . k )
A49: f = (max+ f) - (max- f) by MESFUNC6:42;
assume A50: k in dom x1 ; :: thesis: (xp1 - xm1) . k = x1 . k
then reconsider z = M . {(s . k)} as Element of REAL by A8, A10, A13;
A51: xm1 . k = ((max- f) . (s . k)) * (M . {(s . k)}) by A10, A40, A41, A50
.= ((max- f) . (s . k)) * z by EXTREAL1:1 ;
s . k in rng s by A8, A10, A50, FUNCT_1:3;
then s . k in Omega ;
then A52: s . k in dom f by FUNCT_2:def 1;
k in (dom xp1) /\ (dom xm1) by A10, A31, A40, A50;
then A53: k in dom (xp1 - xm1) by VALUED_1:12;
xp1 . k = ((max+ f) . (s . k)) * (M . {(s . k)}) by A10, A31, A32, A50
.= ((max+ f) . (s . k)) * z by EXTREAL1:1 ;
hence (xp1 - xm1) . k = (((max+ f) . (s . k)) * z) - (((max- f) . (s . k)) * z) by A53, A51, VALUED_1:13
.= (((max+ f) . (s . k)) - ((max- f) . (s . k))) * z
.= (f . (s . k)) * z by A52, A49, VALUED_1:13
.= (f . (s . k)) * (M . {(s . k)}) by EXTREAL1:1
.= x1 . k by A6, A50 ;
:: thesis: verum
end;
dom (max- f) = Omega by A11, RFUNCT_3:def 11;
then A54: max- f is_integrable_on M by A1, Lm5, Th6;
A55: dom (max+ f) = dom f by RFUNCT_3:def 10;
A56: dom (xp1 - xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12
.= dom x1 by A10, A31, A40 ;
A57: len xp1 = len F by A30, FINSEQ_1:def 3
.= len xm1 by A39, FINSEQ_1:def 3 ;
dom ((- 1) (#) (max- f)) = dom (max- f) by VALUED_1:def 5
.= Omega by A11, RFUNCT_3:def 11 ;
then A58: E = Omega /\ Omega by A11, A26, RFUNCT_3:def 10
.= Omega ;
A59: Integral (M,((max+ f) + ((- 1) (#) (max- f)))) = (Integral (M,(max+ f))) + (Integral (M,((- 1) (#) (max- f)))) by A27, A58
.= (Integral (M,(max+ f))) + (- (Integral (M,(max- f)))) by A54, A28, MESFUNC6:102 ;
( max+ f is_simple_func_in Trivial-SigmaField Omega & max+ f is nonnegative ) by Th6, MESFUNC6:61;
then A60: Integral (M,(max+ f)) = Sum xp by A7, A55, A17, A20, A30, Lm1;
thus Integral (M,f) = Integral (M,((max+ f) - (max- f))) by MESFUNC6:42
.= (Sum xp) - (Sum xm) by A7, A24, A17, A23, A16, A39, A60, A59, Lm1
.= (Sum xp1) - (Sum xm1) by A47, SUPINF_2:3
.= Sum (xp1 - xm1) by A57, INTEGRA5:2
.= Sum x by A56, A48, FINSEQ_1:13, MESFUNC3:2 ; :: thesis: verum