let X be non empty set ; :: thesis: for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let F be Functional_Sequence of X,REAL; :: thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) implies lim (Partial_Sums F) is E -measurable )

assume that

A1: ( dom (F . 0) = E & F is with_the_same_dom ) and

A2: for n being Nat holds (Partial_Sums F) . n is E -measurable and

A3: for x being Element of X st x in E holds

F # x is summable ; :: thesis: lim (Partial_Sums F) is E -measurable

hence lim (Partial_Sums F) is E -measurable by A2, A4, MESFUN7C:21; :: thesis: verum

for E being Element of S

for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let S be SigmaField of X; :: thesis: for E being Element of S

for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

let F be Functional_Sequence of X,REAL; :: thesis: ( dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) implies lim (Partial_Sums F) is E -measurable )

assume that

A1: ( dom (F . 0) = E & F is with_the_same_dom ) and

A2: for n being Nat holds (Partial_Sums F) . n is E -measurable and

A3: for x being Element of X st x in E holds

F # x is summable ; :: thesis: lim (Partial_Sums F) is E -measurable

A4: now :: thesis: for x being Element of X st x in E holds

(Partial_Sums F) # x is convergent

( dom ((Partial_Sums F) . 0) = E & Partial_Sums F is with_the_same_dom Functional_Sequence of X,REAL )
by A1, Th11, Th17;(Partial_Sums F) # x is convergent

let x be Element of X; :: thesis: ( x in E implies (Partial_Sums F) # x is convergent )

assume A5: x in E ; :: thesis: (Partial_Sums F) # x is convergent

then F # x is summable by A3;

then Partial_Sums (F # x) is convergent ;

hence (Partial_Sums F) # x is convergent by A1, A5, Th13; :: thesis: verum

end;assume A5: x in E ; :: thesis: (Partial_Sums F) # x is convergent

then F # x is summable by A3;

then Partial_Sums (F # x) is convergent ;

hence (Partial_Sums F) # x is convergent by A1, A5, Th13; :: thesis: verum

hence lim (Partial_Sums F) is E -measurable by A2, A4, MESFUN7C:21; :: thesis: verum