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 ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

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

for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

let F be Functional_Sequence of X,REAL; :: thesis: ( ( for x being Element of X st x in E holds

F # x is summable ) implies for x being Element of X st x in E holds

(F || E) # x is summable )

set G = F || E;

assume A1: for x being Element of X st x in E holds

F # x is summable ; :: thesis: for x being Element of X st x in E holds

(F || E) # x is summable

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

assume A2: x in E ; :: thesis: (F || E) # x is summable

for n being Element of NAT holds (F # x) . n = ((F || E) # x) . n

F # x is summable by A1, A2;

then Partial_Sums (F # x) is convergent ;

hence (F || E) # x is summable by A3; :: thesis: verum

for E being Element of S

for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

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

for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

let F be Functional_Sequence of X,REAL; :: thesis: ( ( for x being Element of X st x in E holds

F # x is summable ) implies for x being Element of X st x in E holds

(F || E) # x is summable )

set G = F || E;

assume A1: for x being Element of X st x in E holds

F # x is summable ; :: thesis: for x being Element of X st x in E holds

(F || E) # x is summable

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

assume A2: x in E ; :: thesis: (F || E) # x is summable

for n being Element of NAT holds (F # x) . n = ((F || E) # x) . n

proof

then A3:
Partial_Sums (F # x) = Partial_Sums ((F || E) # x)
by FUNCT_2:63;
let n be Element of NAT ; :: thesis: (F # x) . n = ((F || E) # x) . n

(F # x) . n = (F . n) . x by SEQFUNC:def 10;

then (F # x) . n = ((F . n) | E) . x by A2, FUNCT_1:49;

then (F # x) . n = ((F || E) . n) . x by Def1;

hence (F # x) . n = ((F || E) # x) . n by SEQFUNC:def 10; :: thesis: verum

end;(F # x) . n = (F . n) . x by SEQFUNC:def 10;

then (F # x) . n = ((F . n) | E) . x by A2, FUNCT_1:49;

then (F # x) . n = ((F || E) . n) . x by Def1;

hence (F # x) . n = ((F || E) # x) . n by SEQFUNC:def 10; :: thesis: verum

F # x is summable by A1, A2;

then Partial_Sums (F # x) is convergent ;

hence (F || E) # x is summable by A3; :: thesis: verum