let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be Function of X,ExtREAL; :: thesis:
let E be Finite_Sep_Sequence of S; :: thesis:
let F be summable FinSequence of Funcs (X,ExtREAL); :: thesis:
assume that
A1: dom E = dom F and
A2: dom f = union (rng E) and
A3: for n being Nat st n in dom F holds
ex r being Real st F /. n = r (#) (chi ((E . n),X)) and
A4: f = (Partial_Sums F) /. (len F) ; :: thesis:
E <> {} by A2, ZFMISC_1:2;
then 1 <= len E by FINSEQ_1:20;
then 1 <= len F by A1, FINSEQ_3:29;
then A5: len F in dom F by FINSEQ_3:25;
thus A6: for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & m <> n holds
(F /. n) . x = 0 :: thesis:

proof

let x be Element of X; :: thesis:
let m, n be Nat; :: thesis:
assume A7: ( m in dom F & n in dom F & x in E . m ) ; :: thesis:
then consider rn being Real such that
A8: F /. n = rn (#) (chi ((E . n),X)) by A3;
dom (F /. n) = X by FUNCT_2:def 1;
then A9: (F /. n) . x = rn * ((chi ((E . n),X)) . x) by A8, MESFUNC1:def 6;
thus ( m <> n implies (F /. n) . x = 0 ) :: thesis:

proof

assume m <> n ; :: thesis:
then not x in E . n by A7, XBOOLE_0:3, PROB_2:def 2;
then (chi ((E . n),X)) . x = 0 by FUNCT_3:def 3;
hence (F /. n) . x = 0 by A9; :: thesis:

end;

thus A10: for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n < m holds
((Partial_Sums F) /. n) . x = 0 :: thesis:

proof

let x be Element of X; :: thesis:
let m, n be Nat; :: thesis:
assume A11: ( m in dom F & n in dom F & x in E . m & n < m ) ; :: thesis:
defpred S₁[ Nat] means ( $1 in dom F & $1 < m implies ((Partial_Sums F) /. $1) . x = 0 );
A12: S₁[ 0 ] by FINSEQ_3:25;
A13: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A14: S₁[k] ; :: thesis:
assume A15: ( k + 1 in dom F & k + 1 < m ) ; :: thesis:
then A16: (F /. (k + 1)) . x = 0 by A6, A11;

per cases ;

suppose A17: k + 1 = 1 ; :: thesis:

(Partial_Sums F) /. (k + 1) = (Partial_Sums F) . (k + 1) by A15, Th10
.= F . (k + 1) by A17, MEASUR11:def 11
.= F /. (k + 1) by A15, PARTFUN1:def 6 ;
hence ((Partial_Sums F) /. (k + 1)) . x = 0 by A6, A11, A15; :: thesis:

end;

suppose A18: k + 1 <> 1 ; :: thesis:

( 1 <= k + 1 & k + 1 <= len F ) by A15, FINSEQ_3:25;
then ( 1 < k + 1 & k + 1 <= len F ) by A18, XXREAL_0:1;
then ( 1 <= k & k < len F ) by NAT_1:13;
then ((Partial_Sums F) /. (k + 1)) . x = 0 + ((F /. (k + 1)) . x) by A14, A15, NAT_1:13, FINSEQ_3:25, Th10;
hence ((Partial_Sums F) /. (k + 1)) . x = 0 by A16; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A13);
hence ((Partial_Sums F) /. n) . x = 0 by A11; :: thesis:

end;

thus A17: for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n >= m holds
((Partial_Sums F) /. n) . x = f . x :: thesis:

proof

let x be Element of X; :: thesis:
let m, n be Nat; :: thesis:
assume A18: ( m in dom F & n in dom F & x in E . m & n >= m ) ; :: thesis:
then A24: 1 <= m by FINSEQ_3:25;
defpred S₁[ Nat] means ( $1 in dom F & $1 >= m implies ((Partial_Sums F) /. $1) . x = (F /. m) . x );
A19: S₁[ 0 ] by FINSEQ_3:25;
A20: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A21: S₁[k] ; :: thesis:
assume A22: ( k + 1 in dom F & k + 1 >= m ) ; :: thesis:

per cases ;

suppose A23: k + 1 = 1 ; :: thesis:

(Partial_Sums F) /. (k + 1) = (Partial_Sums F) . (k + 1) by A22, Th10
.= F . (k + 1) by A23, MEASUR11:def 11
.= F /. (k + 1) by A22, PARTFUN1:def 6 ;
hence ((Partial_Sums F) /. (k + 1)) . x = (F /. m) . x by A22, A23, A24, XXREAL_0:1; :: thesis:

end;

suppose A25: k + 1 <> 1 ; :: thesis:

( 1 <= k + 1 & k + 1 <= len F ) by A22, FINSEQ_3:25;
then ( 1 < k + 1 & k + 1 <= len F ) by A25, XXREAL_0:1;
then A26: ( 1 <= k & k < len F ) by NAT_1:13;
then A27: k in dom F by FINSEQ_3:25;

per cases ;

suppose A28: k + 1 = m ; :: thesis:

then k < m by NAT_1:13;
then ((Partial_Sums F) /. k) . x = 0 by A10, A18, A27;
then ((Partial_Sums F) /. (k + 1)) . x = 0 + ((F /. (k + 1)) . x) by A26, Th10;
hence ((Partial_Sums F) /. (k + 1)) . x = (F /. m) . x by A28, XXREAL_3:4; :: thesis:

end;

suppose A29: k + 1 <> m ; :: thesis:

then m < k + 1 by A22, XXREAL_0:1;
then ((Partial_Sums F) /. (k + 1)) . x = ((F /. m) . x) + ((F /. (k + 1)) . x) by A21, A26, FINSEQ_3:25, NAT_1:13, Th10
.= ((F /. m) . x) + 0 by A6, A18, A22, A29 ;
hence ((Partial_Sums F) /. (k + 1)) . x = (F /. m) . x by XXREAL_3:4; :: thesis:

end;

A30: for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A20);
then ((Partial_Sums F) /. n) . x = (F /. m) . x by A18;
hence ((Partial_Sums F) /. n) . x = f . x by A4, A5, A18, A30, FINSEQ_3:25; :: thesis:

