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)
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)
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)
let z be set ; :: thesis: ( z in dom ((Partial_Sums F) . n) & m <= n implies z in dom ((Partial_Sums 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)
defpred S₁[ Nat] means ( m <= $1 & $1 <= n implies not z in dom ((Partial_Sums F) . $1) );
assume A3: not z in dom ((Partial_Sums F) . m) ; :: thesis: contradiction
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume that
A6: m <= k + 1 and
A7: k + 1 <= n ; :: thesis: not z in dom ((Partial_Sums F) . (k + 1))

per cases ( m <= k or m = k + 1 ) by A6, NAT_1:8;

suppose A8: m <= k ; :: thesis: not z in dom ((Partial_Sums F) . (k + 1))

(Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by Def4;
then A9: dom ((Partial_Sums F) . (k + 1)) = ((dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1)))) \ (((((Partial_Sums F) . k) " {-infty}) /\ ((F . (k + 1)) " {+infty})) \/ ((((Partial_Sums F) . k) " {+infty}) /\ ((F . (k + 1)) " {-infty}))) by MESFUNC1:def 3;
not z in (dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1))) by A5, A7, A8, NAT_1:13, XBOOLE_0:def 4;
hence not z in dom ((Partial_Sums F) . (k + 1)) by A9, XBOOLE_0:def 5; :: thesis: verum

end;

suppose m = k + 1 ; :: thesis: not z in dom ((Partial_Sums F) . (k + 1))

hence not z in dom ((Partial_Sums F) . (k + 1)) by A3; :: thesis: verum

end;

end;

end;

A10: S₁[ 0 ] by A3;
for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A4);
hence contradiction by A1, A2; :: thesis: verum