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 }
( dom ((Partial_Sums (R_EAL F)) . n) = meet { (dom ((R_EAL F) . k)) where k is Element of NAT : k <= n } & (Partial_Sums (R_EAL F)) . n = (R_EAL (Partial_Sums F)) . n ) by Th7, Th9, MESFUNC9:28;
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: verum