let X be non empty set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom implies Partial_Sums F is with_the_same_dom )

assume F is with_the_same_dom ; :: thesis: Partial_Sums F is with_the_same_dom

then Re F is with_the_same_dom ;

then Partial_Sums (Re F) is with_the_same_dom by Th17;

then Re (Partial_Sums F) is with_the_same_dom by Th29;

hence Partial_Sums F is with_the_same_dom by Th24; :: thesis: verum

Partial_Sums F is with_the_same_dom

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom implies Partial_Sums F is with_the_same_dom )

assume F is with_the_same_dom ; :: thesis: Partial_Sums F is with_the_same_dom

then Re F is with_the_same_dom ;

then Partial_Sums (Re F) is with_the_same_dom by Th17;

then Re (Partial_Sums F) is with_the_same_dom by Th29;

hence Partial_Sums F is with_the_same_dom by Th24; :: thesis: verum