let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let A be Element of S; :: thesis:
let E be SetSequence of S; :: thesis:
assume that
A1: f is nonnegative and
A2: f is A -measurable and
A3: A = dom f and
A4: E is disjoint_valued and
A5: A = Union E ; :: thesis:
A6: dom E = NAT by FUNCT_2:def 1;
A7: rng E c= S ;
defpred S₁[ Element of NAT , PartFunc of X,ExtREAL] means ( dom $2 = dom f & ( for x being Element of X st x in E . $1 holds
$2 . x = f . x ) & ( for x being Element of X st not x in E . $1 holds
$2 . x = 0 ) );
A8: for n being Element of NAT holds E . n c= dom f

let n be Element of NAT ; :: thesis:
E . n c= union (rng E) by A6, ZFMISC_1:74, FUNCT_1:3;
hence E . n c= dom f by A3, A5, CARD_3:def 4; :: thesis:

end;

A9: for n being Element of NAT ex g being Element of PFuncs (X,ExtREAL) st S₁[n,g]

proof

let n be Element of NAT ; :: thesis:
defpred S₂[ object , object ] means ( ( $1 in E . n implies $2 = f . $1 ) & ( not $1 in E . n implies $2 = 0 ) );
A10: for x, y1, y2 being object st x in dom f & S₂[x,y1] & S₂[x,y2] holds
y1 = y2 ;
A11: for x being object st x in dom f holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis:
assume x in dom f ; :: thesis:
( x in E . n or not x in E . n ) ;
hence ex y being object st S₂[x,y] ; :: thesis:

end;

consider g being Function such that
A12: ( dom g = dom f & ( for x being object st x in dom f holds
S₂[x,g . x] ) ) from FUNCT_1:sch 2(A10, A11);

now :: thesis:

let y be object ; :: thesis:
assume y in rng g ; :: thesis:
then consider x being object such that
A13: ( x in dom g & g . x = y ) by FUNCT_1:def 3;

per cases ;

suppose x in E . n ; :: thesis:

then A14: g . x = f . x by A12, A13;
f . x in rng f by A12, A13, FUNCT_1:3;
hence y in ExtREAL by A13, A14; :: thesis:

end;

suppose not x in E . n ; :: thesis:

then g . x = 0 by A12, A13;
then g . x in REAL by XREAL_0:def 1;
hence y in ExtREAL by A13, XBOOLE_0:def 3, XXREAL_0:def 4; :: thesis:

end;

then rng g c= ExtREAL ;
then reconsider g = g as Element of PFuncs (X,ExtREAL) by A12, PARTFUN1:def 3;
take g ; :: thesis:
A15: for x being Element of X st x in E . n holds
g . x = f . x

proof

let x be Element of X; :: thesis:
A16: E . n c= dom f by A8;
assume x in E . n ; :: thesis:
hence g . x = f . x by A12, A16; :: thesis:

end;

for x being Element of X st not x in E . n holds
g . x = 0

proof

let x be Element of X; :: thesis:
assume A17: not x in E . n ; :: thesis:
( x in dom f or not x in dom f ) ;
hence g . x = 0 by A12, A17, FUNCT_1:def 2; :: thesis:

end;

hence S₁[n,g] by A12, A15; :: thesis:

end;

consider F being sequence of (PFuncs (X,ExtREAL)) such that
A18: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A9);
for n being Nat
for x being Element of X holds (F . n) . x >= 0

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
A19: n is Element of NAT by ORDINAL1:def 12;

per cases ;

suppose x in E . n ; :: thesis:

then (F . n) . x = f . x by A18, A19;
hence (F . n) . x >= 0 by A1, SUPINF_2:51; :: thesis:

end;

suppose not x in E . n ; :: thesis:

hence (F . n) . x >= 0 by A18, A19; :: thesis:

end;

then A20: for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) ;

now :: thesis:

let n, m be Nat; :: thesis:
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
then ( dom (F . n) = dom f & dom (F . m) = dom f ) by A18;
hence dom (F . n) = dom (F . m) ; :: thesis:

end;

then A21: F is with_the_same_dom by MESFUNC8:def 2;
A22: for n being Nat holds
( F . n is nonnegative & F . n is A -measurable )

proof

let n be Nat; :: thesis:
A23: n is Element of NAT by ORDINAL1:def 12;
then reconsider En = E . n as Element of S by A6, A7, FUNCT_1:3;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (F . n) ; :: thesis:
then ( ( x in E . n implies (F . n) . x = f . x ) & ( not x in E . n implies (F . n) . x = 0 ) ) by A23, A18;
hence (F . n) . x >= 0 by A1, SUPINF_2:51; :: thesis:

