let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
assume that
A1: E = dom (F . 0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) and
A5: for x being Element of X st x in E holds
F # x is summable ; :: thesis:
consider FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) such that
A6: for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonnegative ) & ( for j, k being Nat st j <= k holds
for x being Element of X st x in dom (F . n) holds
((FF . n) . j) . x <= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) ) by A1, A3, A4, Th49;
defpred S₁[ Element of NAT , Element of NAT , set ] means for n, m being Nat st n = $1 & m = $2 holds
$3 = (FF . n) . m;
A7: for i1, j1 being Element of NAT ex F1 being Element of PFuncs (X,ExtREAL) st S₁[i1,j1,F1]

proof

let i1, j1 be Element of NAT ; :: thesis:
reconsider i = i1, j = j1 as Nat ;
reconsider F1 = (FF . i) . j as Element of PFuncs (X,ExtREAL) by PARTFUN1:45;
take F1 ; :: thesis:
thus S₁[i1,j1,F1] ; :: thesis:

end;

consider FF2 being Function of [:NAT,NAT:],(PFuncs (X,ExtREAL)) such that
A8: for i, j being Element of NAT holds S₁[i,j,FF2 . (i,j)] from BINOP_1:sch 3(A7);
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (Partial_Sums (ProjMap2 (FF2,$1))) . $1;
consider P being Functional_Sequence of X,ExtREAL such that
A9: for k being Nat holds P . k = H₁(k) from SEQFUNC:sch 1();
A10: for n being Nat holds
( ( for m being Nat holds
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S ) ) & ProjMap1 (FF2,n) is additive & ProjMap2 (FF2,n) is additive & ProjMap1 (FF2,n) is with_the_same_dom & ProjMap2 (FF2,n) is with_the_same_dom )

proof

let n be Nat; :: thesis:

A11: now :: thesis:

let m be Nat; :: thesis:
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
A12: (ProjMap1 (FF2,n)) . m = FF2 . (n,m) by Def8;
A13: FF2 . (n1,m1) = (FF . n1) . m by A8;
A14: dom (F . m1) = dom (F . 0) by A3;
A15: (ProjMap2 (FF2,n)) . m = FF2 . (m,n) by Def9;
A16: FF2 . (m1,n1) = (FF . m1) . n by A8;
dom (F . n1) = dom (F . m1) by A3;
hence ( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E ) by A1, A6, A12, A15, A13, A16, A14; :: thesis:
thus ( (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S ) by A6, A12, A15, A13, A16; :: thesis:

end;

for i1, j1 being Nat holds
( dom ((ProjMap1 (FF2,n)) . i1) = dom ((ProjMap1 (FF2,n)) . j1) & dom ((ProjMap2 (FF2,n)) . i1) = dom ((ProjMap2 (FF2,n)) . j1) )

proof

let i1, j1 be Nat; :: thesis:
A17: dom ((ProjMap2 (FF2,n)) . i1) = E by A11;
dom ((ProjMap1 (FF2,n)) . i1) = E by A11;
hence ( dom ((ProjMap1 (FF2,n)) . i1) = dom ((ProjMap1 (FF2,n)) . j1) & dom ((ProjMap2 (FF2,n)) . i1) = dom ((ProjMap2 (FF2,n)) . j1) ) by A11, A17; :: thesis:

end;

hence ( ( for m being Nat holds
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S ) ) & ProjMap1 (FF2,n) is additive & ProjMap2 (FF2,n) is additive & ProjMap1 (FF2,n) is with_the_same_dom & ProjMap2 (FF2,n) is with_the_same_dom ) by A11, Th35; :: thesis:

end;

for n, m being Nat holds dom (P . n) = dom (P . m)

proof

let n, m be Nat; :: thesis:
A18: ProjMap2 (FF2,n) is with_the_same_dom by A10;
A19: dom (P . n) = dom ((Partial_Sums (ProjMap2 (FF2,n))) . n) by A9;
ProjMap2 (FF2,n) is additive by A10;
then dom (P . n) = dom ((ProjMap2 (FF2,n)) . 0) by A18, A19, Th29;
then dom (P . n) = E by A10;
then A20: dom (P . n) = dom ((ProjMap2 (FF2,m)) . 0) by A10;
A21: ProjMap2 (FF2,m) is with_the_same_dom by A10;
ProjMap2 (FF2,m) is additive by A10;
then dom (P . n) = dom ((Partial_Sums (ProjMap2 (FF2,m))) . m) by A21, A20, Th29;
hence dom (P . n) = dom (P . m) by A9; :: thesis:

end;

then reconsider P = P as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
dom (lim P) = dom (P . 0) by MESFUNC8:def 9;
then dom (lim P) = dom ((Partial_Sums (ProjMap2 (FF2,0))) . 0) by A9;
then dom (lim P) = dom ((ProjMap2 (FF2,0)) . 0) by Def4;
then dom (lim P) = dom (FF2 . (0,0)) by Def9;
then A22: dom (lim P) = dom ((FF . 0) . 0) by A8;
then A23: dom (lim P) = dom (F . 0) by A6;
A24: for k, m being Nat
for x being Element of X st x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x

proof

let k, m be Nat; :: thesis:
let x be Element of X; :: thesis:
reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 12;
assume x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) ; :: thesis:
then x in dom (F . 0) by XBOOLE_0:def 4;
then A25: x in dom (F . m) by A3;
(FF . m1) # x is non-decreasing

proof

