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

Partial_Sums F is with_the_same_dom

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

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

let n, m be Nat; :: according to MESFUNC8:def 2 :: thesis: dom ((Partial_Sums F) . n) = dom ((Partial_Sums F) . m)

dom ((Partial_Sums F) . n) = dom (F . 0) by A1, Th11;

hence dom ((Partial_Sums F) . n) = dom ((Partial_Sums F) . m) by A1, Th11; :: thesis: verum

Partial_Sums F is with_the_same_dom

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

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

let n, m be Nat; :: according to MESFUNC8:def 2 :: thesis: dom ((Partial_Sums F) . n) = dom ((Partial_Sums F) . m)

dom ((Partial_Sums F) . n) = dom (F . 0) by A1, Th11;

hence dom ((Partial_Sums F) . n) = dom ((Partial_Sums F) . m) by A1, Th11; :: thesis: verum