end;

thus A31: for x being Element of X
for m being Nat st m in dom F & x in E . m holds
(F /. m) . x = f . x :: thesis:

proof

let x be Element of X; :: thesis:
let m be Nat; :: thesis:
assume A32: ( m in dom F & x in E . m ) ; :: thesis:
then A33: ( 1 <= m & m <= len F ) by FINSEQ_3:25;
A34: ((Partial_Sums F) /. m) . x = f . x by A17, A32;

per cases ;

suppose m = 1 ; :: thesis:

then (Partial_Sums F) . m = F . m by MEASUR11:def 11;
then (Partial_Sums F) /. m = F . m by A32, Th10;
hence (F /. m) . x = f . x by A32, A34, PARTFUN1:def 6; :: thesis:

end;

suppose m <> 1 ; :: thesis:

then A35: m > 1 by A33, XXREAL_0:1;
reconsider m1 = m - 1 as Nat by A33;
A36: m = m1 + 1 ;
then A37: ( 1 <= m1 & m1 < len F ) by A33, A35, NAT_1:13;
then ( m1 in dom F & m1 < m ) by A36, NAT_1:19, FINSEQ_3:25;
then ((Partial_Sums F) /. m1) . x = 0 by A10, A32;
then f . x = 0 + ((F /. (m1 + 1)) . x) by A34, A37, Th10;
hence (F /. m) . x = f . x by XXREAL_3:4; :: thesis:

end;

A38: for x being Element of X st x in dom f holds
|.(f . x).| < +infty

proof

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
then consider A being set such that
A39: ( x in A & A in rng E ) by A2, TARSKI:def 4;
consider k being object such that
A40: ( k in dom E & A = E . k ) by A39, FUNCT_1:def 3;
reconsider k = k as Nat by A40;
consider r being Real such that
A41: F /. k = r (#) (chi ((E . k),X)) by A1, A3, A40;
dom (chi ((E . k),X)) = X by FUNCT_2:def 1;
then x in dom (chi ((E . k),X)) ;
then A42: x in dom (r (#) (chi ((E . k),X))) by MESFUNC1:def 6;
A43: (chi ((E . k),X)) . x = 1 by A39, A40, FUNCT_3:def 3;
f . x = (r (#) (chi ((E . k),X))) . x by A31, A39, A1, A40, A41;
then f . x = r * ((chi ((E . k),X)) . x) by A42, MESFUNC1:def 6;
hence |.(f . x).| < +infty by A43, EXTREAL1:41, XREAL_0:def 1; :: thesis:

end;

for n being Nat
for x, y being Element of X st n in dom E & x in E . n & y in E . n holds
f . x = f . y

proof

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume A44: ( n in dom E & x in E . n & y in E . n ) ; :: thesis:
then consider r being Real such that
A45: F /. n = r (#) (chi ((E . n),X)) by A3, A1;
dom (chi ((E . n),X)) = X by FUNCT_2:def 1;
then ( x in dom (chi ((E . n),X)) & y in dom (chi ((E . n),X)) ) ;
then A46: ( x in dom (r (#) (chi ((E . n),X))) & y in dom (r (#) (chi ((E . n),X))) ) by MESFUNC1:def 6;
A47: ( (chi ((E . n),X)) . x = 1 & (chi ((E . n),X)) . y = 1 ) by A44, FUNCT_3:def 3;
( (F /. n) . x = r * ((chi ((E . n),X)) . x) & (F /. n) . y = r * ((chi ((E . n),X)) . y) ) by A45, A46, MESFUNC1:def 6;
then ( (F /. n) . x = r & (F /. n) . y = r ) by A47, XXREAL_3:81;
then ( f . x = r & f . y = r ) by A1, A31, A44;
hence f . x = f . y ; :: thesis:

end;

hence f is_simple_func_in S by A2, A38, MESFUNC2:def 1, MESFUNC2:def 4; :: thesis: