let X be non empty set ; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
let n be Nat; :: thesis:
deffunc H₁( Nat) -> set = { (dom (F . k)) where k is Element of NAT : k <= $1 } ;
set PF = Partial_Sums F;
defpred S₁[ Nat] means dom ((Partial_Sums F) . $1) = meet { (dom (F . k)) where k is Element of NAT : k <= $1 } ;
A1: dom ((Partial_Sums F) . 0) = dom (F . 0) by Def4;

let V be object ; :: thesis:
assume V in H₁( 0 ) ; :: thesis:
then consider k being Element of NAT such that
A2: V = dom (F . k) and
A3: k <= 0 ;
k = 0 by A3;
hence V in {(dom (F . 0))} by A2, TARSKI:def 1; :: thesis:

end;

let m be Nat; :: thesis:
A7: (Partial_Sums F) . (m + 1) = ((Partial_Sums F) . m) + (F . (m + 1)) by Def4;
A8: (((Partial_Sums F) . m) " {+infty}) /\ ((F . (m + 1)) " {-infty}) = {} by A5, Th27;
A9: dom (F . 0) in H₁(m + 1) ;

let W be set ; :: thesis:
assume W in H₁(m + 1) ; :: thesis:
then consider i being Element of NAT such that
A13: W = dom (F . i) and
A14: i <= m + 1 ;

end;

end;

end;

then A15: (meet H₁(m)) /\ (dom (F . (m + 1))) c= meet H₁(m + 1) ;
A16: dom (F . 0) in H₁(m) ;

let V be object ; :: thesis:
assume V in H₁(m) ; :: thesis:
then consider i being Element of NAT such that
A17: V = dom (F . i) and
A18: i <= m ;
i <= m + 1 by A18, NAT_1:12;
hence V in H₁(m + 1) by A17; :: thesis:

end;

end;

end;

end;

then {(dom (F . 0))} c= H₁( 0 ) ;
then H₁( 0 ) = {(dom (F . 0))} by A4, XBOOLE_0:def 10;
then A23: S₁[ 0 ] by A1, SETFAM_1:10;
for k being Nat holds S₁[k] from NAT_1:sch 2(A23, A6);
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: