let Omega be non empty finite set ; :: thesis:
let M be sigma_Measure of (Trivial-SigmaField Omega); :: thesis:
let f be Function of Omega,REAL ; :: thesis:
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 S₁[ Nat, set ] means $2 = (R_EAL (ap . $1)) * ((M * Fp) . $1);
A6: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S₁[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
S₁[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 set st x in Fp . n holds
(max+ f) . x = ap . n

proof

let n be Nat; :: thesis:
assume A10: n in dom Fp ; :: thesis:
let x be set ; :: thesis:
assume x in Fp . n ; :: thesis:
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:22; :: thesis:

end;

reconsider a = f * (canFS (dom f)) as FinSequence of REAL by Lm8;
A11: (R_EAL (- 1)) * (Integral M,(max- f)) = (- (R_EAL 1)) * (Integral M,(max- f)) by SUPINF_2:3
.= - ((R_EAL 1) * (Integral M,(max- f))) by XXREAL_3:103
.= - (Integral M,(max- f)) by XXREAL_3:92 ;
defpred S₂[ Nat, set ] means $2 = (R_EAL (a . $1)) * ((M * F) . $1);
A12: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S₂[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
S₂[k,x . k] ) ) from FINSEQ_1:sch 5(A12);
assume A14: M . Omega < +infty ; :: thesis:
A15: for n being Nat st n in dom (canFS Omega) holds
M . {((canFS Omega) . n)} in REAL

proof

let n be Nat; :: thesis:
assume n in dom (canFS Omega) ; :: thesis:
then (canFS Omega) . n in rng (canFS Omega) by FUNCT_1:12;
then A16: {((canFS Omega) . n)} c= Omega by ZFMISC_1:37;
Omega in Trivial-SigmaField Omega by MEASURE1:21;
hence M . {((canFS Omega) . n)} in REAL by A14, A16, Lm7; :: thesis:

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 = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)})

proof

let n be Nat; :: thesis:
assume A22: n in dom x ; :: thesis:
then A23: (M * F) . n = M . (F . n) by A20, FUNCT_1:23
.= M . {((canFS Omega) . n)} by A2, A17, A20, A22 ;
A24: f . ((canFS (dom f)) . n) = a . n by A1, A20, A22, FUNCT_1:23;
thus x . n = (R_EAL (a . n)) * ((M * F) . n) by A13, A22
.= (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A24, A23, FUNCT_2:def 1 ; :: thesis:

end;

x is FinSequence of REAL

proof

let y be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis:
assume y in rng x ; :: thesis:
then consider n being Element of NAT such that
A25: n in dom x and
A26: y = x . n by PARTFUN1:26;
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 ;
x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A21, A25
.= w * z by EXTREAL1:13 ;
hence y in REAL by A26; :: thesis:

end;

then reconsider x1 = x as FinSequence of REAL ;
take x ; :: thesis:
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 = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)})

proof

let n be Nat; :: thesis:
assume A32: n in dom xp ; :: thesis:
then A33: (M * Fp) . n = M . (Fp . n) by A29, FUNCT_1:23
.= 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:23;
thus xp . n = (R_EAL (ap . n)) * ((M * Fp) . n) by A7, A32
.= (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A34, A33, FUNCT_2:def 1 ; :: thesis:

end;

now

let y be set ; :: thesis:
assume y in rng xp ; :: thesis:
then consider n being Element of NAT such that
A35: n in dom xp and
A36: y = xp . n by PARTFUN1:26;
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 ;
xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A31, A35
.= w * z by EXTREAL1:13 ;
hence y in REAL by A36; :: thesis:

end;

then rng xp c= REAL by TARSKI:def 3;
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 S₃[ Nat, set ] means $2 = (R_EAL (am . $1)) * ((M * Fm) . $1);
A40: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S₃[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
S₃[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 = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)})

proof

let n be Nat; :: thesis:
assume A46: n in dom xm ; :: thesis:
then A47: (M * Fm) . n = M . (Fm . n) by A43, FUNCT_1:23
.= M . {((canFS Omega) . n)} by A17, A39, A44, A43, A46 ;
thus xm . n = (R_EAL (am . n)) * ((M * Fm) . n) by A41, A46
.= (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A38, A43, A18, A46, A47, FUNCT_1:23 ; :: thesis:

end;

now

let y be set ; :: thesis:
assume y in rng xm ; :: thesis:
then consider n being Element of NAT such that
A48: n in dom xm and
A49: y = xm . n by PARTFUN1:26;
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 ;
xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by A45, A48
.= w * z by EXTREAL1:13 ;
hence y in REAL by A49; :: thesis:

end;

proof

let n be Nat; :: thesis:
assume A62: n in dom Fm ; :: thesis:
let x be set ; :: thesis:
assume x in Fm . n ; :: thesis:
then x in {((canFS (dom (max- f))) . n)} by A39, A62;
then x = (canFS (dom (max- f))) . n by TARSKI:def 1;
hence (max- f) . x = am . n by A60, A62, FUNCT_1:22; :: thesis:

end;

( max+ f is_simple_func_in Trivial-SigmaField Omega & max+ f is nonnegative ) by Th6, MESFUNC6:61;
then A63: 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 A64: len F = len (canFS (dom f)) by FINSEQ_1:def 3;
A65: len x = len F by A13, FINSEQ_1:def 3;
A66: dom (xp1 - xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12
.= dom x1 by A28, A42, A13, A29, A43, FINSEQ_1:def 3 ;
A67: len xp1 = len F by A7, FINSEQ_1:def 3
.= len xm1 by A41, FINSEQ_1:def 3 ;
A68: for k being Nat st k in dom x1 holds
(xp1 - xm1) . k = x1 . k

proof

let k be Nat; :: thesis:
A69: f = (max+ f) - (max- f) by MESFUNC6:42;
assume A70: k in dom x1 ; :: thesis:
then reconsider z = M . {((canFS Omega) . k)} as Element of REAL by A1, A17, A20, A15;
A71: xm1 . k = (R_EAL ((max- f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by A13, A41, A45, A70
.= ((max- f) . ((canFS Omega) . k)) * z by EXTREAL1:13 ;
k in dom (canFS Omega) by A1, A20, A70, FUNCT_2:def 1;
then (canFS Omega) . k in rng (canFS Omega) by FUNCT_1:12;
then (canFS Omega) . k in Omega ;
then A72: (canFS Omega) . k in dom f by FUNCT_2:def 1;
k in (dom xp1) /\ (dom xm1) by A13, A7, A41, A70;
then A73: k in dom (xp1 - xm1) by VALUED_1:12;
xp1 . k = (R_EAL ((max+ f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by A13, A7, A31, A70
.= ((max+ f) . ((canFS Omega) . k)) * z by EXTREAL1:13 ;
hence (xp1 - xm1) . k = (((max+ f) . ((canFS Omega) . k)) * z) - (((max- f) . ((canFS Omega) . k)) * z) by A73, A71, VALUED_1:13
.= (((max+ f) . ((canFS Omega) . k)) - ((max- f) . ((canFS Omega) . k))) * z
.= (f . ((canFS Omega) . k)) * z by A72, A69, VALUED_1:13
.= (R_EAL (f . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by EXTREAL1:13
.= x1 . k by A21, A70 ;
:: thesis:

end;

Integral M,f = Integral M,((max+ f) - (max- f)) by MESFUNC6:42
.= (Sum xp) - (Sum xm) by A52, A37, A27, A41, A43, A63, A59, A60, A61, Lm1
.= (Sum xp1) - (Sum xm1) by A50, SUPINF_2:5
.= Sum (xp1 - xm1) by A67, INTEGRA5:2
.= Sum x by A66, A68, FINSEQ_1:17, MESFUNC3:2 ;
hence ( len x = card Omega & ( for n being Nat st n in dom x holds
x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) & Integral M,f = Sum x ) by A17, A21, A65, A64, UPROOTS:5; :: thesis: