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