let j, k be ExtReal; :: according to VALUED_0:def 15 :: thesis:
assume that
A26: j in dom ((FF . m1) # x) and
A27: k in dom ((FF . m1) # x) and
A28: j <= k ; :: thesis:
reconsider j = j, k = k as Element of NAT by A26, A27;
A29: ((FF . m1) # x) . k = ((FF . m1) . k) . x by MESFUNC5:def 13;
((FF . m1) # x) . j = ((FF . m1) . j) . x by MESFUNC5:def 13;
hence ((FF . m1) # x) . j <= ((FF . m1) # x) . k by A6, A25, A28, A29; :: thesis:

end;

then lim ((FF . m1) # x) = sup ((FF . m1) # x) by RINFSUP2:37;
then ((FF . m1) # x) . k1 <= lim ((FF . m1) # x) by RINFSUP2:23;
then A30: ((FF . m1) # x) . k <= (F . m1) . x by A6, A25;
(ProjMap2 (FF2,k)) . m = FF2 . (m1,k1) by Def9;
then (ProjMap2 (FF2,k)) . m = (FF . m) . k by A8;
hence ((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x by A30, MESFUNC5:def 13; :: thesis:

end;

A31: for x being Element of X
for k being Element of NAT st x in dom (lim P) holds
(P # x) . k <= ((Partial_Sums F) # x) . k

proof

let x be Element of X; :: thesis:
let k be Element of NAT ; :: thesis:
assume A32: x in dom (lim P) ; :: thesis:
dom ((ProjMap2 (FF2,k)) . 0) = E by A10;
then A33: x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) by A1, A6, A22, A32;
A34: ProjMap2 (FF2,k) is with_the_same_dom by A10;
(P # x) . k = (P . k) . x by MESFUNC5:def 13;
then A35: (P # x) . k = ((Partial_Sums (ProjMap2 (FF2,k))) . k) . x by A9;
A36: for m being Nat
for x being Element of X st x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x by A24;
ProjMap2 (FF2,k) is additive by A10;
then ((Partial_Sums (ProjMap2 (FF2,k))) . k) . x <= ((Partial_Sums F) . k) . x by A2, A3, A33, A34, A36, Th42;
hence (P # x) . k <= ((Partial_Sums F) # x) . k by A35, MESFUNC5:def 13; :: thesis:

end;

dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0) by MESFUNC8:def 9;
then A37: dom (lim (Partial_Sums F)) = E by A1, Def4;
A38: for n, m being Nat holds
( (ProjMap1 (FF2,n)) . m is nonnegative & (ProjMap2 (FF2,n)) . m is nonnegative )

proof

let n, m be Nat; :: thesis:
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
(ProjMap1 (FF2,n)) . m = FF2 . (n1,m1) by Def8;
then (ProjMap1 (FF2,n)) . m = (FF . n) . m by A8;
hence (ProjMap1 (FF2,n)) . m is nonnegative by A6; :: thesis:
(ProjMap2 (FF2,n)) . m = FF2 . (m1,n1) by Def9;
then (ProjMap2 (FF2,n)) . m = (FF . m) . n by A8;
hence (ProjMap2 (FF2,n)) . m is nonnegative by A6; :: thesis:

end;

A39: for n being Element of NAT
for x being Element of X st x in E holds
( (ProjMap1 (FF2,n)) # x is convergent & (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) )

proof

let n be Element of NAT ; :: thesis:
reconsider n1 = n as Nat ;
let x be Element of X; :: thesis:
assume A40: x in E ; :: thesis:
for k being Nat ex m being Nat st
( k <= m & ((ProjMap1 (FF2,n)) # x) . m > - 1 )

proof

let k be Nat; :: thesis:
take m = k; :: thesis:
A41: ((ProjMap1 (FF2,n)) # x) . m = ((ProjMap1 (FF2,n)) . m) . x by MESFUNC5:def 13;
(ProjMap1 (FF2,n)) . m is nonnegative by A38;
hence ( k <= m & ((ProjMap1 (FF2,n)) # x) . m > - 1 ) by A41, SUPINF_2:39; :: thesis:

end;

then A42: not (ProjMap1 (FF2,n)) # x is convergent_to_-infty ;
A43: E = dom (F . n1) by A1, A3;
(ProjMap1 (FF2,n)) # x is non-decreasing

proof

let i, j be ExtReal; :: according to VALUED_0:def 15 :: thesis:
assume that
A44: i in dom ((ProjMap1 (FF2,n)) # x) and
A45: j in dom ((ProjMap1 (FF2,n)) # x) and
A46: i <= j ; :: thesis:
reconsider i1 = i, j1 = j as Element of NAT by A44, A45;
A47: ((ProjMap1 (FF2,n)) # x) . i1 = ((ProjMap1 (FF2,n)) . i1) . x by MESFUNC5:def 13;
(ProjMap1 (FF2,n)) . i1 = FF2 . (n,i1) by Def8;
then A48: (ProjMap1 (FF2,n)) . i1 = (FF . n1) . i1 by A8;
A49: ((ProjMap1 (FF2,n)) # x) . j1 = ((ProjMap1 (FF2,n)) . j1) . x by MESFUNC5:def 13;
A50: (ProjMap1 (FF2,n)) . j1 = FF2 . (n,j1) by Def8;
((FF . n1) . i1) . x <= ((FF . n1) . j1) . x by A6, A43, A40, A46;
hence ((ProjMap1 (FF2,n)) # x) . i <= ((ProjMap1 (FF2,n)) # x) . j by A8, A47, A49, A48, A50; :: thesis:

end;

hence A51: (ProjMap1 (FF2,n)) # x is convergent by RINFSUP2:37; :: thesis:

per cases ) # x is convergent_to_finite_number or (ProjMap1 (FF2,n)) # x is convergent_to_+infty ) by A51, A42;

suppose A52: (ProjMap1 (FF2,n)) # x is convergent_to_finite_number ; :: thesis:

then A53: not (ProjMap1 (FF2,n)) # x is convergent_to_-infty by MESFUNC5:51;
not (ProjMap1 (FF2,n)) # x is convergent_to_+infty by A52, MESFUNC5:50;
then consider lP being Real such that
A54: lim ((ProjMap1 (FF2,n)) # x) = lP and
A55: for p being Real st 0 < p holds
ex nn being Nat st
for mm being Nat st nn <= mm holds
|.((((ProjMap1 (FF2,n)) # x) . mm) - (lim ((ProjMap1 (FF2,n)) # x))).| < p and
(ProjMap1 (FF2,n)) # x is convergent_to_finite_number by A51, A53, MESFUNC5:def 12;
A56: for p being Real st 0 < p holds
ex nn being Nat st
for mm being Nat st nn <= mm holds
|.((((FF . n1) # x) . mm) - lP).| < p

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider nn being Nat such that
A57: for mm being Nat st nn <= mm holds
|.((((ProjMap1 (FF2,n)) # x) . mm) - (lim ((ProjMap1 (FF2,n)) # x))).| < p by A55;
take nn ; :: thesis:
let mm be Nat; :: thesis:
assume A58: nn <= mm ; :: thesis:
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
(ProjMap1 (FF2,n)) . mm = FF2 . (n,mm) by Def8;
then A59: (ProjMap1 (FF2,n)) . mm = (FF . n1) . mm1 by A8;
((ProjMap1 (FF2,n)) # x) . mm = ((ProjMap1 (FF2,n)) . mm) . x by MESFUNC5:def 13;
then ((FF . n1) # x) . mm = ((ProjMap1 (FF2,n)) # x) . mm by A59, MESFUNC5:def 13;
hence |.((((FF . n1) # x) . mm) - lP).| < p by A54, A57, A58; :: thesis:

end;

then A60: (FF . n1) # x is convergent_to_finite_number ;
reconsider lP = lP as R_eal by XXREAL_0:def 1;
(FF . n1) # x is convergent by A60;
then lim ((FF . n1) # x) = lP by A56, A60, MESFUNC5:def 12;
hence (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) by A6, A43, A40, A54; :: thesis:

end;

suppose A61: (ProjMap1 (FF2,n)) # x is convergent_to_+infty ; :: thesis:

for g being Real st 0 < g holds
ex nn being Nat st
for mm being Nat st nn <= mm holds
g <= ((FF . n1) # x) . mm

proof

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
then consider nn being Nat such that
A62: for mm being Nat st nn <= mm holds
g <= ((ProjMap1 (FF2,n)) # x) . mm by A61;
take nn ; :: thesis:
let mm be Nat; :: thesis:
assume nn <= mm ; :: thesis:
then A63: g <= ((ProjMap1 (FF2,n)) # x) . mm by A62;
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
(ProjMap1 (FF2,n)) . mm = FF2 . (n,mm1) by Def8;
then A64: (ProjMap1 (FF2,n)) . mm = (FF . n) . mm by A8;
((ProjMap1 (FF2,n)) # x) . mm = ((ProjMap1 (FF2,n)) . mm) . x by MESFUNC5:def 13;
hence g <= ((FF . n1) # x) . mm by A63, A64, MESFUNC5:def 13; :: thesis:

end;

then A65: (FF . n1) # x is convergent_to_+infty ;
then (FF . n1) # x is convergent ;
then A66: lim ((FF . n1) # x) = +infty by A65, MESFUNC5:def 12;
lim ((ProjMap1 (FF2,n)) # x) = +infty by A51, A61, MESFUNC5:def 12;
hence (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) by A6, A43, A40, A66; :: thesis:

end;

A67: dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0) by MESFUNC8:def 9;
then A68: dom (lim (Partial_Sums F)) = E by A1, Def4;
A69: for n being Nat holds dom (P . n) = dom (lim (Partial_Sums F))

proof

let n be Nat; :: thesis:
A70: ProjMap2 (FF2,n) is with_the_same_dom by A10;
A71: dom (P . n) = dom ((Partial_Sums (ProjMap2 (FF2,n))) . n) by A9;
ProjMap2 (FF2,n) is additive by A10;
then dom (P . n) = dom ((ProjMap2 (FF2,n)) . 0) by A70, A71, Th29;
hence dom (P . n) = dom (lim (Partial_Sums F)) by A68, A10; :: thesis:

end;

A72: for n, m being Nat st n <= m holds
for i being Nat
for x being Element of X st x in E holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x

proof

let n, m be Nat; :: thesis:
assume A73: n <= m ; :: thesis:
let i be Nat; :: thesis:
let x be Element of X; :: thesis:
reconsider i1 = i, n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
((ProjMap2 (FF2,n)) . i) . x = (FF2 . (i1,n1)) . x by Def9;
then A74: ((ProjMap2 (FF2,n)) . i) . x = ((FF . i) . n) . x by A8;
((ProjMap2 (FF2,m)) . i) . x = (FF2 . (i1,m1)) . x by Def9;
then A75: ((ProjMap2 (FF2,m)) . i) . x = ((FF . i) . m) . x by A8;
assume x in E ; :: thesis:
then x in dom (F . i) by A1, A3;
hence ((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x by A6, A73, A74, A75; :: thesis:

end;

A76: for n, m being Nat st n <= m holds
for i being Nat
for x being Element of X st x in E holds
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x

proof

let n, m be Nat; :: thesis:
A77: ProjMap2 (FF2,n) is with_the_same_dom by A10;
A78: ProjMap2 (FF2,m) is additive by A10;
assume A79: n <= m ; :: thesis:
A80: for i being Nat
for x being Element of X st x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x

proof

let i be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) ; :: thesis:
then x in dom ((ProjMap2 (FF2,n)) . 0) by XBOOLE_0:def 4;
then x in E by A10;
hence ((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x by A72, A79; :: thesis:

end;

let i be Nat; :: thesis:
let x be Element of X; :: thesis:
assume A81: x in E ; :: thesis:
then A82: x in dom ((ProjMap2 (FF2,m)) . 0) by A10;
x in dom ((ProjMap2 (FF2,n)) . 0) by A10, A81;
then A83: x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) by A82, XBOOLE_0:def 4;
A84: ProjMap2 (FF2,m) is with_the_same_dom by A10;
ProjMap2 (FF2,n) is additive by A10;
hence ((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x by A83, A77, A78, A84, A80, Th42; :: thesis:

end;

A85: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(P . n) . x <= (P . m) . x

proof

end;

A91: for x being Element of X st x in dom (lim P) holds
P # x is convergent

proof

let x be Element of X; :: thesis:
assume A92: x in dom (lim P) ; :: thesis:
for n, m being Nat st m <= n holds
(P # x) . m <= (P # x) . n

proof

let n, m be Nat; :: thesis:
assume m <= n ; :: thesis:
then (P . m) . x <= (P . n) . x by A1, A85, A23, A92;
then (P # x) . m <= (P . n) . x by MESFUNC5:def 13;
hence (P # x) . m <= (P # x) . n by MESFUNC5:def 13; :: thesis:

end;

then P # x is non-decreasing by RINFSUP2:7;
hence P # x is convergent by RINFSUP2:37; :: thesis:

end;

A93: for x being Element of X st x in dom (lim P) holds
lim (P # x) = lim ((Partial_Sums F) # x)

proof

defpred S₂[ Element of NAT , Element of NAT , set ] means for n, m being Nat st n = $1 & m = $2 holds
$3 = (Partial_Sums (ProjMap2 (FF2,n))) . m;
let x be Element of X; :: thesis:
A94: for i1, j1 being Element of NAT ex PP2 being Element of PFuncs (X,ExtREAL) st S₂[i1,j1,PP2]

proof

let i1, j1 be Element of NAT ; :: thesis:
reconsider i = i1, j = j1 as Nat ;
reconsider F1 = (Partial_Sums (ProjMap2 (FF2,i))) . j as Element of PFuncs (X,ExtREAL) by PARTFUN1:45;
take F1 ; :: thesis:
thus S₂[i1,j1,F1] ; :: thesis:

end;

consider PP2 being Function of [:NAT,NAT:],(PFuncs (X,ExtREAL)) such that
A95: for i, j being Element of NAT holds S₂[i,j,PP2 . (i,j)] from BINOP_1:sch 3(A94);
assume A96: x in dom (lim P) ; :: thesis:
then A97: P # x is convergent by A91;
A98: for p, n being Element of NAT holds (ProjMap2 (PP2,n)) . p = (Partial_Sums (ProjMap2 (FF2,p))) . n

proof

let p, n be Element of NAT ; :: thesis:
(ProjMap2 (PP2,n)) . p = PP2 . (p,n) by Def9;
hence (ProjMap2 (PP2,n)) . p = (Partial_Sums (ProjMap2 (FF2,p))) . n by A95; :: thesis:

end;

A99: for n being Element of NAT holds
( (ProjMap2 (PP2,n)) # x is convergent & ((ProjMap2 (PP2,n)) # x) ^\ n is convergent & lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) )

proof

let n be Element of NAT ; :: thesis:
(ProjMap2 (PP2,n)) # x is non-decreasing

proof

let j, k be ExtReal; :: according to VALUED_0:def 15 :: thesis:
assume that
A100: j in dom ((ProjMap2 (PP2,n)) # x) and
A101: k in dom ((ProjMap2 (PP2,n)) # x) and
A102: j <= k ; :: thesis:
reconsider j = j, k = k as Element of NAT by A100, A101;
A103: ProjMap2 (FF2,j) is additive by A10;
A104: ProjMap2 (FF2,k) is with_the_same_dom by A10;
A105: dom ((ProjMap2 (FF2,k)) . 0) = E by A10;
((ProjMap2 (PP2,n)) # x) . k = ((ProjMap2 (PP2,n)) . k) . x by MESFUNC5:def 13;
then A106: ((ProjMap2 (PP2,n)) # x) . k = ((Partial_Sums (ProjMap2 (FF2,k))) . n) . x by A98;
A107: ProjMap2 (FF2,k) is additive by A10;
((ProjMap2 (PP2,n)) # x) . j = ((ProjMap2 (PP2,n)) . j) . x by MESFUNC5:def 13;
then A108: ((ProjMap2 (PP2,n)) # x) . j = ((Partial_Sums (ProjMap2 (FF2,j))) . n) . x by A98;
A109: ProjMap2 (FF2,j) is with_the_same_dom by A10;
A110: dom ((ProjMap2 (FF2,j)) . 0) = E by A10;
then for i being Nat
for z being Element of X st z in (dom ((ProjMap2 (FF2,j)) . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,j)) . i) . z <= ((ProjMap2 (FF2,k)) . i) . z by A72, A102, A105;
hence ((ProjMap2 (PP2,n)) # x) . j <= ((ProjMap2 (PP2,n)) # x) . k by A1, A23, A96, A108, A106, A103, A109, A107, A104, A110, A105, Th42; :: thesis:

end;

hence (ProjMap2 (PP2,n)) # x is convergent by RINFSUP2:37; :: thesis:
hence ( ((ProjMap2 (PP2,n)) # x) ^\ n is convergent & lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) ) by RINFSUP2:21; :: thesis:

end;

A111: for n being Nat holds ((Partial_Sums F) # x) . n <= lim (P # x)

proof

for p being object st p in NAT holds
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p

proof

let p be object ; :: thesis:
assume p in NAT ; :: thesis:
then reconsider p9 = p as Element of NAT ;
(ProjMap2 (PP2,0)) . p9 = (Partial_Sums (ProjMap2 (FF2,p9))) . 0 by A98;
then (ProjMap2 (PP2,0)) . p9 = (ProjMap2 (FF2,p9)) . 0 by Def4;
then (ProjMap2 (PP2,0)) . p9 = FF2 . (0,p9) by Def9;
then A112: (ProjMap2 (PP2,0)) . p9 = (ProjMap1 (FF2,0)) . p9 by Def8;
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap2 (PP2,0)) . p9) . x by MESFUNC5:def 13;
hence ((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p by A112, MESFUNC5:def 13; :: thesis:

end;

then (ProjMap2 (PP2,0)) # x = (ProjMap1 (FF2,0)) # x ;
then A113: lim ((ProjMap2 (PP2,0)) # x) = (F . 0) . x by A1, A39, A23, A96;
defpred S₃[ Nat] means lim ((ProjMap2 (PP2,$1)) # x) = ((Partial_Sums F) # x) . $1;
let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A114: lim ((P # x) ^\ n9) = lim (P # x) by A97, RINFSUP2:21;
A115: ((ProjMap2 (PP2,n)) # x) ^\ n9 is convergent by A99;
A116: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
assume A117: S₃[k] ; :: thesis:
A118: (ProjMap2 (PP2,k9)) # x is convergent by A99;

now :: thesis:

let m be object ; :: thesis:
assume m in dom ((ProjMap1 (FF2,(k + 1))) # x) ; :: thesis:
then reconsider m1 = m as Element of NAT ;
(ProjMap1 (FF2,(k + 1))) . m1 is nonnegative by A38;
then 0. <= ((ProjMap1 (FF2,(k + 1))) . m1) . x by SUPINF_2:51;
hence 0. <= ((ProjMap1 (FF2,(k + 1))) # x) . m by MESFUNC5:def 13; :: thesis:

end;

then A119: (ProjMap1 (FF2,(k + 1))) # x is nonnegative by SUPINF_2:52;

now :: thesis:

let m be object ; :: thesis:
assume m in dom ((ProjMap2 (PP2,k)) # x) ; :: thesis:
then reconsider m1 = m as Element of NAT ;
A120: (ProjMap2 (PP2,k)) . m1 = (Partial_Sums (ProjMap2 (FF2,m1))) . k9 by A98;
for l being Nat holds (ProjMap2 (FF2,m1)) . l is nonnegative by A38;
then (ProjMap2 (PP2,k)) . m1 is nonnegative by A120, Th36;
then 0. <= ((ProjMap2 (PP2,k)) . m1) . x by SUPINF_2:51;
hence 0. <= ((ProjMap2 (PP2,k)) # x) . m by MESFUNC5:def 13; :: thesis:

end;

then A121: (ProjMap2 (PP2,k)) # x is nonnegative by SUPINF_2:52;
x in dom ((Partial_Sums F) . (k + 1)) by A2, A3, A23, A96, Th29;
then A122: x in dom (((Partial_Sums F) . k) + (F . (k + 1))) by Def4;
A123: for p being Nat holds ((ProjMap2 (PP2,(k + 1))) # x) . p = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) # x) . p)

proof

let p be Nat; :: thesis:
reconsider p9 = p as Element of NAT by ORDINAL1:def 12;
A124: (ProjMap2 (FF2,p9)) . (k + 1) = FF2 . ((k + 1),p9) by Def9;
A125: ProjMap2 (FF2,p) is with_the_same_dom by A10;
A126: dom ((ProjMap2 (FF2,p)) . 0) = E by A10;
ProjMap2 (FF2,p) is additive by A10;
then E c= dom ((Partial_Sums (ProjMap2 (FF2,p))) . (k + 1)) by A125, A126, Th29;
then A127: E c= dom ((ProjMap2 (PP2,(k + 1))) . p9) by A98;
(ProjMap2 (PP2,(k + 1))) . p9 = (Partial_Sums (ProjMap2 (FF2,p9))) . (k + 1) by A98;
then A128: (ProjMap2 (PP2,(k + 1))) . p9 = ((Partial_Sums (ProjMap2 (FF2,p9))) . k) + ((ProjMap2 (FF2,p9)) . (k + 1)) by Def4;
(Partial_Sums (ProjMap2 (FF2,p9))) . k9 = (ProjMap2 (PP2,k)) . p9 by A98;
then (ProjMap2 (PP2,(k + 1))) . p9 = ((ProjMap2 (PP2,k)) . p9) + ((ProjMap1 (FF2,(k + 1))) . p9) by A128, A124, Def8;
then ((ProjMap2 (PP2,(k + 1))) . p9) . x = (((ProjMap2 (PP2,k)) . p9) . x) + (((ProjMap1 (FF2,(k + 1))) . p9) . x) by A1, A23, A96, A127, MESFUNC1:def 3;
then A129: ((ProjMap2 (PP2,(k + 1))) . p9) . x = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) . p9) . x) by MESFUNC5:def 13;
((ProjMap2 (PP2,(k + 1))) # x) . p = ((ProjMap2 (PP2,(k + 1))) . p9) . x by MESFUNC5:def 13;
hence ((ProjMap2 (PP2,(k + 1))) # x) . p = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) # x) . p) by A129, MESFUNC5:def 13; :: thesis:

end;

A130: lim ((ProjMap1 (FF2,(k + 1))) # x) = (F . (k + 1)) . x by A1, A39, A23, A96;
(ProjMap1 (FF2,(k + 1))) # x is convergent by A1, A39, A23, A96;
then lim ((ProjMap2 (PP2,(k + 1))) # x) = (lim ((ProjMap2 (PP2,k)) # x)) + (lim ((ProjMap1 (FF2,(k + 1))) # x)) by A118, A121, A119, A123, Th11;
then lim ((ProjMap2 (PP2,(k + 1))) # x) = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) by A117, A130, MESFUNC5:def 13;
then lim ((ProjMap2 (PP2,(k + 1))) # x) = (((Partial_Sums F) . k) + (F . (k + 1))) . x by A122, MESFUNC1:def 3;
then lim ((ProjMap2 (PP2,(k + 1))) # x) = ((Partial_Sums F) . (k + 1)) . x by Def4;
hence S₃[k + 1] by MESFUNC5:def 13; :: thesis:

end;

A131: for p being Nat holds (((ProjMap2 (PP2,n)) # x) ^\ n9) . p <= ((P # x) ^\ n9) . p

proof

end;

((Partial_Sums F) # x) . 0 = ((Partial_Sums F) . 0) . x by MESFUNC5:def 13;
then A138: S₃[ 0 ] by A113, Def4;
A139: for k being Nat holds S₃[k] from NAT_1:sch 2(A138, A116);
(P # x) ^\ n9 is convergent by A97, RINFSUP2:21;
then lim (((ProjMap2 (PP2,n)) # x) ^\ n9) <= lim ((P # x) ^\ n9) by A115, A131, RINFSUP2:38;
then lim ((ProjMap2 (PP2,n)) # x) <= lim (P # x) by A99, A114;
hence ((Partial_Sums F) # x) . n <= lim (P # x) by A139; :: thesis:

end;

F # x is summable by A1, A5, A23, A96;
then A140: Partial_Sums (F # x) is convergent ;
(Partial_Sums F) # x is convergent

proof

per cases by A140;

suppose Partial_Sums (F # x) is convergent_to_finite_number ; :: thesis:

then (Partial_Sums F) # x is convergent_to_finite_number by A2, A3, A23, A96, Th33;
hence (Partial_Sums F) # x is convergent ; :: thesis:

end;

suppose Partial_Sums (F # x) is convergent_to_+infty ; :: thesis:

then (Partial_Sums F) # x is convergent_to_+infty by A2, A3, A23, A96, Th33;
hence (Partial_Sums F) # x is convergent ; :: thesis:

end;

suppose Partial_Sums (F # x) is convergent_to_-infty ; :: thesis:

then (Partial_Sums F) # x is convergent_to_-infty by A2, A3, A23, A96, Th33;
hence (Partial_Sums F) # x is convergent ; :: thesis:

end;

then A141: lim ((Partial_Sums F) # x) <= lim (P # x) by A111, Th9;
A142: for k being Nat holds (P # x) . k <= ((Partial_Sums F) # x) . k

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence (P # x) . n <= ((Partial_Sums F) # x) . n by A31, A96; :: thesis:

end;

(Partial_Sums F) # x is convergent by A3, A4, A23, A96, Th38;
then lim (P # x) <= lim ((Partial_Sums F) # x) by A97, A142, RINFSUP2:38;
hence lim (P # x) = lim ((Partial_Sums F) # x) by A141, XXREAL_0:1; :: thesis:

end;

A143: for x being Element of X st x in dom (lim (Partial_Sums F)) holds
( P # x is convergent & lim (P # x) = (lim (Partial_Sums F)) . x )

proof

let x be Element of X; :: thesis:
assume A144: x in dom (lim (Partial_Sums F)) ; :: thesis:
then x in dom (lim P) by A1, A6, A22, A37;
hence P # x is convergent by A91; :: thesis:
lim (P # x) = lim ((Partial_Sums F) # x) by A1, A23, A37, A93, A144;
hence lim (P # x) = (lim (Partial_Sums F)) . x by A144, MESFUNC8:def 9; :: thesis:

end;

A145: for n being Nat holds P . n is nonnegative

proof

let n be Nat; :: thesis:
for k being Nat holds (ProjMap2 (FF2,n)) . k is nonnegative by A38;
then (Partial_Sums (ProjMap2 (FF2,n))) . n is nonnegative by Th36;
hence P . n is nonnegative by A9; :: thesis:

end;

A146: for x being object st x in dom (lim (Partial_Sums F)) holds
(lim (Partial_Sums F)) . x >= 0

proof

let x be object ; :: thesis:
assume A147: x in dom (lim (Partial_Sums F)) ; :: thesis:
then reconsider x1 = x as Element of X ;
A148: for n being Nat holds ((Partial_Sums F) # x1) . n >= 0

proof

let n be Nat; :: thesis:
(Partial_Sums F) . n is nonnegative by A4, Th36;
then ((Partial_Sums F) . n) . x1 >= 0 by SUPINF_2:51;
hence ((Partial_Sums F) # x1) . n >= 0 by MESFUNC5:def 13; :: thesis:

end;

x in dom (F . 0) by A67, A147, Def4;
then (Partial_Sums F) # x1 is convergent by A3, A4, Th38;
then lim ((Partial_Sums F) # x1) >= 0 by A148, Th10;
hence (lim (Partial_Sums F)) . x >= 0 by A147, MESFUNC8:def 9; :: thesis:

end;

then A149: lim (Partial_Sums F) is nonnegative by SUPINF_2:52;
consider I being ExtREAL_sequence such that
A150: for n being Nat holds
( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n ) by A1, A2, A3, A4, Th50;
for n being object st n in dom I holds
0 <= I . n

proof

let n be object ; :: thesis:
assume n in dom I ; :: thesis:
then reconsider n1 = n as Nat ;
A151: F . n1 is nonnegative by A4;
A152: F . n1 is E -measurable by A4;
E = dom (F . n1) by A1, A3;
then 0 <= Integral (M,(F . n1)) by A151, A152, MESFUNC5:90;
hence 0 <= I . n by A150; :: thesis:

end;

then I is nonnegative by SUPINF_2:52;
then A153: Partial_Sums I is non-decreasing by Th16;
then A154: Partial_Sums I is convergent by RINFSUP2:37;
deffunc H₂( Element of NAT ) -> Element of ExtREAL = integral' (M,(P . $1));
consider J being sequence of ExtREAL such that
A155: for n being Element of NAT holds J . n = H₂(n) from FUNCT_2:sch 4();
reconsider J = J as ExtREAL_sequence ;
A156: for n being Nat holds P . n is_simple_func_in S

proof

let n be Nat; :: thesis:
for m being Nat holds (ProjMap2 (FF2,n)) . m is_simple_func_in S by A10;
then (Partial_Sums (ProjMap2 (FF2,n))) . n is_simple_func_in S by Th35;
hence P . n is_simple_func_in S by A9; :: thesis:

end;

A157: for n being Nat holds J . n = integral' (M,(P . n))

proof

let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
J . n = integral' (M,(P . n9)) by A155;
hence J . n = integral' (M,(P . n)) ; :: thesis:

end;

for n, m being Nat st m <= n holds
J . m <= J . n

proof

let n, m be Nat; :: thesis:
A158: P . n is nonnegative by A145;
A159: P . m is_simple_func_in S by A156;
A160: for n, m, l being Nat holds dom ((P . n) - (P . m)) = dom (P . l)

proof

let n, m, l be Nat; :: thesis:
P . m is_simple_func_in S by A156;
then A161: P . m is without+infty by MESFUNC5:14;
P . n is_simple_func_in S by A156;
then P . n is without-infty by MESFUNC5:14;
then dom ((P . n) - (P . m)) = (dom (P . n)) /\ (dom (P . m)) by A161, MESFUNC5:17;
then dom ((P . n) - (P . m)) = (dom (lim (Partial_Sums F))) /\ (dom (P . m)) by A69;
then dom ((P . n) - (P . m)) = (dom (lim (Partial_Sums F))) /\ (dom (lim (Partial_Sums F))) by A69;
hence dom ((P . n) - (P . m)) = dom (P . l) by A69; :: thesis:

end;

then A162: dom ((P . n) - (P . m)) = dom (P . n) ;
then A163: (P . n) | (dom ((P . n) - (P . m))) = P . n ;
assume A164: m <= n ; :: thesis:
A165: for x being object st x in dom ((P . n) - (P . m)) holds
(P . m) . x <= (P . n) . x

proof

let x be object ; :: thesis:
assume x in dom ((P . n) - (P . m)) ; :: thesis:
then x in dom (lim (Partial_Sums F)) by A69, A162;
hence (P . m) . x <= (P . n) . x by A68, A85, A164; :: thesis:

end;

A166: P . m is nonnegative by A145;
dom ((P . n) - (P . m)) = dom (P . m) by A160;
then A167: (P . m) | (dom ((P . n) - (P . m))) = P . m ;
P . n is_simple_func_in S by A156;
then integral' (M,((P . m) | (dom ((P . n) - (P . m))))) <= integral' (M,((P . n) | (dom ((P . n) - (P . m))))) by A158, A159, A166, A165, MESFUNC5:70;
then J . m <= integral' (M,(P . n)) by A157, A167, A163;
hence J . m <= J . n by A157; :: thesis:

end;

then J is non-decreasing by RINFSUP2:7;
then A168: J is convergent by RINFSUP2:37;
A169: for n being Nat holds F . n is without-infty by A4, MESFUNC5:12;
then A170: for n being Nat holds (Partial_Sums F) . n is E -measurable by A4, Th41;
then lim (Partial_Sums F) is E -measurable by A1, A2, A3, A5, Th44;
then integral+ (M,(lim (Partial_Sums F))) = lim J by A68, A156, A85, A157, A69, A143, A145, A149, A168, MESFUNC5:def 15;
then A171: Integral (M,(lim (Partial_Sums F))) = lim J by A1, A2, A3, A5, A170, A37, A149, Th44, MESFUNC5:88;
A172: for n being Nat
for x being Element of X st x in dom (F . n) holds
(FF . n) # x is non-decreasing

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume A173: x in dom (F . n) ; :: thesis:
let i, j be ExtReal; :: according to VALUED_0:def 15 :: thesis:
assume that
A174: i in dom ((FF . n) # x) and
A175: j in dom ((FF . n) # x) and
A176: i <= j ; :: thesis:
reconsider i = i, j = j as Element of NAT by A174, A175;
((FF . n) . i) . x <= ((FF . n) . j) . x by A6, A173, A176;
then ((FF . n) # x) . i <= ((FF . n) . j) . x by MESFUNC5:def 13;
hence ((FF . n) # x) . i <= ((FF . n) # x) . j by MESFUNC5:def 13; :: thesis:

end;

A177: for n, p being Nat st p >= n holds
for x being Element of X st x in E holds
( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )

proof

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0)) ; :: thesis:
then x in dom (F . 0) by XBOOLE_0:def 4;
then A185: x in dom (F . n) by A3;
then (FF . n) # x is non-decreasing by A172;
then lim ((FF . n) # x) = sup ((FF . n) # x) by RINFSUP2:37;
then ((FF . n) # x) . p1 <= lim ((FF . n) # x) by RINFSUP2:23;
then A186: ((FF . n) # x) . p <= (F . n) . x by A6, A185;
((ProjMap2 (FF2,p)) . n) . x = (FF2 . (n1,p1)) . x by Def9;
then ((ProjMap2 (FF2,p)) . n) . x = ((FF . n) . p) . x by A8;
hence ((ProjMap2 (FF2,p)) . n) . x <= (F . n) . x by A186, MESFUNC5:def 13; :: thesis:

end;

x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0)) by A1, A180, A181, XBOOLE_0:def 4;
hence ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x by A2, A3, A182, A183, A184, Th42; :: thesis:
(Partial_Sums F) # x is non-decreasing by A1, A3, A4, A180, Th38;
then lim ((Partial_Sums F) # x) = sup ((Partial_Sums F) # x) by RINFSUP2:37;
then ((Partial_Sums F) # x) . p1 <= lim ((Partial_Sums F) # x) by RINFSUP2:23;
then ((Partial_Sums F) . p) . x <= lim ((Partial_Sums F) # x) by MESFUNC5:def 13;
hence ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x by A68, A180, MESFUNC8:def 9; :: thesis:

end;

for n being Nat holds (Partial_Sums I) . n <= Integral (M,(lim (Partial_Sums F)))

proof

let n be Nat; :: thesis:
A187: (Partial_Sums F) . n is nonnegative by A4, Th36;
A188: lim (Partial_Sums F) is E -measurable by A1, A2, A3, A5, A170, Th44;
A189: (Partial_Sums F) . n is E -measurable by A4, A169, Th41;
A190: E = dom ((Partial_Sums F) . n) by A1, A2, A3, Th29;
then for x being Element of X st x in dom ((Partial_Sums F) . n) holds
((Partial_Sums F) . n) . x <= (lim (Partial_Sums F)) . x by A177;
then integral+ (M,((Partial_Sums F) . n)) <= integral+ (M,(lim (Partial_Sums F))) by A37, A149, A190, A189, A188, A187, MESFUNC5:85;
then Integral (M,((Partial_Sums F) . n)) <= integral+ (M,(lim (Partial_Sums F))) by A170, A190, A187, MESFUNC5:88;
then Integral (M,((Partial_Sums F) . n)) <= Integral (M,(lim (Partial_Sums F))) by A37, A146, A188, MESFUNC5:88, SUPINF_2:52;
hence (Partial_Sums I) . n <= Integral (M,(lim (Partial_Sums F))) by A150; :: thesis:

end;

then A191: lim (Partial_Sums I) <= Integral (M,(lim (Partial_Sums F))) by A153, Th9, RINFSUP2:37;
take I ; :: thesis:
thus for n being Nat holds I . n = Integral (M,((F . n) | E)) :: thesis:

proof

let n be Nat; :: thesis:
dom (F . 0) = dom (F . n) by A3;
then (F . n) | E = F . n by A1;
hence I . n = Integral (M,((F . n) | E)) by A150; :: thesis:

end;

A192: for n being Nat holds J . n = Integral (M,(P . n))

proof

let n be Nat; :: thesis:
A193: P . n is nonnegative by A145;
A194: J . n = integral' (M,(P . n)) by A157;
P . n is_simple_func_in S by A156;
hence J . n = Integral (M,(P . n)) by A193, A194, MESFUNC5:89; :: thesis:

end;

for n being Nat holds J . n <= (Partial_Sums I) . n

proof

let n be Nat; :: thesis:
A195: P . n is E -measurable by A156, MESFUNC2:34;
A196: (Partial_Sums F) . n is nonnegative by A4, Th36;
A197: n in NAT by ORDINAL1:def 12;
A198: for x being Element of X st x in dom (P . n) holds
(P . n) . x <= ((Partial_Sums F) . n) . x

proof

let x be Element of X; :: thesis:
assume x in dom (P . n) ; :: thesis:
then x in dom (lim (Partial_Sums F)) by A69;
then (P # x) . n <= ((Partial_Sums F) # x) . n by A1, A23, A37, A31, A197;
then (P . n) . x <= ((Partial_Sums F) # x) . n by MESFUNC5:def 13;
hence (P . n) . x <= ((Partial_Sums F) . n) . x by MESFUNC5:def 13; :: thesis:

end;

A199: P . n is nonnegative by A145;
A200: dom (P . n) = E by A37, A69;
A201: E = dom ((Partial_Sums F) . n) by A1, A2, A3, Th29;
(Partial_Sums F) . n is E -measurable by A4, A169, Th41;
then integral+ (M,(P . n)) <= integral+ (M,((Partial_Sums F) . n)) by A201, A200, A195, A199, A196, A198, MESFUNC5:85;
then Integral (M,(P . n)) <= integral+ (M,((Partial_Sums F) . n)) by A145, A200, A195, MESFUNC5:88;
then Integral (M,(P . n)) <= Integral (M,((Partial_Sums F) . n)) by A170, A201, A196, MESFUNC5:88;
then J . n <= Integral (M,((Partial_Sums F) . n)) by A192;
hence J . n <= (Partial_Sums I) . n by A150; :: thesis:

end;

then lim J <= lim (Partial_Sums I) by A168, A154, RINFSUP2:38;
then Sum I = Integral (M,(lim (Partial_Sums F))) by A171, A191, XXREAL_0:1;
hence ( I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I ) by A37, A154; :: thesis: