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 :: thesis: for D being object st D in meet { (dom (F . k)) where k is Element of NAT : k <= n } holds
D in meet {(dom (F . 0))}

let D be object ; :: 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:10; :: thesis: verum

end;

then A4: meet { (dom (F . k)) where k is Element of NAT : k <= n } c= meet {(dom (F . 0))} ;

now :: thesis: for D being object st D in meet {(dom (F . 0))} holds
D in meet { (dom (F . k)) where k is Element of NAT : k <= n }

let D be object ; :: 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:10;
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; :: 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 } ;
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:10; :: thesis: verum