let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive & F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0 )
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for n being Nat st F is additive & F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0 )
let n be Nat; :: thesis: ( F is additive & F is with_the_same_dom implies dom ((Partial_Sums F) . n) = dom (F . 0 ) )
assume A0: ( F is additive & F is with_the_same_dom ) ; :: thesis: dom ((Partial_Sums F) . n) = dom (F . 0 )

now

let D be set ; :: thesis: ( D in meet { (dom (F . k)) where k is Element of NAT : k <= n } implies D in meet {(dom (F . 0 ))} )
assume B1: D in meet { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: D in meet {(dom (F . 0 ))}
dom (F . 0 ) in { (dom (F . k)) where k is Element of NAT : k <= n } ;
then D in dom (F . 0 ) by B1, SETFAM_1:def 1;
hence D in meet {(dom (F . 0 ))} by SETFAM_1:11; :: thesis: verum

end;

then B2: meet { (dom (F . k)) where k is Element of NAT : k <= n } c= meet {(dom (F . 0 ))} by TARSKI:def 3;

now

let D be set ; :: thesis: ( D in meet {(dom (F . 0 ))} implies D in meet { (dom (F . k)) where k is Element of NAT : k <= n } )
assume D in meet {(dom (F . 0 ))} ; :: thesis: D in meet { (dom (F . k)) where k is Element of NAT : k <= n }
then B5: D in dom (F . 0 ) by SETFAM_1:11;
B3: dom (F . 0 ) in { (dom (F . k)) where k is Element of NAT : k <= n } ;
for E being set st E in { (dom (F . k)) where k is Element of NAT : k <= n } holds
D in E

proof

let E be set ; :: thesis: ( E in { (dom (F . k)) where k is Element of NAT : k <= n } implies D in E )
assume E in { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: D in E
then ex k1 being Element of NAT st
( E = dom (F . k1) & k1 <= n ) ;
hence D in E by B5, A0, MESFUNC8:def 2; :: thesis: verum

end;

hence D in meet { (dom (F . k)) where k is Element of NAT : k <= n } by B3, SETFAM_1:def 1; :: thesis: verum

end;

then meet {(dom (F . 0 ))} c= meet { (dom (F . k)) where k is Element of NAT : k <= n } by TARSKI:def 3;
then meet { (dom (F . k)) where k is Element of NAT : k <= n } = meet {(dom (F . 0 ))} by B2, XBOOLE_0:def 10;
then dom ((Partial_Sums F) . n) = meet {(dom (F . 0 ))} by A0, Lem07;
hence dom ((Partial_Sums F) . n) = dom (F . 0 ) by SETFAM_1:11; :: thesis: verum