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 = (R_EAL (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 = (R_EAL (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 = (R_EAL (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 = (R_EAL (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 = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) implies Integral M,f = Sum x )
assume AS: ( 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 = (R_EAL (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
P1: ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds
F . k = {(s . 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 Lm9A4, AS;
set fp = max+ f;
set fm = max- f;
XSD: dom x = Seg (len s) by AS, FINSEQ_1:def 3
.= dom F by P1, FINSEQ_1:def 3 ;
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 L = len F;
CC: dom F = Seg (len F) by FINSEQ_1:def 3;
defpred S1[ Nat, set ] means for x being set st x in F . $1 holds
$2 = (max+ f) . x;
AP1: 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 P0: k in Seg (len F) ; :: thesis: ex y being Element of REAL st S1[k,y]
take y = (max+ f) . (s . k); :: thesis: S1[k,y]
F . k = {(s . k)} by P1, CC, P0;
hence S1[k,y] by TARSKI:def 1; :: thesis: verum
end;
consider ap being FinSequence of REAL such that
AP2: ( 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(AP1);
 defpred S2[ Nat, set ] means for x being set st x in F . $1 holds
$2 = (max- f) . x;
AM1: 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 P0: k in Seg (len F) ; :: thesis: ex y being Element of REAL st S2[k,y]
take y = (max- f) . (s . k); :: thesis: S2[k,y]
F . k = {(s . k)} by P1, CC, P0;
hence S2[k,y] by TARSKI:def 1; :: thesis: verum
end;
consider am being FinSequence of REAL such that
AM2: ( 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(AM1);
 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;
defpred S3[ Nat, set ] means $2 = (R_EAL (ap . $1)) * ((M * F) . $1);
A1P: 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(A1P);
 A3: ( dom xp = dom F & ( for n being Nat st n in dom xp holds
xp . n = (R_EAL (ap . n)) * ((M * F) . n) ) ) by A30, FINSEQ_1:def 3;
defpred S4[ Nat, set ] means $2 = (R_EAL (am . $1)) * ((M * F) . $1);
B1P: 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
B30: ( 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(B1P);
 B3: ( dom xm = dom F & ( for n being Nat st n in dom xm holds
xm . n = (R_EAL (am . n)) * ((M * F) . n) ) ) by B30, FINSEQ_1:def 3;
A5: Integral M,(max+ f) = Sum xp by MES43, A1, A2, A30, P1, CC, AP2, XDp;
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 XD0, RFUNCT_3:def 11 ;
K9: E = Omega /\ Omega by K8, XD0, RFUNCT_3:def 10, 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 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:12;
then {(s . n)} c= Omega by ZFMISC_1:37;
hence M . {(s . n)} in REAL by Lm9A2, AS; :: thesis: verum
end;
x is FinSequence of REAL
proof
now
let y be set ; :: 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
C71: ( n in dom x & y = x . n ) by PARTFUN1:26;
reconsider w = f . (s . n) as Element of REAL ;
reconsider z = M . {(s . n)} as Element of REAL by CFSD, XSD, P1, C71;
x . n = (R_EAL (f . (s . n))) * (M . {(s . n)}) by AS, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis: verum
end;
hence rng x c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis: verum
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) . (s . n))) * (M . {(s . n)})
proof
let n be Nat; :: thesis: ( n in dom xp implies xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) )
assume C71: n in dom xp ; :: thesis: xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)})
F . n = {(s . n)} by P1, A3, C71;
then PC73: s . n in F . n by TARSKI:def 1;
C74: (M * F) . n = M . (F . n) by FUNCT_1:23, A3, C71
.= M . {(s . n)} by P1, A3, C71 ;
thus xp . n = (R_EAL (ap . n)) * ((M * F) . n) by A30, C71
.= (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) by A30, AP2, C71, PC73, C74 ; :: thesis: verum
end;
xp is FinSequence of REAL
proof
now
let y be set ; :: 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
C71: ( n in dom xp & y = xp . n ) by PARTFUN1:26;
reconsider w = (max+ f) . (s . n) as Element of REAL ;
reconsider z = M . {(s . n)} as Element of REAL by CFSD, P1, A3, C71;
xp . n = (R_EAL ((max+ f) . (s . n))) * (M . {(s . n)}) by XB7, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis: verum
end;
hence rng xp c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis: verum
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) . (s . n))) * (M . {(s . n)})
proof
let n be Nat; :: thesis: ( n in dom xm implies xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) )
assume C71: n in dom xm ; :: thesis: xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)})
F . n = {(s . n)} by P1, B3, C71;
then PC73: s . n in F . n by TARSKI:def 1;
C74: (M * F) . n = M . (F . n) by FUNCT_1:23, B3, C71
.= M . {(s . n)} by P1, B3, C71 ;
thus xm . n = (R_EAL (am . n)) * ((M * F) . n) by B30, C71
.= (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) by B30, AM2, C71, PC73, C74 ; :: thesis: verum
end;
xm is FinSequence of REAL
proof
now
let y be set ; :: 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
C71: ( n in dom xm & y = xm . n ) by PARTFUN1:26;
reconsider w = (max- f) . (s . n) as Element of REAL ;
reconsider z = M . {(s . n)} as Element of REAL by CFSD, B3, C71, P1;
xm . n = (R_EAL ((max- f) . (s . n))) * (M . {(s . n)}) by XA7, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis: verum
end;
hence rng xm c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis: verum
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 XSD, A3, B3 ;
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 )
assume A6: k in dom x1 ; :: thesis: (xp1 - xm1) . k = x1 . k
k in (dom xp1) /\ (dom xm1) by XSD, A3, B3, A6;
then PA8: k in dom (xp1 - xm1) by VALUED_1:12;
reconsider z = M . {(s . k)} as Element of REAL by CFSD, XSD, P1, A6;
A9: xp1 . k = (R_EAL ((max+ f) . (s . k))) * (M . {(s . k)}) by XB7, XSD, A3, A6
.= ((max+ f) . (s . k)) * z by EXTREAL1:13 ;
A10: xm1 . k = (R_EAL ((max- f) . (s . k))) * (M . {(s . k)}) by XA7, XSD, B3, A6
.= ((max- f) . (s . k)) * z by EXTREAL1:13 ;
s . k in rng s by XSD, P1, A6, FUNCT_1:12;
then s . k in Omega ;
then A11: s . k in dom f by FUNCT_2:def 1;
A12: f = (max+ f) - (max- f) by MESFUNC6:42;
thus (xp1 - xm1) . k = (((max+ f) . (s . k)) * z) - (((max- f) . (s . k)) * z) by A9, A10, VALUED_1:13, PA8
.= (((max+ f) . (s . k)) - ((max- f) . (s . k))) * z
.= (f . (s . k)) * z by VALUED_1:13, A11, A12
.= (R_EAL (f . (s . k))) * (M . {(s . k)}) by EXTREAL1:13
.= x1 . k by AS, A6 ; :: thesis: verum
end;
hence x1 = xp1 - xm1 by FINSEQ_1:17, AA4; :: thesis: verum
end;
thus Integral M,f = Integral M,((max+ f) - (max- f)) by MESFUNC6:42
.= (Sum xp) - (Sum xm) by A5, MES43, B1, B2, B30, XDm, P1, AM2, CC, P7
.= (Sum xp1) - (Sum xm1) by C51, C52, SUPINF_2:5
.= Sum (xp1 - xm1) by INTEGRA5:2, C54
.= Sum x by MESFUNC3:2, C53 ; :: thesis: verum