let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL
for n being Nat holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
let F be Functional_Sequence of X,REAL ; :: thesis: for n being Nat holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
let n be Nat; :: thesis: dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
A1: dom ((Partial_Sums (R_EAL F)) . n) = meet { (dom ((R_EAL F) . k)) where k is Element of NAT : k <= n } by Lem20, MESFUNC9:28;
(Partial_Sums (R_EAL F)) . n = (R_EAL (Partial_Sums F)) . n by Lm11;
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } by A1; :: thesis: verum