let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive 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,ExtREAL; :: thesis: for n being Nat st F is additive holds
dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
let n be Nat; :: thesis: ( F is additive implies dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } )
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;

now :: thesis: for V being object st V in H₁( 0 ) holds
V in {(dom (F . 0))}

let V be object ; :: thesis: ( V in H₁( 0 ) implies V in {(dom (F . 0))} )
assume V in H₁( 0 ) ; :: thesis: V in {(dom (F . 0))}
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: verum

end;

then A4: H₁( 0 ) c= {(dom (F . 0))} ;
assume A5: F is additive ; :: thesis: dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
A6: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
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) ;

now :: thesis: for V being object st V in (meet H₁(m)) /\ (dom (F . (m + 1))) holds
V in meet H₁(m + 1)

let V be object ; :: thesis: ( V in (meet H₁(m)) /\ (dom (F . (m + 1))) implies V in meet H₁(m + 1) )
assume A10: V in (meet H₁(m)) /\ (dom (F . (m + 1))) ; :: thesis: V in meet H₁(m + 1)
then A11: V in dom (F . (m + 1)) by XBOOLE_0:def 4;
A12: V in meet H₁(m) by A10, XBOOLE_0:def 4;
for W being set st W in H₁(m + 1) holds
V in W

proof

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

now :: thesis: ( i <= m implies V in W )

assume i <= m ; :: thesis: V in W
then W in H₁(m) by A13;
hence V in W by A12, SETFAM_1:def 1; :: thesis: verum

end;

hence V in W by A11, A13, A14, NAT_1:8; :: thesis: verum

end;

hence V in meet H₁(m + 1) by A9, SETFAM_1:def 1; :: thesis: verum

end;

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

now :: thesis: for V being object st V in meet H₁(m + 1) holds
V in (meet H₁(m)) /\ (dom (F . (m + 1)))

now :: thesis: for V being object st V in H₁(m) holds
V in H₁(m + 1)

let V be object ; :: thesis: ( V in H₁(m) implies V in H₁(m + 1) )
assume V in H₁(m) ; :: thesis: V in H₁(m + 1)
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: verum

end;

then H₁(m) c= H₁(m + 1) ;
then A19: meet H₁(m + 1) c= meet H₁(m) by A16, SETFAM_1:6;
let V be object ; :: thesis: ( V in meet H₁(m + 1) implies V in (meet H₁(m)) /\ (dom (F . (m + 1))) )
assume A20: V in meet H₁(m + 1) ; :: thesis: V in (meet H₁(m)) /\ (dom (F . (m + 1)))
dom (F . (m + 1)) in H₁(m + 1) ;
then V in dom (F . (m + 1)) by A20, SETFAM_1:def 1;
hence V in (meet H₁(m)) /\ (dom (F . (m + 1))) by A20, A19, XBOOLE_0:def 4; :: thesis: verum

end;

then A21: meet H₁(m + 1) c= (meet H₁(m)) /\ (dom (F . (m + 1))) ;
(((Partial_Sums F) . m) " {-infty}) /\ ((F . (m + 1)) " {+infty}) = {} by A5, Th27;
then A22: dom ((Partial_Sums F) . (m + 1)) = ((dom ((Partial_Sums F) . m)) /\ (dom (F . (m + 1)))) \ ({} \/ {}) by A8, A7, MESFUNC1:def 3;
assume S₁[m] ; :: thesis: S₁[m + 1]
hence S₁[m + 1] by A22, A21, A15, XBOOLE_0:def 10; :: thesis: verum

end;

now :: thesis: for V being object st V in {(dom (F . 0))} holds
V in H₁( 0 )

let V be object ; :: thesis: ( V in {(dom (F . 0))} implies V in H₁( 0 ) )
assume V in {(dom (F . 0))} ; :: thesis: V in H₁( 0 )
then V = dom (F . 0) by TARSKI:def 1;
hence V in H₁( 0 ) ; :: thesis: verum

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: verum