let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL
for n being Nat st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0 )
let F be Functional_Sequence of X,REAL ; :: thesis: for n being Nat st F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0 )
let n be Nat; :: 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 dom ((Partial_Sums (R_EAL F)) . n) = dom ((R_EAL F) . 0 ) by Lem20, MESFUNC9:29;
then dom ((R_EAL (Partial_Sums F)) . n) = dom ((R_EAL F) . 0 ) by Lm11;
hence dom ((Partial_Sums F) . n) = dom (F . 0 ) ; :: thesis: verum