let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let F be Functional_Sequence of X,ExtREAL; :: thesis: for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let n, m be Nat; :: thesis: for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
let z be set ; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) ) )
set PF = Partial_Sums F;
assume that
A1: z in dom ((Partial_Sums F) . n) and
A2: m <= n ; :: thesis: ( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )
thus A3: z in dom ((Partial_Sums F) . m) by A1, A2, Lm1; :: thesis: z in dom (F . m)

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: z in dom (F . m)

then (Partial_Sums F) . m = F . m by Def4;
hence z in dom (F . m) by A1, A2, Lm1; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: z in dom (F . m)

then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
(Partial_Sums F) . m = ((Partial_Sums F) . k) + (F . m) by A4, Def4;
then dom ((Partial_Sums F) . m) = ((dom ((Partial_Sums F) . k)) /\ (dom (F . m))) \ (((((Partial_Sums F) . k) " {-infty}) /\ ((F . m) " {+infty})) \/ ((((Partial_Sums F) . k) " {+infty}) /\ ((F . m) " {-infty}))) by MESFUNC1:def 3;
then z in (dom ((Partial_Sums F) . k)) /\ (dom (F . m)) by A3, XBOOLE_0:def 5;
hence z in dom (F . m) by XBOOLE_0:def 4; :: thesis: verum

end;

end;