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 PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is_measurable_on E ; :: thesis:
set F = f | E;
R1: dom (f | E) = E by A1, RELAT_1:91;
E = (dom f) /\ E by A1, XBOOLE_1:28;
then ( f | E is_measurable_on E & f | E is nonnegative ) by A2, A3, MESFUNC5:21, MESFUNC5:48;
then consider h being Functional_Sequence of X,ExtREAL such that
A4: ( ( for n being Nat holds
( h . n is_simple_func_in S & dom (h . n) = dom (f | E) ) ) & ( for n being Nat holds h . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | E) holds
(h . n) . x <= (h . m) . x ) & ( for x being Element of X st x in dom (f | E) holds
( h # x is convergent & lim (h # x) = (f | E) . x ) ) ) by R1, MESFUNC5:70;
defpred S₁[ Element of NAT , set , set ] means $3 = (h . ($1 + 1)) - (h . $1);
K1: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y] ;
consider g being Function such that
K3: ( dom g = NAT & g . 0 = h . 0 & ( for n being Element of NAT holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 1(K1);

now

let f be set ; :: thesis:
assume f in rng g ; :: thesis:
then consider m being set such that
K41: ( m in dom g & f = g . m ) by FUNCT_1:def 5;
reconsider m = m as Element of NAT by K41, K3;
defpred S₂[ Element of NAT ] means g . $1 is PartFunc of X,ExtREAL ;
K42: S₂[ 0 ] by K3;
K43: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume S₂[n] ; :: thesis:
then reconsider F2 = g . n as PartFunc of X,ExtREAL ;
g . (n + 1) = (h . (n + 1)) - (h . n) by K3;
hence S₂[n + 1] ; :: thesis:

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(K42, K43);
then g . m is PartFunc of X,ExtREAL ;
hence f in PFuncs X,ExtREAL by K41, PARTFUN1:119; :: thesis:

end;

then rng g c= PFuncs X,ExtREAL by TARSKI:def 3;
then reconsider g = g as Functional_Sequence of X,ExtREAL by K3, FUNCT_2:def 1, RELSET_1:11;
take g ; :: thesis:
Q1: for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is_measurable_on E & E c= dom (g . n) )

proof

let n be Nat; :: thesis:

per cases ;

suppose Q01: n = 0 ; :: thesis:

hence ( g . n is_simple_func_in S & g . n is nonnegative ) by A4, K3; :: thesis:
hence g . n is_measurable_on E by MESFUNC2:37; :: thesis:
thus E c= dom (g . n) by R1, Q01, K3, A4; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then consider m being Nat such that
P2: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
P5: g . n = (h . n) - (h . m) by K3, P2;
then P3: g . n = (h . n) + (- (h . m)) by MESFUNC2:9;
P4: ( h . n is_simple_func_in S & h . m is_simple_func_in S ) by A4;
then (- 1) (#) (h . m) is_simple_func_in S by MESFUNC5:45;
then P11: - (h . m) is_simple_func_in S by MESFUNC2:11;
hence g . n is_simple_func_in S by P3, P4, MESFUNC5:44; :: thesis:
( h . n is without-infty & h . m is without+infty ) by P4, MESFUNC5:20;
then P7: dom ((h . n) - (h . m)) = (dom (h . n)) /\ (dom (h . m)) by MESFUNC5:23;
P10: ( dom (h . n) = dom (f | E) & dom (h . m) = dom (f | E) ) by A4;

now

let x be set ; :: thesis:
assume P9: x in dom ((h . n) - (h . m)) ; :: thesis:
m <= m + 1 by NAT_1:11;
hence (h . m) . x <= (h . n) . x by P9, P10, P7, A4, P2; :: thesis:

end;

hence g . n is nonnegative by P4, P5, MESFUNC5:46; :: thesis:
thus g . n is_measurable_on E by P11, P3, P4, MESFUNC2:37, MESFUNC5:44; :: thesis:
thus E c= dom (g . n) by R1, K3, P2, P10, P7; :: thesis:

end;

hence Q2: g is additive by Lem10; :: thesis:
thus for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is_measurable_on E ) by Q1; :: thesis:

Q3: now

let x be Element of X; :: thesis:
assume L0: x in E ; :: thesis:
then L1: ( h # x is convergent & lim (h # x) = (f | E) . x ) by A4, R1;
L5: for m being Nat holds (Partial_Sums (g # x)) . m = (h # x) . m

proof

let m be Nat; :: thesis:
defpred S₂[ Nat] means (Partial_Sums (g # x)) . $1 = (h # x) . $1;
(Partial_Sums (g # x)) . 0 = (g # x) . 0 by Def1;
then (Partial_Sums (g # x)) . 0 = (g . 0 ) . x by MESFUNC5:def 13;
then B1: S₂[ 0 ] by K3, MESFUNC5:def 13;
B2: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
set Pgx = Partial_Sums (g # x);
assume S₂[k] ; :: thesis:
then B3: (Partial_Sums (g # x)) . k = (h . k) . x by MESFUNC5:def 13;
( h . (k + 1) is_simple_func_in S & h . k is_simple_func_in S ) by A4;
then B4: ( h . (k + 1) is without+infty & h . (k + 1) is without-infty & h . k is without+infty & h . k is without-infty ) by MESFUNC5:20;
B5: ( dom (h . (k + 1)) = dom (f | E) & dom (h . k) = dom (f | E) ) by A4;
then C0: ( -infty < (h . (k + 1)) . x & (h . (k + 1)) . x < +infty & -infty < (h . k) . x & (h . k) . x < +infty ) by L0, R1, B4, MESFUNC5:16, MESFUNC5:17;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
B6: g . (k + 1) = (h . (k + 1)) - (h . k) by K3;
B7: dom ((h . (k + 1)) - (h . k)) = (dom (h . (k + 1))) /\ (dom (h . k)) by B4, MESFUNC5:23;
(Partial_Sums (g # x)) . (k + 1) = ((Partial_Sums (g # x)) . k) + ((g # x) . (k + 1)) by Def1;
then B9: (Partial_Sums (g # x)) . (k + 1) = ((h . k) . x) + ((g . (k + 1)) . x) by B3, MESFUNC5:def 13;
reconsider hk1x = (h . (k + 1)) . x as Real by C0, XXREAL_0:14;
reconsider hkx = (h . k) . x as Real by C0, XXREAL_0:14;
((h . (k + 1)) . x) - ((h . k) . x) = hk1x - hkx by SUPINF_2:5;
then D2: (((h . (k + 1)) . x) - ((h . k) . x)) + ((h . k) . x) = (hk1x - hkx) + hkx by SUPINF_2:1;
(g . (k + 1)) . x = ((h . (k + 1)) . x) - ((h . k) . x) by B6, B7, L0, R1, B5, MESFUNC1:def 4;
hence S₂[k + 1] by B9, D2, MESFUNC5:def 13; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(B1, B2);
hence (Partial_Sums (g # x)) . m = (h # x) . m ; :: thesis:

end;

per cases by L1, MESFUNC5:def 11;

suppose h # x is convergent_to_finite_number ; :: thesis:

then ( not h # x is convergent_to_+infty & not h # x is convergent_to_-infty ) by MESFUNC5:56, MESFUNC5:57;
then consider s being real number such that
L3: ( lim (h # x) = s & ( for p being real number st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p ) & h # x is convergent_to_finite_number ) by L1, MESFUNC5:def 12;
for p being real number st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((Partial_Sums (g # x)) . m) - (R_EAL s)).| < p

proof

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
L4: for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p by L3;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then |.(((h # x) . m) - (lim (h # x))).| < p by L4;
hence |.(((Partial_Sums (g # x)) . m) - (R_EAL s)).| < p by L5, L3; :: thesis:

end;

then L7: Partial_Sums (g # x) is convergent_to_finite_number by MESFUNC5:def 8;
then L8: Partial_Sums (g # x) is convergent by MESFUNC5:def 11;
hence g # x is summable by Def2; :: thesis:
for p being real number st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((Partial_Sums (g # x)) . m) - (lim (h # x))).| < p

proof

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
S1: for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p by L3;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then |.(((h # x) . m) - (lim (h # x))).| < p by S1;
hence |.(((Partial_Sums (g # x)) . m) - (lim (h # x))).| < p by L5; :: thesis:

end;

then lim (Partial_Sums (g # x)) = lim (h # x) by L3, L7, L8, MESFUNC5:def 12;
hence Sum (g # x) = f . x by L0, L1, FUNCT_1:72; :: thesis:

end;

suppose T1: h # x is convergent_to_+infty ; :: thesis:

for p being real number st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
p <= (Partial_Sums (g # x)) . m

proof

let p be real number ; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
T3: for m being Nat st N <= m holds
p <= (h # x) . m by T1, MESFUNC5:def 9;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then p <= (h # x) . m by T3;
hence p <= (Partial_Sums (g # x)) . m by L5; :: thesis:

end;

then T4: Partial_Sums (g # x) is convergent_to_+infty by MESFUNC5:def 9;
then T5: Partial_Sums (g # x) is convergent by MESFUNC5:def 11;
hence g # x is summable by Def2; :: thesis:
T6: lim (h # x) = +infty by T1, L1, MESFUNC5:def 12;
lim (Partial_Sums (g # x)) = +infty by T4, T5, MESFUNC5:def 12;
hence Sum (g # x) = f . x by L0, L1, T6, FUNCT_1:72; :: thesis:

end;

suppose U1: h # x is convergent_to_-infty ; :: thesis:

for p being real number st p < 0 holds
ex N being Nat st
for m being Nat st N <= m holds
(Partial_Sums (g # x)) . m <= p

proof

let p be real number ; :: thesis:
assume p < 0 ; :: thesis:
then consider N being Nat such that
U3: for m being Nat st N <= m holds
(h # x) . m <= p by U1, MESFUNC5:def 10;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then (h # x) . m <= p by U3;
hence (Partial_Sums (g # x)) . m <= p by L5; :: thesis:

end;

then U4: Partial_Sums (g # x) is convergent_to_-infty by MESFUNC5:def 10;
then U5: Partial_Sums (g # x) is convergent by MESFUNC5:def 11;
hence g # x is summable by Def2; :: thesis:
U6: lim (h # x) = -infty by U1, L1, MESFUNC5:def 12;
lim (Partial_Sums (g # x)) = -infty by U4, U5, MESFUNC5:def 12;
hence Sum (g # x) = f . x by L0, L1, U6, FUNCT_1:72; :: thesis:

end;

hence for x being Element of X st x in E holds
( g # x is summable & f . x = Sum (g # x) ) ; :: thesis:

per cases ;

suppose E = {} ; :: thesis:

hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,((g . n) | E) ) & I is summable & Integral M,(f | E) = Sum I ) by A1, A3, Q1, Cor131a; :: thesis:

end;

suppose V1: E <> {} ; :: thesis:

for m being Element of NAT holds
( g . m is_simple_func_in S & g . m is nonnegative & g . m is_measurable_on E & E c= dom (g . m) ) by Q1;
then E common_on_dom g by V1, SEQFUNC:def 10;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,((g . n) | E) ) & I is summable & Integral M,(f | E) = Sum I ) by A1, A2, A3, Q1, Q2, Q3, Cor131b; :: thesis:

end;