let seq be without-infty ExtREAL_sequence; :: thesis: Partial_Sums seq is without-infty ExtREAL_sequence
defpred S₁[ Nat] means (Partial_Sums seq) . $1 <> -infty ;
(Partial_Sums seq) . 0 = seq . 0 by MESFUNC9:def 1;
then (Partial_Sums seq) . 0 > -infty by MESFUNC5:def 5;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
A4: seq . (n + 1) > -infty by MESFUNC5:def 5;
(Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by MESFUNC9:def 1;
hence S₁[n + 1] by A3, A4, XXREAL_3:17; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);

hereby :: thesis: verum

assume Partial_Sums seq is not without-infty ExtREAL_sequence ; :: thesis: contradiction
then -infty in rng (Partial_Sums seq) by MESFUNC5:def 3;
then ex n being Element of NAT st -infty = (Partial_Sums seq) . n by FUNCT_2:113;
hence contradiction by A5; :: thesis: verum

end;