let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL

for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let F be Functional_Sequence of X,REAL; :: thesis: for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let n, m be Nat; :: thesis: for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let z be set ; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )

(Partial_Sums F) . n = (R_EAL (Partial_Sums F)) . n ;

then A1: (Partial_Sums F) . n = (Partial_Sums (R_EAL F)) . n by Th7;

(Partial_Sums (R_EAL F)) . m = (R_EAL (Partial_Sums F)) . m by Th7;

hence ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) ) by A1, MESFUNC9:22; :: thesis: verum

for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let F be Functional_Sequence of X,REAL; :: thesis: for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let n, m be Nat; :: thesis: for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

let z be set ; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )

(Partial_Sums F) . n = (R_EAL (Partial_Sums F)) . n ;

then A1: (Partial_Sums F) . n = (Partial_Sums (R_EAL F)) . n by Th7;

(Partial_Sums (R_EAL F)) . m = (R_EAL (Partial_Sums F)) . m by Th7;

hence ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) ) by A1, MESFUNC9:22; :: thesis: verum