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;
assume A1: F is additive ; :: thesis: dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
defpred S₁[ Nat] means dom ((Partial_Sums F) . $1) = meet { (dom (F . k)) where k is Element of NAT : k <= $1 } ;
A2: dom ((Partial_Sums F) . 0 ) = dom (F . 0 ) by Def0;

now

let V be set ; :: 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 A3: {(dom (F . 0 ))} c= H₁( 0 ) by TARSKI:def 3;

now

let V be set ; :: 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
A4: ( V = dom (F . k) & k <= 0 ) ;
k = 0 by A4;
hence V in {(dom (F . 0 ))} by A4, TARSKI:def 1; :: thesis: verum

end;

then H₁( 0 ) c= {(dom (F . 0 ))} by TARSKI:def 3;
then H₁( 0 ) = {(dom (F . 0 ))} by A3, XBOOLE_0:def 10;
then P0: S₁[ 0 ] by A2, SETFAM_1:11;
P1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume L0: S₁[m] ; :: thesis: S₁[m + 1]
L3: ( (((Partial_Sums F) . m) " {-infty }) /\ ((F . (m + 1)) " {+infty }) = {} & (((Partial_Sums F) . m) " {+infty }) /\ ((F . (m + 1)) " {-infty }) = {} ) by A1, Lem07b;
(Partial_Sums F) . (m + 1) = ((Partial_Sums F) . m) + (F . (m + 1)) by Def0;
then L5: dom ((Partial_Sums F) . (m + 1)) = ((dom ((Partial_Sums F) . m)) /\ (dom (F . (m + 1)))) \ ({} \/ {} ) by L3, MESFUNC1:def 3;
L41: ( dom (F . 0 ) in H₁(m + 1) & dom (F . 0 ) in H₁(m) ) ;

now

let V be set ; :: thesis: ( V in meet H₁(m + 1) implies V in (meet H₁(m)) /\ (dom (F . (m + 1))) )
assume L40: 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 L43: V in dom (F . (m + 1)) by L40, SETFAM_1:def 1;

now

let V be set ; :: 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
L44: ( V = dom (F . i) & i <= m ) ;
i <= m + 1 by L44, NAT_1:12;
hence V in H₁(m + 1) by L44; :: thesis: verum

end;

then H₁(m) c= H₁(m + 1) by TARSKI:def 3;
then meet H₁(m + 1) c= meet H₁(m) by L41, SETFAM_1:7;
hence V in (meet H₁(m)) /\ (dom (F . (m + 1))) by L40, L43, XBOOLE_0:def 4; :: thesis: verum

end;

then L45: meet H₁(m + 1) c= (meet H₁(m)) /\ (dom (F . (m + 1))) by TARSKI:def 3;

now

let V be set ; :: thesis: ( V in (meet H₁(m)) /\ (dom (F . (m + 1))) implies V in meet H₁(m + 1) )
assume V in (meet H₁(m)) /\ (dom (F . (m + 1))) ; :: thesis: V in meet H₁(m + 1)
then L46: ( V in meet H₁(m) & V in dom (F . (m + 1)) ) by 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
L48: ( W = dom (F . i) & i <= m + 1 ) ;

now

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

end;

hence V in W by L48, L46, NAT_1:8; :: thesis: verum

end;

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

end;

then (meet H₁(m)) /\ (dom (F . (m + 1))) c= meet H₁(m + 1) by TARSKI:def 3;
hence S₁[m + 1] by L0, L5, L45, XBOOLE_0:def 10; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(P0, P1);
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: verum