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:
assume AS: M . Omega < +infty ; :: thesis:
set Sigma = Trivial-SigmaField Omega;
set D = dom f;
consider F being Finite_Sep_Sequence of Trivial-SigmaField Omega such that
P1: ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . k)} ) & ( 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 Lm6A;
set fp = max+ f;
set fm = max- f;
XD0: dom f = Omega by FUNCT_2:def 1;
XDp: dom (max+ f) = dom f by RFUNCT_3:def 10;
XDm: dom (max- f) = dom f by RFUNCT_3:def 11;
set Dp = dom (max+ f);
consider Fp being Finite_Sep_Sequence of Trivial-SigmaField Omega such that
Q1: ( dom (max+ f) = union (rng Fp) & dom Fp = dom (canFS (dom (max+ f))) & ( for k being Nat st k in dom Fp holds
Fp . k = {((canFS (dom (max+ f))) . k)} ) & ( 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 Lm6A;
set Dm = dom (max- f);
consider Fm being Finite_Sep_Sequence of Trivial-SigmaField Omega such that
R1: ( dom (max- f) = union (rng Fm) & dom Fm = dom (canFS (dom (max- f))) & ( for k being Nat st k in dom Fm holds
Fm . k = {((canFS (dom (max- f))) . k)} ) & ( 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 Lm6A;
FPP: max+ f is Function of Omega,REAL by XD0, XDp, FUNCT_2:def 1;
A1: max+ f is_simple_func_in Trivial-SigmaField Omega by Lm6;
A2: max+ f is nonnegative by MESFUNC6:61;
FMM: max- f is Function of Omega,REAL by XD0, XDm, FUNCT_2:def 1;
B1: max- f is_simple_func_in Trivial-SigmaField Omega by Lm6;
B2: max- f is nonnegative by MESFUNC6:61;
XXX1: ( dom (max+ f) = dom f & dom (max- f) = dom f ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
XXX2: ( dom Fp = dom F & dom Fm = dom F ) by R1, Q1, P1, RFUNCT_3:def 10, RFUNCT_3:def 11;
set L = len F;
reconsider a = f * (canFS (dom f)) as FinSequence of REAL by LmX1;
defpred S₁[ Nat, set ] means $2 = (R_EAL (a . $1)) * ((M * F) . $1);
A1X: 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
C30: ( 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(A1X);
C3: ( dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) ) by C30, FINSEQ_1:def 3;
take x ; :: thesis:
reconsider ap = (max+ f) * (canFS (dom (max+ f))) as FinSequence of REAL by LmX1;
defpred S₂[ Nat, set ] means $2 = (R_EAL (ap . $1)) * ((M * Fp) . $1);
A1P: 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
A30: ( 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(A1P);
A3: ( dom xp = dom Fp & ( for n being Nat st n in dom xp holds
xp . n = (R_EAL (ap . n)) * ((M * Fp) . n) ) ) by A30, FINSEQ_1:def 3, XXX2;
reconsider am = (max- f) * (canFS (dom (max- f))) as FinSequence of REAL by LmX1;
defpred S₃[ Nat, set ] means $2 = (R_EAL (am . $1)) * ((M * Fm) . $1);
B1P: 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
B30: ( 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(B1P);
B3: ( dom xm = dom Fm & ( for n being Nat st n in dom xm holds
xm . n = (R_EAL (am . n)) * ((M * Fm) . n) ) ) by B30, FINSEQ_1:def 3, XXX2;
UU1: dom Fp = dom ap by LmX2, Q1;
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 Z: 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 Z, Q1;
then x = (canFS (dom (max+ f))) . n by TARSKI:def 1;
hence (max+ f) . x = ap . n by Z, UU1, FUNCT_1:22; :: thesis:

end;

then A5: Integral M,(max+ f) = Sum xp by MES43, A1, A2, A3, Q1, XDp, UU1;
X2: dom (max+ f) = Omega by XD0, RFUNCT_3:def 10;
K2: max+ f is_integrable_on M by X2, Lm9A0, Lm6, AS;
X3: dom (max- f) = Omega by XD0, RFUNCT_3:def 11;
K3: max- f is_integrable_on M by X3, Lm9A0, Lm6, AS;
M . (dom ((- 1) (#) (max- f))) < +infty by AS, FUNCT_2:def 1, FMM;
then K5: (- 1) (#) (max- f) is_integrable_on M by FMM, Lm9A0, Lm6;
consider E being Element of Trivial-SigmaField Omega such that
K6: ( E = (dom (max+ f)) /\ (dom ((- 1) (#) (max- f))) & Integral M,((max+ f) + ((- 1) (#) (max- f))) = (Integral M,((max+ f) | E)) + (Integral M,(((- 1) (#) (max- f)) | E)) ) by K2, K5, MESFUNC6:101;
K8: dom ((- 1) (#) (max- f)) = dom (max- f) by VALUED_1:def 5
.= Omega by XDm, FUNCT_2:def 1 ;
K9: E = Omega /\ Omega by XDp, FUNCT_2:def 1, K8, K6
.= Omega ;
K10: (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 ;
P6: ((- 1) (#) (max- f)) | E = (- 1) (#) (max- f) by FMM, K9, FUNCT_2:40;
P7: Integral M,((max+ f) + ((- 1) (#) (max- f))) = (Integral M,(max+ f)) + (Integral M,((- 1) (#) (max- f))) by FPP, K9, FUNCT_2:40, P6, K6
.= (Integral M,(max+ f)) + (- (Integral M,(max- f))) by K10, MESFUNC6:102, K3 ;
CFSD: 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 B1: {((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 Lm9A2, B1, AS; :: thesis:

end;

C7: 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 C71: n in dom x ; :: thesis:
C73: f . ((canFS (dom f)) . n) = a . n by C3, P1, C71, FUNCT_1:23;
C74: (M * F) . n = M . (F . n) by FUNCT_1:23, C3, C71
.= M . {((canFS Omega) . n)} by XD0, P1, C3, C71 ;
thus x . n = (R_EAL (a . n)) * ((M * F) . n) by C30, C71
.= (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by C73, C74, 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
C71: ( n in dom x & y = x . n ) by PARTFUN1:26;
reconsider w = f . ((canFS Omega) . n) as Element of REAL ;
reconsider z = M . {((canFS Omega) . n)} as Element of REAL by CFSD, C3, P1, C71, XD0;
x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by C7, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis:

end;

then reconsider x1 = x as FinSequence of REAL ;
XB7: 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 C71: n in dom xp ; :: thesis:
C73: (max+ f) . ((canFS (dom f)) . n) = ap . n by A3, Q1, C71, FUNCT_1:23, XXX1;
C74: (M * Fp) . n = M . (Fp . n) by FUNCT_1:23, A3, C71
.= M . {((canFS Omega) . n)} by XD0, XXX1, A3, Q1, C71 ;
thus xp . n = (R_EAL (ap . n)) * ((M * Fp) . n) by A30, C71
.= (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by C73, C74, FUNCT_2:def 1 ; :: thesis:

end;

xp is FinSequence of REAL

proof

now

let y be set ; :: thesis:
assume y in rng xp ; :: thesis:
then consider n being Element of NAT such that
C71: ( n in dom xp & y = xp . n ) by PARTFUN1:26;
reconsider w = (max+ f) . ((canFS Omega) . n) as Element of REAL ;
reconsider z = M . {((canFS Omega) . n)} as Element of REAL by CFSD, XXX1, A3, Q1, C71, XD0;
xp . n = (R_EAL ((max+ f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by XB7, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis:

end;

hence rng xp c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis:

end;

then reconsider xp1 = xp as FinSequence of REAL ;
XA7: 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 C71: n in dom xm ; :: thesis:
C74: (M * Fm) . n = M . (Fm . n) by FUNCT_1:23, B3, C71
.= M . {((canFS Omega) . n)} by XD0, XXX1, B3, R1, C71 ;
thus xm . n = (R_EAL (am . n)) * ((M * Fm) . n) by B30, C71
.= (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by B3, R1, C71, C74, FUNCT_1:23, X3 ; :: thesis:

end;

xm is FinSequence of REAL

proof

now

let y be set ; :: thesis:
assume y in rng xm ; :: thesis:
then consider n being Element of NAT such that
C71: ( n in dom xm & y = xm . n ) by PARTFUN1:26;
reconsider w = (max- f) . ((canFS Omega) . n) as Element of REAL ;
reconsider z = M . {((canFS Omega) . n)} as Element of REAL by CFSD, XXX1, B3, R1, C71, XD0;
xm . n = (R_EAL ((max- f) . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) by XA7, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis:

end;

hence rng xm c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis:

end;

then reconsider xm1 = xm as FinSequence of REAL ;
C51: Sum xp = Sum xp1 by MESFUNC3:2;
C52: Sum xm = Sum xm1 by MESFUNC3:2;
C54: len xp1 = len F by A30, FINSEQ_1:def 3
.= len xm1 by B30, FINSEQ_1:def 3 ;
C53: x1 = xp1 - xm1

proof

AA4: dom (xp1 - xm1) = (dom xp1) /\ (dom xm1) by VALUED_1:12
.= dom x1 by A3, B3, C30, FINSEQ_1:def 3, XXX2 ;
for k being Nat st k in dom x1 holds
(xp1 - xm1) . k = x1 . k

proof

let k be Nat; :: thesis:
assume A6: k in dom x1 ; :: thesis:
k in (dom xp1) /\ (dom xm1) by A30, B30, C30, A6;
then PA8: k in dom (xp1 - xm1) by VALUED_1:12;
A80: k in dom (canFS Omega) by C3, P1, A6, FUNCT_2:def 1;
reconsider z = M . {((canFS Omega) . k)} as Element of REAL by CFSD, C3, P1, A6, XD0;
A9: xp1 . k = (R_EAL ((max+ f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by XB7, A30, C30, A6
.= ((max+ f) . ((canFS Omega) . k)) * z by EXTREAL1:13 ;
A10: xm1 . k = (R_EAL ((max- f) . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by XA7, B30, C30, A6
.= ((max- f) . ((canFS Omega) . k)) * z by EXTREAL1:13 ;
(canFS Omega) . k in rng (canFS Omega) by A80, FUNCT_1:12;
then (canFS Omega) . k in Omega ;
then A11: (canFS Omega) . k in dom f by FUNCT_2:def 1;
A12: f = (max+ f) - (max- f) by MESFUNC6:42;
thus (xp1 - xm1) . k = (((max+ f) . ((canFS Omega) . k)) * z) - (((max- f) . ((canFS Omega) . k)) * z) by A9, A10, VALUED_1:13, PA8
.= (((max+ f) . ((canFS Omega) . k)) - ((max- f) . ((canFS Omega) . k))) * z
.= (f . ((canFS Omega) . k)) * z by VALUED_1:13, A11, A12
.= (R_EAL (f . ((canFS Omega) . k))) * (M . {((canFS Omega) . k)}) by EXTREAL1:13
.= x1 . k by C7, A6 ; :: thesis:

end;

hence x1 = xp1 - xm1 by FINSEQ_1:17, AA4; :: thesis:

end;

UU1: dom Fm = dom am by LmX2, R1;
UU2: for n being Nat st n in dom Fm holds
for x being set st x in Fm . n holds
(max- f) . x = am . n

proof

let n be Nat; :: thesis:
assume Z: 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 Z, R1;
then x = (canFS (dom (max- f))) . n by TARSKI:def 1;
hence (max- f) . x = am . n by Z, UU1, FUNCT_1:22; :: thesis:

end;

C5: Integral M,f = Integral M,((max+ f) - (max- f)) by MESFUNC6:42
.= (Sum xp) - (Sum xm) by A5, MES43, B1, B2, B3, R1, XDm, UU1, UU2, P7
.= (Sum xp1) - (Sum xm1) by C51, C52, SUPINF_2:5
.= Sum (xp1 - xm1) by INTEGRA5:2, C54
.= Sum x by MESFUNC3:2, C53 ;
C61: len x = len F by C30, FINSEQ_1:def 3;
dom (canFS (dom f)) = Seg (len F) by FINSEQ_1:def 3, P1;
then len F = len (canFS (dom f)) by FINSEQ_1:def 3;
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 C5, C61, XD0, UPROOTS:5, C7; :: thesis: