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 that
A1: F is additive and
A2: 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 ))} )
A3: dom (F . 0 ) in { (dom (F . k)) where k is Element of NAT : k <= n } ;
assume D in meet { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: D in meet {(dom (F . 0 ))}
then D in dom (F . 0 ) by A3, SETFAM_1:def 1;
hence D in meet {(dom (F . 0 ))} by SETFAM_1:11; :: thesis: verum

end;

then A4: 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 A5: D in dom (F . 0 ) by SETFAM_1:11;
A6: 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 A2, A5, MESFUNC8:def 2; :: thesis: verum

end;

dom (F . 0 ) in { (dom (F . k)) where k is Element of NAT : k <= n } ;
hence D in meet { (dom (F . k)) where k is Element of NAT : k <= n } by A6, 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 A4, XBOOLE_0:def 10;
then dom ((Partial_Sums F) . n) = meet {(dom (F . 0 ))} by A1, Th28;
hence dom ((Partial_Sums F) . n) = dom (F . 0 ) by SETFAM_1:11; :: thesis: verum