end;

hence F . n is nonnegative by SUPINF_2:52; :: thesis:
A24: E . n c= A by A3, A8, A23;
for r being Real holds A /\ (less_dom ((F . n),r)) in S

proof

let r be Real; :: thesis:

per cases ;

suppose A25: r <= 0 ; :: thesis:

for x being object holds not x in A /\ (less_dom ((F . n),r))

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A26: x in A /\ (less_dom ((F . n),r)) ; :: thesis:
then A27: ( x in A & x in less_dom ((F . n),r) ) by XBOOLE_0:def 4;
( ( x in E . n implies (F . n) . x = f . x ) & ( not x in E . n implies (F . n) . x = 0 ) ) by A23, A18, A26;
then (F . n) . x >= r by A25, A1, SUPINF_2:51;
hence contradiction by A27, MESFUNC1:def 11; :: thesis:

end;

then A /\ (less_dom ((F . n),r)) = {} by XBOOLE_0:def 1;
hence A /\ (less_dom ((F . n),r)) in S by MEASURE1:7; :: thesis:

end;

suppose A28: r > 0 ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in A /\ (less_dom ((F . n),r)) ; :: thesis:
then A29: ( x in A & x in less_dom ((F . n),r) ) by XBOOLE_0:def 4;
then A30: ( x in dom (F . n) & (F . n) . x < r ) by MESFUNC1:def 11;
thus x in (A \ En) \/ (En /\ (less_dom (f,r))) :: thesis:

proof

per cases ;

suppose not x in En ; :: thesis:

then x in A \ En by A29, XBOOLE_0:def 5;
hence x in (A \ En) \/ (En /\ (less_dom (f,r))) by XBOOLE_0:def 3; :: thesis:

end;

suppose A31: x in En ; :: thesis:

then (F . n) . x = f . x by A23, A18;
then x in less_dom (f,r) by A3, A29, A30, MESFUNC1:def 11;
then x in En /\ (less_dom (f,r)) by A31, XBOOLE_0:def 4;
hence x in (A \ En) \/ (En /\ (less_dom (f,r))) by XBOOLE_0:def 3; :: thesis:

end;

then A32: A /\ (less_dom ((F . n),r)) c= (A \ En) \/ (En /\ (less_dom (f,r))) ;

now :: thesis:

let x be object ; :: thesis:
assume A33: x in (A \ En) \/ (En /\ (less_dom (f,r))) ; :: thesis:

per cases by A33, XBOOLE_0:def 3;

suppose x in A \ En ; :: thesis:

then A34: ( x in A & not x in En ) by XBOOLE_0:def 5;
then A35: x in dom (F . n) by A23, A18, A3;
(F . n) . x = 0 by A23, A18, A34;
then x in less_dom ((F . n),r) by A28, A35, MESFUNC1:def 11;
hence x in A /\ (less_dom ((F . n),r)) by A34, XBOOLE_0:def 4; :: thesis:

end;

suppose x in En /\ (less_dom (f,r)) ; :: thesis:

then A36: ( x in En & x in less_dom (f,r) ) by XBOOLE_0:def 4;
then f . x < r by MESFUNC1:def 11;
then A37: (F . n) . x < r by A36, A23, A18;
x in A by A36, A24;
then x in dom (F . n) by A3, A23, A18;
then x in less_dom ((F . n),r) by A37, MESFUNC1:def 11;
hence x in A /\ (less_dom ((F . n),r)) by A36, A24, XBOOLE_0:def 4; :: thesis:

end;

then (A \ En) \/ (En /\ (less_dom (f,r))) c= A /\ (less_dom ((F . n),r)) ;
then A38: A /\ (less_dom ((F . n),r)) = (A \ En) \/ (En /\ (less_dom (f,r))) by A32, XBOOLE_0:def 10;
f is En -measurable by A2, A3, A8, A23, MESFUNC1:30;
then ( A \ En in S & En /\ (less_dom (f,r)) in S ) by MESFUNC1:def 16;
hence A /\ (less_dom ((F . n),r)) in S by A38, FINSUB_1:def 1; :: thesis:

end;

hence F . n is A -measurable by MESFUNC1:def 16; :: thesis:

end;

