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
S1: F is additive and
S2: F is with_the_same_dom and
A2: for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) and
A3: for x being Element of X st x in E holds
F # x is summable ; :: thesis:
G2: for n being Nat holds F . n is without-infty by A2, MESFUNC5:18;
then G3: for n being Nat holds (Partial_Sums F) . n is_measurable_on E by A2, ADD1;
then A4: lim (Partial_Sums F) is_measurable_on E by A1, S1, S2, A3, ADD2;
consider FF being Function of NAT ,(Funcs NAT ,(PFuncs X,ExtREAL )) such that
A5: 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, S2, A2, Th131z;
A6: 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 A61: x in dom (F . n) ; :: thesis:
let i, j be ext-real number ; :: according to VALUED_0:def 15 :: thesis:
assume Z: ( i in dom ((FF . n) # x) & j in dom ((FF . n) # x) & i <= j ) ; :: thesis:
then reconsider i = i, j = j as Element of NAT ;
((FF . n) . i) . x <= ((FF . n) . j) . x by A5, A61, Z;
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;

A7: dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0 ) by MESFUNC8:def 10;
then A72: dom (lim (Partial_Sums F)) = E by A1, Def0;
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;
Z1: 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:119;
take F1 ; :: thesis:
thus S₁[i1,j1,F1] ; :: thesis:

end;

consider FF2 being Function of [:NAT ,NAT :],(PFuncs X,ExtREAL ) such that
Z2: for i, j being Element of NAT holds S₁[i,j,FF2 . i,j] from BINOP_1:sch 3(Z1);
Q1: 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:

T0: now

let m be Nat; :: thesis:
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
T1: ( (ProjMap1 FF2,n) . m = FF2 . n,m & (ProjMap2 FF2,n) . m = FF2 . m,n ) by defproj1, defproj2;
T2: ( FF2 . n1,m1 = (FF . n1) . m & FF2 . m1,n1 = (FF . m1) . n ) by Z2;
( dom (F . n1) = dom (F . m1) & dom (F . m1) = dom (F . 0 ) ) by S2, MESFUNC8:def 2;
hence ( dom ((ProjMap1 FF2,n) . m) = E & dom ((ProjMap2 FF2,n) . m) = E ) by A1, T1, T2, A5; :: thesis:
thus ( (ProjMap1 FF2,n) . m is_simple_func_in S & (ProjMap2 FF2,n) . m is_simple_func_in S ) by A5, T1, T2; :: 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:
( dom ((ProjMap1 FF2,n) . i1) = E & dom ((ProjMap1 FF2,n) . j1) = E & dom ((ProjMap2 FF2,n) . i1) = E & dom ((ProjMap2 FF2,n) . j1) = E ) by T0;
hence ( dom ((ProjMap1 FF2,n) . i1) = dom ((ProjMap1 FF2,n) . j1) & dom ((ProjMap2 FF2,n) . i1) = dom ((ProjMap2 FF2,n) . j1) ) ; :: 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 Lem10, T0, MESFUNC8:def 2; :: thesis:

end;

K2: 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 13;
(ProjMap1 FF2,n) . m = FF2 . n1,m1 by defproj1;
then (ProjMap1 FF2,n) . m = (FF . n) . m by Z2;
hence (ProjMap1 FF2,n) . m is nonnegative by A5; :: thesis:
(ProjMap2 FF2,n) . m = FF2 . m1,n1 by defproj2;
then (ProjMap2 FF2,n) . m = (FF . m) . n by Z2;
hence (ProjMap2 FF2,n) . m is nonnegative by A5; :: thesis:

end;

K3: 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 ;
KL0: E = dom (F . n1) by A1, S2, MESFUNC8:def 2;
let x be Element of X; :: thesis:
assume KK0: x in E ; :: thesis:
(ProjMap1 FF2,n) # x is non-decreasing

proof

let i, j be ext-real number ; :: according to VALUED_0:def 15 :: thesis:
assume KK5: ( i in dom ((ProjMap1 FF2,n) # x) & j in dom ((ProjMap1 FF2,n) # x) & i <= j ) ; :: thesis:
then reconsider i1 = i, j1 = j as Element of NAT ;
KK3: ((FF . n1) . i1) . x <= ((FF . n1) . j1) . x by A5, KK0, KL0, KK5;
KK1: ( ((ProjMap1 FF2,n) # x) . i1 = ((ProjMap1 FF2,n) . i1) . x & ((ProjMap1 FF2,n) # x) . j1 = ((ProjMap1 FF2,n) . j1) . x ) by MESFUNC5:def 13;
(ProjMap1 FF2,n) . i1 = FF2 . n,i1 by defproj1;
then KK2: (ProjMap1 FF2,n) . i1 = (FF . n1) . i1 by Z2;
(ProjMap1 FF2,n) . j1 = FF2 . n,j1 by defproj1;
then ((ProjMap1 FF2,n) # x) . i1 <= ((ProjMap1 FF2,n) # x) . j1 by Z2, KK1, KK2, KK3;
hence ((ProjMap1 FF2,n) # x) . i <= ((ProjMap1 FF2,n) # x) . j ; :: thesis:

end;

hence K31: (ProjMap1 FF2,n) # x is convergent by RINFSUP2:37; :: 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:
K321: ((ProjMap1 FF2,n) # x) . m = ((ProjMap1 FF2,n) . m) . x by MESFUNC5:def 13;
(ProjMap1 FF2,n) . m is nonnegative by K2;
hence ( k <= m & ((ProjMap1 FF2,n) # x) . m > - 1 ) by K321, SUPINF_2:58; :: thesis:

end;

then K33: not (ProjMap1 FF2,n) # x is convergent_to_-infty by MESFUNC5:def 10;

per cases ) # x is convergent_to_finite_number or (ProjMap1 FF2,n) # x is convergent_to_+infty ) by K31, K33, MESFUNC5:def 11;

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

then ( not (ProjMap1 FF2,n) # x is convergent_to_+infty & not (ProjMap1 FF2,n) # x is convergent_to_-infty ) by MESFUNC5:56, MESFUNC5:57;
then consider lP being real number such that
T2: ( lim ((ProjMap1 FF2,n) # x) = lP & ( for p being real number 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 ) & (ProjMap1 FF2,n) # x is convergent_to_finite_number ) by K31, MESFUNC5:def 12;
T3: for p being real number st 0 < p holds
ex nn being Nat st
for mm being Nat st nn <= mm holds
|.((((FF . n1) # x) . mm) - (R_EAL lP)).| < p

proof

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then consider nn being Nat such that
T31: for mm being Nat st nn <= mm holds
|.((((ProjMap1 FF2,n) # x) . mm) - (lim ((ProjMap1 FF2,n) # x))).| < p by T2;
take nn ; :: thesis:
let mm be Nat; :: thesis:
assume T32: nn <= mm ; :: thesis:
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 13;
T33: ((ProjMap1 FF2,n) # x) . mm = ((ProjMap1 FF2,n) . mm) . x by MESFUNC5:def 13;
(ProjMap1 FF2,n) . mm = FF2 . n,mm by defproj1;
then (ProjMap1 FF2,n) . mm = (FF . n1) . mm1 by Z2;
then ((FF . n1) # x) . mm = ((ProjMap1 FF2,n) # x) . mm by T33, MESFUNC5:def 13;
hence |.((((FF . n1) # x) . mm) - (R_EAL lP)).| < p by T32, T31, T2; :: thesis:

end;

then T4: (FF . n1) # x is convergent_to_finite_number by MESFUNC5:def 8;
then (FF . n1) # x is convergent by MESFUNC5:def 11;
then lim ((FF . n1) # x) = R_EAL lP by T3, T4, MESFUNC5:def 12;
hence (F . n) . x = lim ((ProjMap1 FF2,n) # x) by A5, T2, KL0, KK0; :: thesis:

end;

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

then KK5: lim ((ProjMap1 FF2,n) # x) = +infty by K31, MESFUNC5:def 12;
for g being real number 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 number ; :: thesis:
assume 0 < g ; :: thesis:
then consider nn being Nat such that
KK8: for mm being Nat st nn <= mm holds
g <= ((ProjMap1 FF2,n) # x) . mm by KK1, MESFUNC5:def 9;
take nn ; :: thesis:
let mm be Nat; :: thesis:
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 13;
assume nn <= mm ; :: thesis:
then KK9: g <= ((ProjMap1 FF2,n) # x) . mm by KK8;
KK10: ((ProjMap1 FF2,n) # x) . mm = ((ProjMap1 FF2,n) . mm) . x by MESFUNC5:def 13;
(ProjMap1 FF2,n) . mm = FF2 . n,mm1 by defproj1;
then (ProjMap1 FF2,n) . mm = (FF . n) . mm by Z2;
hence g <= ((FF . n1) # x) . mm by KK9, KK10, MESFUNC5:def 13; :: thesis:

end;

then KK2: (FF . n1) # x is convergent_to_+infty by MESFUNC5:def 9;
then (FF . n1) # x is convergent by MESFUNC5:def 11;
then lim ((FF . n1) # x) = +infty by KK2, MESFUNC5:def 12;
hence (F . n) . x = lim ((ProjMap1 FF2,n) # x) by A5, KK0, KL0, KK5; :: thesis:

end;

deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (Partial_Sums (ProjMap2 FF2,$1)) . $1;
consider P being Functional_Sequence of X,ExtREAL such that
K5: for k being Nat holds P . k = H₁(k) from SEQFUNC:sch 1();
for n, m being Nat holds dom (P . n) = dom (P . m)

proof

let n, m be Nat; :: thesis:
K51: ( ProjMap2 FF2,n is additive & ProjMap2 FF2,n is with_the_same_dom & ProjMap2 FF2,m is additive & ProjMap2 FF2,m is with_the_same_dom ) by Q1;
dom (P . n) = dom ((Partial_Sums (ProjMap2 FF2,n)) . n) by K5;
then dom (P . n) = dom ((ProjMap2 FF2,n) . 0 ) by K51, ADD0;
then dom (P . n) = E by Q1;
then dom (P . n) = dom ((ProjMap2 FF2,m) . 0 ) by Q1;
then dom (P . n) = dom ((Partial_Sums (ProjMap2 FF2,m)) . m) by K51, ADD0;
hence dom (P . n) = dom (P . m) by K5; :: thesis:

end;

then reconsider P = P as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
K6: 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 Q1;
then (Partial_Sums (ProjMap2 FF2,n)) . n is_simple_func_in S by Lem10;
hence P . n is_simple_func_in S by K5; :: thesis:

end;

K7: 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 J21: n <= m ; :: thesis:
let i be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in E ; :: thesis:
then JJ0: x in dom (F . i) by A1, S2, MESFUNC8:def 2;
reconsider i1 = i, n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
((ProjMap2 FF2,n) . i) . x = (FF2 . i1,n1) . x by defproj2;
then JJ1: ((ProjMap2 FF2,n) . i) . x = ((FF . i) . n) . x by Z2;
((ProjMap2 FF2,m) . i) . x = (FF2 . i1,m1) . x by defproj2;
then ((ProjMap2 FF2,m) . i) . x = ((FF . i) . m) . x by Z2;
hence ((ProjMap2 FF2,n) . i) . x <= ((ProjMap2 FF2,m) . i) . x by J21, JJ0, JJ1, A5; :: thesis:

end;

K8: 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:
assume K81: n <= m ; :: thesis:
let i be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in E ; :: thesis:
then ( x in dom ((ProjMap2 FF2,n) . 0 ) & x in dom ((ProjMap2 FF2,m) . 0 ) ) by Q1;
then K83: x in (dom ((ProjMap2 FF2,n) . 0 )) /\ (dom ((ProjMap2 FF2,m) . 0 )) by XBOOLE_0:def 4;
K82: ( ProjMap2 FF2,n is additive & ProjMap2 FF2,n is with_the_same_dom & ProjMap2 FF2,m is additive & ProjMap2 FF2,m is with_the_same_dom ) by Q1;
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 Q1;
hence ((ProjMap2 FF2,n) . i) . x <= ((ProjMap2 FF2,m) . i) . x by K7, K81; :: thesis:

end;

hence ((Partial_Sums (ProjMap2 FF2,n)) . i) . x <= ((Partial_Sums (ProjMap2 FF2,m)) . i) . x by K82, K83, ADD4; :: thesis:

end;

K9: 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

let n, m be Nat; :: thesis:
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
assume K91: n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume K92: x in E ; :: thesis:
then ((Partial_Sums (ProjMap2 FF2,n)) . n) . x <= ((Partial_Sums (ProjMap2 FF2,m)) . n) . x by K91, K8;
then K93: (P . n) . x <= ((Partial_Sums (ProjMap2 FF2,m)) . n) . x by K5;
K94: ( ProjMap2 FF2,m is additive & ProjMap2 FF2,m is with_the_same_dom ) by Q1;
K95: x in dom ((ProjMap2 FF2,m) . 0 ) by Q1, K92;
for n being Nat holds (ProjMap2 FF2,m) . n is nonnegative by K2;
then (Partial_Sums (ProjMap2 FF2,m)) # x is non-decreasing by K94, K95, ADD3;
then ((Partial_Sums (ProjMap2 FF2,m)) # x) . n1 <= ((Partial_Sums (ProjMap2 FF2,m)) # x) . m1 by K91, RINFSUP2:7;
then ((Partial_Sums (ProjMap2 FF2,m)) . n) . x <= ((Partial_Sums (ProjMap2 FF2,m)) # x) . m1 by MESFUNC5:def 13;
then ((Partial_Sums (ProjMap2 FF2,m)) . n) . x <= ((Partial_Sums (ProjMap2 FF2,m)) . m) . x by MESFUNC5:def 13;
then ((Partial_Sums (ProjMap2 FF2,m)) . n) . x <= (P . m) . x by K5;
hence (P . n) . x <= (P . m) . x by K93, XXREAL_0:2; :: thesis:

end;

J1: 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

let n, p be Nat; :: thesis:
reconsider p1 = p, n1 = n as Element of NAT by ORDINAL1:def 13;
assume BB1: p >= n ; :: thesis:
let x be Element of X; :: thesis:
assume BB0: x in E ; :: thesis:
then BB2: x in dom ((ProjMap2 FF2,p) . 0 ) by Q1;
( ProjMap2 FF2,p is additive & ProjMap2 FF2,p is with_the_same_dom & ( for i being Nat holds (ProjMap2 FF2,p) . i is nonnegative ) ) by Q1, K2;
then (Partial_Sums (ProjMap2 FF2,p)) # x is non-decreasing by BB2, ADD3;
then ((Partial_Sums (ProjMap2 FF2,p)) # x) . n1 <= ((Partial_Sums (ProjMap2 FF2,p)) # x) . p1 by BB1, RINFSUP2:7;
then ((Partial_Sums (ProjMap2 FF2,p)) . n) . x <= ((Partial_Sums (ProjMap2 FF2,p)) # x) . p by MESFUNC5:def 13;
then ((Partial_Sums (ProjMap2 FF2,p)) . n) . x <= ((Partial_Sums (ProjMap2 FF2,p)) . p) . x by MESFUNC5:def 13;
hence ((Partial_Sums (ProjMap2 FF2,p)) . n) . x <= (P . p) . x by K5; :: thesis:
thus (P . p) . x = ((Partial_Sums (ProjMap2 FF2,p)) . p) . x by K5; :: thesis:
ND31: ( ProjMap2 FF2,p is additive & ProjMap2 FF2,p is with_the_same_dom ) by Q1;
ND32: for n being Nat
for x being Element of X st x in (dom ((ProjMap2 FF2,p) . 0 )) /\ (dom (F . 0 )) holds
((ProjMap2 FF2,p) . n) . x <= (F . n) . x

proof

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
assume x in (dom ((ProjMap2 FF2,p) . 0 )) /\ (dom (F . 0 )) ; :: thesis:
then x in dom (F . 0 ) by XBOOLE_0:def 4;
then N322: x in dom (F . n) by S2, MESFUNC8:def 2;
((ProjMap2 FF2,p) . n) . x = (FF2 . n1,p1) . x by defproj2;
then N323: ((ProjMap2 FF2,p) . n) . x = ((FF . n) . p) . x by Z2;
(FF . n) # x is non-decreasing by N322, A6;
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 ((FF . n) # x) . p <= (F . n) . x by N322, A5;
hence ((ProjMap2 FF2,p) . n) . x <= (F . n) . x by N323, MESFUNC5:def 13; :: thesis:

end;

x in (dom ((ProjMap2 FF2,p) . 0 )) /\ (dom (F . 0 )) by BB0, A1, BB2, XBOOLE_0:def 4;
hence ((Partial_Sums (ProjMap2 FF2,p)) . p) . x <= ((Partial_Sums F) . p) . x by S1, S2, ND31, ND32, ADD4; :: thesis:
(Partial_Sums F) # x is non-decreasing by BB0, A1, S2, A2, ADD3;
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 BB0, A72, MESFUNC8:def 10; :: thesis:

end;

dom (lim P) = dom (P . 0 ) by MESFUNC8:def 10;
then dom (lim P) = dom ((Partial_Sums (ProjMap2 FF2,0 )) . 0 ) by K5;
then dom (lim P) = dom ((ProjMap2 FF2,0 ) . 0 ) by Def0;
then dom (lim P) = dom (FF2 . 0 ,0 ) by defproj2;
then N1: dom (lim P) = dom ((FF . 0 ) . 0 ) by Z2;
reconsider FF0 = FF . 0 as Functional_Sequence of X,ExtREAL ;
N21: dom (lim P) = dom (F . 0 ) by A5, N1;
dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0 ) by MESFUNC8:def 10;
then N5: dom (lim (Partial_Sums F)) = E by A1, Def0;
N8: 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 N4: x in dom (lim P) ; :: thesis:
for n, m being Element of NAT st m <= n holds
(P # x) . m <= (P # x) . n

proof

let n, m be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then (P . m) . x <= (P . n) . x by K9, N4, N21, A1;
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;

HHH: 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:
assume x in (dom (F . 0 )) /\ (dom ((ProjMap2 FF2,k) . 0 )) ; :: thesis:
then x in dom (F . 0 ) by XBOOLE_0:def 4;
then H1: x in dom (F . m) by S2, MESFUNC8:def 2;
reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 13;
(ProjMap2 FF2,k) . m = FF2 . m1,k1 by defproj2;
then H2: (ProjMap2 FF2,k) . m = (FF . m) . k by Z2;
(FF . m1) # x is non-decreasing

proof

let j, k be ext-real number ; :: according to VALUED_0:def 15 :: thesis:
assume H3: ( j in dom ((FF . m1) # x) & k in dom ((FF . m1) # x) & j <= k ) ; :: thesis:
then reconsider j = j, k = k as Element of NAT ;
( ((FF . m1) # x) . j = ((FF . m1) . j) . x & ((FF . m1) # x) . k = ((FF . m1) . k) . x ) by MESFUNC5:def 13;
hence ((FF . m1) # x) . j <= ((FF . m1) # x) . k by H1, H3, A5; :: 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 ((FF . m1) # x) . k <= (F . m1) . x by H1, A5;
hence ((ProjMap2 FF2,k) . m) . x <= (F . m) . x by H2, MESFUNC5:def 13; :: thesis:

end;

U0: 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 N4: x in dom (lim P) ; :: thesis:
(P # x) . k = (P . k) . x by MESFUNC5:def 13;
then U1: (P # x) . k = ((Partial_Sums (ProjMap2 FF2,k)) . k) . x by K5;
dom ((ProjMap2 FF2,k) . 0 ) = E by Q1;
then N73: x in (dom (F . 0 )) /\ (dom ((ProjMap2 FF2,k) . 0 )) by N4, A5, N1, A1;
( ProjMap2 FF2,k is additive & ProjMap2 FF2,k is with_the_same_dom & ( 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 Q1, HHH;
then ((Partial_Sums (ProjMap2 FF2,k)) . k) . x <= ((Partial_Sums F) . k) . x by S1, S2, N73, ADD4;
hence (P # x) . k <= ((Partial_Sums F) # x) . k by U1, MESFUNC5:def 13; :: thesis:

end;

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

proof

let x be Element of X; :: thesis:
assume N4: x in dom (lim P) ; :: thesis:
then NN8: P # x is convergent by N8;
N9: (Partial_Sums F) # x is convergent by N4, N21, S2, A2, ADD3;
for k being Element of NAT holds (P # x) . k <= ((Partial_Sums F) # x) . k by N4, U0;
then N10: lim (P # x) <= lim ((Partial_Sums F) # x) by NN8, N9, RINFSUP2:38;
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;
ZZ1: 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:119;
take F1 ; :: thesis:
thus S₂[i1,j1,F1] ; :: thesis:

end;

consider PP2 being Function of [:NAT ,NAT :],(PFuncs X,ExtREAL ) such that
ZZ2: for i, j being Element of NAT holds S₂[i,j,PP2 . i,j] from BINOP_1:sch 3(ZZ1);
ZZ3: 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:
reconsider p1 = p, n1 = n as Nat ;
(ProjMap2 PP2,n) . p = PP2 . p,n by defproj2;
hence (ProjMap2 PP2,n) . p = (Partial_Sums (ProjMap2 FF2,p)) . n by ZZ2; :: thesis:

end;

J2: 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 ext-real number ; :: according to VALUED_0:def 15 :: thesis:
assume J21: ( j in dom ((ProjMap2 PP2,n) # x) & k in dom ((ProjMap2 PP2,n) # x) & j <= k ) ; :: thesis:
then reconsider j = j, k = k as Element of NAT ;
( ((ProjMap2 PP2,n) # x) . j = ((ProjMap2 PP2,n) . j) . x & ((ProjMap2 PP2,n) # x) . k = ((ProjMap2 PP2,n) . k) . x ) by MESFUNC5:def 13;
then J22: ( ((ProjMap2 PP2,n) # x) . j = ((Partial_Sums (ProjMap2 FF2,j)) . n) . x & ((ProjMap2 PP2,n) # x) . k = ((Partial_Sums (ProjMap2 FF2,k)) . n) . x ) by ZZ3;
J23: ( ProjMap2 FF2,j is additive & ProjMap2 FF2,j is with_the_same_dom & ProjMap2 FF2,k is additive & ProjMap2 FF2,k is with_the_same_dom ) by Q1;
N73: ( dom ((ProjMap2 FF2,j) . 0 ) = E & dom ((ProjMap2 FF2,k) . 0 ) = E ) by Q1;
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 J21, K7;
hence ((ProjMap2 PP2,n) # x) . j <= ((ProjMap2 PP2,n) # x) . k by J22, J23, ADD4, N73, N21, A1, N4; :: 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;

lim ((Partial_Sums F) # x) <= lim (P # x)

proof

F # x is summable by A3, N21, A1, N4;
then R00: Partial_Sums (F # x) is convergent by Def2;
R0: (Partial_Sums F) # x is convergent

proof

per cases by R00, MESFUNC5:def 11;

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

then (Partial_Sums F) # x is convergent_to_finite_number by S1, S2, N21, N4, Cor01;
hence (Partial_Sums F) # x is convergent by MESFUNC5:def 11; :: thesis:

end;

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

then (Partial_Sums F) # x is convergent_to_+infty by S1, S2, N21, N4, Cor01;
hence (Partial_Sums F) # x is convergent by MESFUNC5:def 11; :: thesis:

end;

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

then (Partial_Sums F) # x is convergent_to_-infty by S1, S2, N21, N4, Cor01;
hence (Partial_Sums F) # x is convergent by MESFUNC5:def 11; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
R1: ( (P # x) ^\ n' is convergent & lim ((P # x) ^\ n') = lim (P # x) ) by NN8, RINFSUP2:21;
R2: ((ProjMap2 PP2,n) # x) ^\ n' is convergent by J2;
for p being Element of NAT holds (((ProjMap2 PP2,n) # x) ^\ n') . p <= ((P # x) ^\ n') . p

proof

let p be Element of NAT ; :: thesis:
(((ProjMap2 PP2,n) # x) ^\ n') . p = ((ProjMap2 PP2,n) # x) . (n + p) by NAT_1:def 3;
then (((ProjMap2 PP2,n) # x) ^\ n') . p = ((ProjMap2 PP2,n) . (n + p)) . x by MESFUNC5:def 13;
then R3: (((ProjMap2 PP2,n) # x) ^\ n') . p = ((Partial_Sums (ProjMap2 FF2,(n + p))) . n) . x by ZZ3;
((P # x) ^\ n') . p = (P # x) . (n + p) by NAT_1:def 3;
then ((P # x) ^\ n') . p = (P . (n + p)) . x by MESFUNC5:def 13;
then R4: ((P # x) ^\ n') . p = ((Partial_Sums (ProjMap2 FF2,(n + p))) . (n + p)) . x by K5;
R51: n <= n + p by NAT_1:11;
R52: x in dom ((ProjMap2 FF2,(n + p)) . 0 ) by Q1, N21, A1, N4;
( ProjMap2 FF2,(n + p) is additive & ProjMap2 FF2,(n + p) is with_the_same_dom & ( for i being Nat holds (ProjMap2 FF2,(n + p)) . i is nonnegative ) ) by Q1, K2;
then (Partial_Sums (ProjMap2 FF2,(n + p))) # x is non-decreasing by R52, ADD3;
then ((Partial_Sums (ProjMap2 FF2,(n + p))) # x) . n' <= ((Partial_Sums (ProjMap2 FF2,(n + p))) # x) . (n' + p) by R51, RINFSUP2:7;
then ((Partial_Sums (ProjMap2 FF2,(n + p))) # x) . n' <= ((Partial_Sums (ProjMap2 FF2,(n + p))) . (n + p)) . x by MESFUNC5:def 13;
hence (((ProjMap2 PP2,n) # x) ^\ n') . p <= ((P # x) ^\ n') . p by R3, R4, MESFUNC5:def 13; :: thesis:

end;

then lim (((ProjMap2 PP2,n) # x) ^\ n') <= lim ((P # x) ^\ n') by R1, R2, RINFSUP2:38;
then J3: lim ((ProjMap2 PP2,n) # x) <= lim (P # x) by R1, J2;
defpred S₃[ Nat] means lim ((ProjMap2 PP2,$1) # x) = ((Partial_Sums F) # x) . $1;
V1: lim ((ProjMap2 PP2,0 ) # x) = (F . 0 ) . x

proof

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

proof

let p be set ; :: thesis:
assume p in NAT ; :: thesis:
then reconsider p' = p as Element of NAT ;
V74: ((ProjMap2 PP2,0 ) # x) . p = ((ProjMap2 PP2,0 ) . p') . x by MESFUNC5:def 13;
(ProjMap2 PP2,0 ) . p' = (Partial_Sums (ProjMap2 FF2,p')) . 0 by ZZ3;
then (ProjMap2 PP2,0 ) . p' = (ProjMap2 FF2,p') . 0 by Def0;
then (ProjMap2 PP2,0 ) . p' = FF2 . 0 ,p' by defproj2;
then (ProjMap2 PP2,0 ) . p' = (ProjMap1 FF2,0 ) . p' by defproj1;
hence ((ProjMap2 PP2,0 ) # x) . p = ((ProjMap1 FF2,0 ) # x) . p by V74, MESFUNC5:def 13; :: thesis:

end;

then (ProjMap2 PP2,0 ) # x = (ProjMap1 FF2,0 ) # x by FUNCT_2:18;
hence lim ((ProjMap2 PP2,0 ) # x) = (F . 0 ) . x by K3, N4, N21, A1; :: thesis:

end;

((Partial_Sums F) # x) . 0 = ((Partial_Sums F) . 0 ) . x by MESFUNC5:def 13;
then V2: S₃[ 0 ] by V1, Def0;
V3: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
assume V31: S₃[k] ; :: thesis:
(ProjMap2 PP2,k') # x is convergent by J2;
then V41: ( (ProjMap2 PP2,k) # x is convergent & (ProjMap1 FF2,(k + 1)) # x is convergent ) by K3, N4, N21, A1;

now

let m be set ; :: thesis:
assume m in dom ((ProjMap2 PP2,k) # x) ; :: thesis:
then reconsider m1 = m as Element of NAT ;
V413: for l being Nat holds (ProjMap2 FF2,m1) . l is nonnegative by K2;
(ProjMap2 PP2,k) . m1 = (Partial_Sums (ProjMap2 FF2,m1)) . k' by ZZ3;
then (ProjMap2 PP2,k) . m1 is nonnegative by V413, ADD3C;
then 0. <= ((ProjMap2 PP2,k) . m1) . x by SUPINF_2:70;
hence 0. <= ((ProjMap2 PP2,k) # x) . m by MESFUNC5:def 13; :: thesis:

end;

then V42: (ProjMap2 PP2,k) # x is nonnegative by SUPINF_2:71;

now

let m be set ; :: 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 K2;
then 0. <= ((ProjMap1 FF2,(k + 1)) . m1) . x by SUPINF_2:70;
hence 0. <= ((ProjMap1 FF2,(k + 1)) # x) . m by MESFUNC5:def 13; :: thesis:

end;

then V43: (ProjMap1 FF2,(k + 1)) # x is nonnegative by SUPINF_2:71;
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 p' = p as Element of NAT by ORDINAL1:def 13;
V32: ((ProjMap2 PP2,(k + 1)) # x) . p = ((ProjMap2 PP2,(k + 1)) . p') . x by MESFUNC5:def 13;
(ProjMap2 PP2,(k + 1)) . p' = (Partial_Sums (ProjMap2 FF2,p')) . (k + 1) by ZZ3;
then V33: (ProjMap2 PP2,(k + 1)) . p' = ((Partial_Sums (ProjMap2 FF2,p')) . k) + ((ProjMap2 FF2,p') . (k + 1)) by Def0;
V34: (Partial_Sums (ProjMap2 FF2,p')) . k' = (ProjMap2 PP2,k) . p' by ZZ3;
(ProjMap2 FF2,p') . (k + 1) = FF2 . (k + 1),p' by defproj2;
then V35: (ProjMap2 PP2,(k + 1)) . p' = ((ProjMap2 PP2,k) . p') + ((ProjMap1 FF2,(k + 1)) . p') by V33, V34, defproj1;
( ProjMap2 FF2,p is additive & ProjMap2 FF2,p is with_the_same_dom & dom ((ProjMap2 FF2,p) . 0 ) = E ) by Q1;
then E c= dom ((Partial_Sums (ProjMap2 FF2,p)) . (k + 1)) by ADD0;
then E c= dom ((ProjMap2 PP2,(k + 1)) . p') by ZZ3;
then ((ProjMap2 PP2,(k + 1)) . p') . x = (((ProjMap2 PP2,k) . p') . x) + (((ProjMap1 FF2,(k + 1)) . p') . x) by N4, N21, A1, V35, MESFUNC1:def 3;
then ((ProjMap2 PP2,(k + 1)) . p') . x = (((ProjMap2 PP2,k) # x) . p) + (((ProjMap1 FF2,(k + 1)) . p') . x) by MESFUNC5:def 13;
hence ((ProjMap2 PP2,(k + 1)) # x) . p = (((ProjMap2 PP2,k) # x) . p) + (((ProjMap1 FF2,(k + 1)) # x) . p) by V32, MESFUNC5:def 13; :: thesis:

end;

then V44: lim ((ProjMap2 PP2,(k + 1)) # x) = (lim ((ProjMap2 PP2,k) # x)) + (lim ((ProjMap1 FF2,(k + 1)) # x)) by V41, V42, V43, LIM2;
lim ((ProjMap1 FF2,(k + 1)) # x) = (F . (k + 1)) . x by K3, N4, N21, A1;
then V46: lim ((ProjMap2 PP2,(k + 1)) # x) = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) by V44, V31, MESFUNC5:def 13;
x in dom ((Partial_Sums F) . (k + 1)) by S1, S2, N4, N21, ADD0;
then x in dom (((Partial_Sums F) . k) + (F . (k + 1))) by Def0;
then lim ((ProjMap2 PP2,(k + 1)) # x) = (((Partial_Sums F) . k) + (F . (k + 1))) . x by V46, MESFUNC1:def 3;
then lim ((ProjMap2 PP2,(k + 1)) # x) = ((Partial_Sums F) . (k + 1)) . x by Def0;
hence S₃[k + 1] by MESFUNC5:def 13; :: thesis:

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(V2, V3);
hence ((Partial_Sums F) # x) . n <= lim (P # x) by J3; :: thesis:

end;

hence lim ((Partial_Sums F) # x) <= lim (P # x) by R0, LIM3; :: thesis:

end;

hence lim (P # x) = lim ((Partial_Sums F) # x) by N10, XXREAL_0:1; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of ExtREAL = integral' M,(P . $1);
consider J being Function of NAT ,ExtREAL such that
JJ1: for n being Element of NAT holds J . n = H₂(n) from FUNCT_2:sch 4();
reconsider J = J as ExtREAL_sequence ;
T0: for n being Nat holds J . n = integral' M,(P . n)

proof

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

end;

T1: for n being Nat holds dom (P . n) = dom (lim (Partial_Sums F))

proof

let n be Nat; :: thesis:
K51: ( ProjMap2 FF2,n is additive & ProjMap2 FF2,n is with_the_same_dom ) by Q1;
dom (P . n) = dom ((Partial_Sums (ProjMap2 FF2,n)) . n) by K5;
then dom (P . n) = dom ((ProjMap2 FF2,n) . 0 ) by K51, ADD0;
hence dom (P . n) = dom (lim (Partial_Sums F)) by Q1, A72; :: thesis:

end;

T2: 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 T21: x in dom (lim (Partial_Sums F)) ; :: thesis:
then x in dom (lim P) by A1, N5, A5, N1;
hence P # x is convergent by N8; :: thesis:
lim (P # x) = lim ((Partial_Sums F) # x) by LL7, T21, N21, A1, N5;
hence lim (P # x) = (lim (Partial_Sums F)) . x by T21, MESFUNC8:def 10; :: thesis:

end;

T3: ( lim (Partial_Sums F) is nonnegative & ( for n being Nat holds P . n is nonnegative ) & J is convergent )

proof

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

proof

let x be set ; :: thesis:
assume T31: x in dom (lim (Partial_Sums F)) ; :: thesis:
then reconsider x1 = x as Element of X ;
x in dom (F . 0 ) by T31, A7, Def0;
then T32: (Partial_Sums F) # x1 is convergent by A2, S2, ADD3;
for n being Nat holds ((Partial_Sums F) # x1) . n >= 0

proof

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

end;

then lim ((Partial_Sums F) # x1) >= 0 by T32, LIM3a;
hence (lim (Partial_Sums F)) . x >= 0 by T31, MESFUNC8:def 10; :: thesis:

end;

hence lim (Partial_Sums F) is nonnegative by SUPINF_2:71; :: thesis:
thus T33: for n being Nat holds P . n is nonnegative :: thesis:

proof

let n be Nat; :: thesis:
( ( for k being Nat holds (ProjMap2 FF2,n) . k is nonnegative ) & ProjMap2 FF2,n is with_the_same_dom ) by Q1, K2;
then (Partial_Sums (ProjMap2 FF2,n)) . n is nonnegative by ADD3C;
hence P . n is nonnegative by K5; :: thesis:

end;

for n, m being Element of NAT st m <= n holds
J . m <= J . n

proof

let n, m be Element of NAT ; :: thesis:
assume T34: m <= n ; :: thesis:
T35: ( P . n is_simple_func_in S & P . n is nonnegative & P . m is_simple_func_in S & P . m is nonnegative ) by K6, T33;
for n, m, l being Element of NAT holds dom ((P . n) - (P . m)) = dom (P . l)

proof

let n, m, l be Element of NAT ; :: thesis:
( P . n is_simple_func_in S & P . m is_simple_func_in S ) by K6;
then ( P . n is without-infty & P . m is without+infty ) by MESFUNC5:20;
then dom ((P . n) - (P . m)) = (dom (P . n)) /\ (dom (P . m)) by MESFUNC5:23;
then dom ((P . n) - (P . m)) = (dom (lim (Partial_Sums F))) /\ (dom (P . m)) by T1;
then dom ((P . n) - (P . m)) = (dom (lim (Partial_Sums F))) /\ (dom (lim (Partial_Sums F))) by T1;
hence dom ((P . n) - (P . m)) = dom (P . l) by T1; :: thesis:

end;

then T37: ( dom ((P . n) - (P . m)) = dom (P . n) & dom ((P . n) - (P . m)) = dom (P . m) ) ;
then T36: ( (P . m) | (dom ((P . n) - (P . m))) = P . m & (P . n) | (dom ((P . n) - (P . m))) = P . n ) by RELAT_1:97;
for x being set st x in dom ((P . n) - (P . m)) holds
(P . m) . x <= (P . n) . x

proof

let x be set ; :: thesis:
assume x in dom ((P . n) - (P . m)) ; :: thesis:
then x in dom (lim (Partial_Sums F)) by T1, T37;
hence (P . m) . x <= (P . n) . x by A72, T34, K9; :: thesis:

end;

then integral' M,((P . m) | (dom ((P . n) - (P . m)))) <= integral' M,((P . n) | (dom ((P . n) - (P . m)))) by T35, MESFUNC5:76;
then J . m <= integral' M,(P . n) by T0, T36;
hence J . m <= J . n by T0; :: thesis:

end;

then J is non-decreasing by RINFSUP2:7;
hence J is convergent by RINFSUP2:37; :: thesis:

end;

then integral+ M,(lim (Partial_Sums F)) = lim J by A4, T0, T1, T2, A72, K6, K9, MESFUNC5:def 15;
then T4: Integral M,(lim (Partial_Sums F)) = lim J by A4, T3, N5, MESFUNC5:94;
T5: for n being Nat holds J . n = Integral M,(P . n)

proof

let n be Nat; :: thesis:
T01: ( P . n is_simple_func_in S & P . n is nonnegative ) by K6, T3;
J . n = integral' M,(P . n) by T0;
hence J . n = Integral M,(P . n) by T01, MESFUNC5:95; :: thesis:

end;

consider I being ExtREAL_sequence such that
T7: for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n ) by S1, S2, A1, A2, FSUM2;
for n being set st n in dom I holds
0 <= I . n

proof

let n be set ; :: thesis:
assume n in dom I ; :: thesis:
then reconsider n1 = n as Nat ;
( E = dom (F . n1) & F . n1 is nonnegative & F . n1 is_measurable_on E ) by A1, S2, A2, MESFUNC8:def 2;
then 0 <= Integral M,(F . n1) by MESFUNC5:96;
hence 0 <= I . n by T7; :: thesis:

end;

then I is nonnegative by SUPINF_2:71;
then Partial_Sums I is non-decreasing by ADD3a;
then Z1: Partial_Sums I is convergent by RINFSUP2:37;
for n being Element of NAT holds J . n <= (Partial_Sums I) . n

proof

let n be Element of NAT ; :: thesis:
C1: E = dom ((Partial_Sums F) . n) by A1, S1, S2, ADD0;
V1: dom (P . n) = E by N5, T1;
C2: (Partial_Sums F) . n is_measurable_on E by G2, A2, ADD1;
C3: P . n is_measurable_on E by K6, MESFUNC2:37;
C5: P . n is nonnegative by T3;
C7: (Partial_Sums F) . n is nonnegative by A2, ADD3C;
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 T1;
then (P # x) . n <= ((Partial_Sums F) # x) . n by N5, U0, N21, A1;
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;

then integral+ M,(P . n) <= integral+ M,((Partial_Sums F) . n) by C1, V1, C2, C3, C5, C7, MESFUNC5:91;
then Integral M,(P . n) <= integral+ M,((Partial_Sums F) . n) by V1, C3, T3, MESFUNC5:94;
then Integral M,(P . n) <= Integral M,((Partial_Sums F) . n) by C1, G3, C7, MESFUNC5:94;
then J . n <= Integral M,((Partial_Sums F) . n) by T5;
hence J . n <= (Partial_Sums I) . n by T7; :: thesis:

end;

then T8: lim J <= lim (Partial_Sums I) by T3, Z1, RINFSUP2:38;
for n being Nat holds (Partial_Sums I) . n <= Integral M,(lim (Partial_Sums F))

proof

let n be Nat; :: thesis:
C1: E = dom ((Partial_Sums F) . n) by A1, S1, S2, ADD0;
C2: (Partial_Sums F) . n is_measurable_on E by G2, A2, ADD1;
C4: lim (Partial_Sums F) is_measurable_on E by A1, S1, S2, A3, G3, ADD2;
C7: (Partial_Sums F) . n is nonnegative by A2, ADD3C;
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 C1, J1;
then integral+ M,((Partial_Sums F) . n) <= integral+ M,(lim (Partial_Sums F)) by C1, C2, N5, C4, C7, T3, MESFUNC5:91;
then Integral M,((Partial_Sums F) . n) <= integral+ M,(lim (Partial_Sums F)) by C1, G3, C7, MESFUNC5:94;
then Integral M,((Partial_Sums F) . n) <= Integral M,(lim (Partial_Sums F)) by N5, C4, T3, MESFUNC5:94;
hence (Partial_Sums I) . n <= Integral M,(lim (Partial_Sums F)) by T7; :: thesis:

end;

then lim (Partial_Sums I) <= Integral M,(lim (Partial_Sums F)) by Z1, LIM3;
then P9: Sum I = Integral M,(lim (Partial_Sums F)) by T8, T4, XXREAL_0:1;
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 S2, MESFUNC8:def 2;
then (F . n) | E = F . n by A1, RELAT_1:97;
hence I . n = Integral M,((F . n) | E) by T7; :: thesis:

end;

thus ( I is summable & Integral M,((lim (Partial_Sums F)) | E) = Sum I ) by P9, N5, Z1, Def2, RELAT_1:97; :: thesis: