let X be non empty set ; :: thesis: for n, m being Nat

for z being set

for F being Functional_Sequence of X,COMPLEX 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

for F being Functional_Sequence of X,COMPLEX 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: for F being Functional_Sequence of X,COMPLEX 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,COMPLEX; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )

assume A1: ( z in dom ((Partial_Sums F) . n) & m <= n ) ; :: thesis: ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

A2: dom ((Partial_Sums F) . n) = dom ((Re (Partial_Sums F)) . n) by MESFUN7C:def 11

.= dom ((Partial_Sums (Re F)) . n) by Th29 ;

dom ((Partial_Sums (Re F)) . m) = dom ((Re (Partial_Sums F)) . m) by Th29

.= dom ((Partial_Sums F) . m) by MESFUN7C:def 11 ;

hence z in dom ((Partial_Sums F) . m) by A1, A2, Th8; :: thesis: z in dom (F . m)

z in dom ((Re F) . m) by A1, A2, Th8;

hence z in dom (F . m) by MESFUN7C:def 11; :: thesis: verum

for z being set

for F being Functional_Sequence of X,COMPLEX 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

for F being Functional_Sequence of X,COMPLEX 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: for F being Functional_Sequence of X,COMPLEX 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,COMPLEX; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )

assume A1: ( z in dom ((Partial_Sums F) . n) & m <= n ) ; :: thesis: ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

A2: dom ((Partial_Sums F) . n) = dom ((Re (Partial_Sums F)) . n) by MESFUN7C:def 11

.= dom ((Partial_Sums (Re F)) . n) by Th29 ;

dom ((Partial_Sums (Re F)) . m) = dom ((Re (Partial_Sums F)) . m) by Th29

.= dom ((Partial_Sums F) . m) by MESFUN7C:def 11 ;

hence z in dom ((Partial_Sums F) . m) by A1, A2, Th8; :: thesis: z in dom (F . m)

z in dom ((Re F) . m) by A1, A2, Th8;

hence z in dom (F . m) by MESFUN7C:def 11; :: thesis: verum