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

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

let n be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom implies dom ((Partial_Sums F) . n) = dom (F . 0) )

assume F is with_the_same_dom ; :: thesis: dom ((Partial_Sums F) . n) = dom (F . 0)

then Re F is with_the_same_dom ;

then dom ((Partial_Sums (Re F)) . n) = dom ((Re F) . 0) by Th11;

then dom ((Partial_Sums (Re F)) . n) = dom (F . 0) by MESFUN7C:def 11;

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

hence dom ((Partial_Sums F) . n) = dom (F . 0) by MESFUN7C:def 11; :: thesis: verum

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

let n be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom implies dom ((Partial_Sums F) . n) = dom (F . 0) )

assume F is with_the_same_dom ; :: thesis: dom ((Partial_Sums F) . n) = dom (F . 0)

then Re F is with_the_same_dom ;

then dom ((Partial_Sums (Re F)) . n) = dom ((Re F) . 0) by Th11;

then dom ((Partial_Sums (Re F)) . n) = dom (F . 0) by MESFUN7C:def 11;

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

hence dom ((Partial_Sums F) . n) = dom (F . 0) by MESFUN7C:def 11; :: thesis: verum