A39: for n being Nat
for x being Element of X st x in E . n holds
for m being Nat st ( m < n or m > n ) holds
(F # x) . m = 0

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume A40: x in E . n ; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
A41: m is Element of NAT by ORDINAL1:def 12;
assume ( m < n or m > n ) ; :: thesis:
then A42: not x in E . m by A40, A4, PROB_2:def 2, XBOOLE_0:3;
(F # x) . m = (F . m) . x by MESFUNC5:def 13;
hence (F # x) . m = 0 by A41, A18, A42; :: thesis:

end;

A43: for n being Nat
for x being Element of X st x in E . n holds
for m being Nat st m < n holds
(Partial_Sums (F # x)) . m = 0

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume A44: x in E . n ; :: thesis:
defpred S₂[ Nat] means ( $1 < n implies (Partial_Sums (F # x)) . $1 = 0 );

now :: thesis:

assume 0 < n ; :: thesis:
then (F # x) . 0 = 0 by A44, A39;
hence (Partial_Sums (F # x)) . 0 = 0 by MESFUNC9:def 1; :: thesis:

end;

then A45: S₂[ 0 ] ;
A46: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A47: S₂[k] ; :: thesis:
assume A48: k + 1 < n ; :: thesis:
A49: k <= k + 1 by NAT_1:11;
A50: (F # x) . (k + 1) = 0 by A48, A39, A44;
(Partial_Sums (F # x)) . (k + 1) = ((Partial_Sums (F # x)) . k) + ((F # x) . (k + 1)) by MESFUNC9:def 1;
hence (Partial_Sums (F # x)) . (k + 1) = 0 by A49, A50, A47, A48, XXREAL_0:2; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A45, A46);
hence for m being Nat st m < n holds
(Partial_Sums (F # x)) . m = 0 ; :: thesis:

end;

A51: for n being Nat
for x being Element of X st x in E . n holds
for m being Nat st m >= n holds
(Partial_Sums (F # x)) . m = f . x

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
A52: n is Element of NAT by ORDINAL1:def 12;
assume A53: x in E . n ; :: thesis:
defpred S₂[ Nat] means ( $1 >= n implies (Partial_Sums (F # x)) . $1 = f . x );

now :: thesis:

assume 0 >= n ; :: thesis:
then A54: n = 0 ;
(Partial_Sums (F # x)) . 0 = (F # x) . 0 by MESFUNC9:def 1;
then (Partial_Sums (F # x)) . 0 = (F . 0) . x by MESFUNC5:def 13;
hence (Partial_Sums (F # x)) . 0 = f . x by A18, A54, A53; :: thesis:

end;

then A55: S₂[ 0 ] ;
A56: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A57: S₂[k] ; :: thesis:
assume A58: k + 1 >= n ; :: thesis:
A59: (Partial_Sums (F # x)) . (k + 1) = ((Partial_Sums (F # x)) . k) + ((F # x) . (k + 1)) by MESFUNC9:def 1;

per cases by A58, XXREAL_0:1;

suppose A60: k + 1 = n ; :: thesis:

then k < n by NAT_1:13;
then A61: (Partial_Sums (F # x)) . k = 0 by A43, A53;
(F # x) . (k + 1) = (F . n) . x by A60, MESFUNC5:def 13;
then (F # x) . (k + 1) = f . x by A18, A53, A52;
hence (Partial_Sums (F # x)) . (k + 1) = f . x by A61, A59, XXREAL_3:4; :: thesis:

end;

suppose A62: k + 1 > n ; :: thesis:

then (F # x) . (k + 1) = 0 by A39, A53;
hence (Partial_Sums (F # x)) . (k + 1) = f . x by A62, A59, A57, NAT_1:13, XXREAL_3:4; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A55, A56);
hence for m being Nat st m >= n holds
(Partial_Sums (F # x)) . m = f . x ; :: thesis:

end;

A63: for x being Element of X st x in A & f . x in REAL holds
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - (f . x)).| < p

proof

let x be Element of X; :: thesis:
assume that
A64: x in A and
A65: f . x in REAL ; :: thesis:
reconsider g = f . x as Real by A65;
x in union (rng E) by A5, A64, CARD_3:def 4;
then consider En being set such that
A66: ( x in En & En in rng E ) by TARSKI:def 4;
consider n being object such that
A67: ( n in dom E & En = E . n ) by A66, FUNCT_1:def 3;
reconsider n = n as Nat by A67;

hereby :: thesis:

let p be Real; :: thesis:
assume A68: 0 < p ; :: thesis:
take n = n; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then ((Partial_Sums (F # x)) . m) - g = (f . x) - g by A66, A67, A51;
then ((Partial_Sums (F # x)) . m) - g = (f . x) + (- (f . x)) by XXREAL_3:def 4;
then ((Partial_Sums (F # x)) . m) - g = 0 by XXREAL_3:7;
hence |.(((Partial_Sums (F # x)) . m) - (f . x)).| < p by A68, EXTREAL1:def 1; :: thesis:

end;

A69: for x being Element of X st x in A & f . x in REAL holds
Partial_Sums (F # x) is convergent_to_finite_number

proof

let x be Element of X; :: thesis:
assume that
A70: x in A and
A71: f . x in REAL ; :: thesis:
reconsider g = f . x as Real by A71;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - g).| < p by A70, A71, A63;
hence Partial_Sums (F # x) is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:

end;

A72: for x being Element of X st x in A & f . x = +infty holds
Partial_Sums (F # x) is convergent_to_+infty

proof

let x be Element of X; :: thesis:
assume that
A73: x in A and
A74: f . x = +infty ; :: thesis:
x in union (rng E) by A5, A73, CARD_3:def 4;
then consider En being set such that
A75: ( x in En & En in rng E ) by TARSKI:def 4;
consider n being object such that
A76: ( n in dom E & En = E . n ) by A75, FUNCT_1:def 3;
reconsider n = n as Nat by A76;

now :: thesis:

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
take n = n; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then (Partial_Sums (F # x)) . m = +infty by A51, A75, A76, A74;
hence g <= (Partial_Sums (F # x)) . m by XXREAL_0:3; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_+infty by MESFUNC5:def 9; :: thesis:

end;

A77: for x being Element of X st x in A holds
F # x is summable

proof

let x be Element of X; :: thesis:
assume A78: x in A ; :: thesis:
f . x >= 0 by A1, SUPINF_2:51;
then ( f . x in REAL or f . x = +infty ) by XXREAL_0:14;
then ( Partial_Sums (F # x) is convergent_to_finite_number or Partial_Sums (F # x) is convergent_to_+infty ) by A78, A69, A72;
hence F # x is summable by MESFUNC9:def 2; :: thesis:

end;

A c= dom (F . 0) by A18, A3;
then consider I being ExtREAL_sequence such that
A79: for n being Nat holds I . n = Integral (M,((F . n) | A)) and
A80: I is summable and
A81: Integral (M,((lim (Partial_Sums F)) | A)) = Sum I by A20, A21, A22, A77, MESFUNC9:def 5, MESFUNC9:51;
A82: for n being Nat holds Integral (M,((F . n) | A)) = Integral (M,(f | (E . n)))

proof

let n be Nat; :: thesis:
A83: n is Element of NAT by ORDINAL1:def 12;
then A84: dom (F . n) = A by A3, A18;
reconsider En = E . n as Element of S by A83, A6, A7, FUNCT_1:3;
set E1 = A \ En;
A85: ( F . n is nonnegative & F . n is A -measurable ) by A22;
then A86: F . n is A \ En -measurable by MESFUNC1:30, XBOOLE_1:36;
(A \ En) \/ En = A \/ En by XBOOLE_1:39;
then A87: (A \ En) \/ En = A by A8, A83, A3, XBOOLE_1:12;
A88: dom ((F . n) | (A \ En)) = (dom (F . n)) /\ (A \ En) by RELAT_1:61;
then A89: dom ((F . n) | (A \ En)) = (A /\ A) \ En by A84, XBOOLE_1:49;
A90: (dom (F . n)) /\ (A \ En) = (A /\ A) \ En by A84, XBOOLE_1:49;
for x being Element of X st x in dom ((F . n) | (A \ En)) holds
((F . n) | (A \ En)) . x = 0

proof

let x be Element of X; :: thesis:
assume A91: x in dom ((F . n) | (A \ En)) ; :: thesis:
then A92: not x in En by A89, XBOOLE_0:def 5;
((F . n) | (A \ En)) . x = (F . n) . x by A91, FUNCT_1:47;
hence ((F . n) | (A \ En)) . x = 0 by A18, A83, A92; :: thesis:

end;

then A93: integral+ (M,((F . n) | (A \ En))) = 0 by A88, A90, A86, MESFUNC5:42, MESFUNC5:87;
A94: dom (f | En) = (dom f) /\ En by RELAT_1:61;
A95: dom ((F . n) | En) = En by A8, A83, A84, A3, RELAT_1:62;
A96: dom (f | En) = En by A8, A83, RELAT_1:62;

now :: thesis:

let x be Element of X; :: thesis:
assume A97: x in dom ((F . n) | En) ; :: thesis:
then ((F . n) | En) . x = (F . n) . x by A95, FUNCT_1:49;
then ((F . n) | En) . x = f . x by A83, A18, A97, A95;
hence ((F . n) | En) . x = (f | En) . x by A97, A95, FUNCT_1:49; :: thesis:

end;

then A98: (F . n) | En = f | En by A95, A96, PARTFUN1:5;
f is En -measurable by A2, A8, A83, A3, MESFUNC1:30;
then A99: f | En is En -measurable by A94, A96, MESFUNC5:42;
integral+ (M,((F . n) | ((A \ En) \/ En))) = (integral+ (M,((F . n) | (A \ En)))) + (integral+ (M,((F . n) | En))) by A84, A85, MESFUNC5:81, XBOOLE_1:79;
then integral+ (M,((F . n) | A)) = integral+ (M,((F . n) | En)) by A87, A93, XXREAL_3:4;
then Integral (M,((F . n) | A)) = integral+ (M,(f | En)) by A98, A84, A85, MESFUNC5:88;
hence Integral (M,((F . n) | A)) = Integral (M,(f | (E . n))) by A96, A99, A1, MESFUNC5:15, MESFUNC5:88; :: thesis:

end;

for n being object st n in dom I holds
0 <= I . n

proof

let n be object ; :: thesis:
assume A100: n in dom I ; :: thesis:
then A101: E . n is Element of S by A6, A7, FUNCT_1:3;
I . n = Integral (M,((F . n) | A)) by A79, A100;
then I . n = Integral (M,(f | (E . n))) by A82, A100;
hence I . n >= 0 by A1, A2, A3, A101, MESFUNC5:92; :: thesis:

end;

then reconsider I = I as nonnegative ExtREAL_sequence by SUPINF_2:52;
take I ; :: thesis:
thus for n being Nat holds I . n = Integral (M,(f | (E . n))) :: thesis:

proof

let n be Nat; :: thesis:
I . n = Integral (M,((F . n) | A)) by A79;
hence I . n = Integral (M,(f | (E . n))) by A82; :: thesis:

end;

thus I is summable by A80; :: thesis:
for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty )

proof

let n, m be Nat; :: thesis:
assume A102: n <> m ; :: thesis:
A103: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;

hereby :: thesis:

let x be set ; :: thesis:
( ( not x in E . n & not x in E . m ) or not x in E . m or not x in E . n ) by A102, A4, PROB_2:def 2, XBOOLE_0:3;
hence ( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) by A18, A103; :: thesis:

end;

then A104: F is additive by MESFUNC9:def 5;
for n, m being Nat holds dom (F . n) = dom (F . m)

proof

let n, m be Nat; :: thesis:
( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;
then ( dom (F . n) = dom f & dom (F . m) = dom f ) by A18;
hence dom (F . n) = dom (F . m) ; :: thesis:

end;

then A105: F is with_the_same_dom by MESFUNC8:def 2;
A106: dom f = dom (F . 0) by A18;
dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0) by MESFUNC8:def 9;
then A107: dom (lim (Partial_Sums F)) = dom (F . 0) by MESFUNC9:def 4;
for x being Element of X st x in dom f holds
f . x = ((lim (Partial_Sums F)) | A) . x

proof

let x be Element of X; :: thesis:
assume A108: x in dom f ; :: thesis:
A109: f . x >= 0 by A1, SUPINF_2:51;

now :: thesis:

per cases by A109, XXREAL_0:14;

suppose A110: f . x in REAL ; :: thesis:

then reconsider g = f . x as Real ;
A111: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - g).| < p by A108, A3, A63, A110;
Partial_Sums (F # x) is convergent_to_finite_number by A108, A3, A69, A110;
hence f . x = lim (Partial_Sums (F # x)) by A111, MESFUNC5:def 12; :: thesis:

end;

suppose A112: f . x = +infty ; :: thesis:

then Partial_Sums (F # x) is convergent_to_+infty by A108, A3, A72;
hence f . x = lim (Partial_Sums (F # x)) by A112, MESFUNC5:def 12; :: thesis:

end;

then f . x = Sum (F # x) by MESFUNC9:def 3;
then f . x = lim ((Partial_Sums F) # x) by A3, A77, A104, A105, A106, A108, MESFUNC9:34;
hence f . x = ((lim (Partial_Sums F)) | A) . x by A3, A108, A106, A107, MESFUNC8:def 9; :: thesis:

end;

hence Integral (M,f) = Sum I by A3, A81, A106, A107, PARTFUN1:5; :: thesis: