let F be FinSequence of ExtREAL ; :: thesis: ( ( F is without-infty implies Sum F <> -infty ) & ( F is without+infty implies Sum F <> +infty ) )

hereby :: thesis: ( F is without+infty implies Sum F <> +infty )

assume F is without-infty ; :: thesis: Sum F <> -infty
then A1: not -infty in rng F by MESFUNC5:def 3;
consider S being sequence of ExtREAL such that
A2: ( Sum F = S . (len F) & S . 0 = 0 & ( for n being Nat st n < len F holds
S . (n + 1) = (S . n) + (F . (n + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len F implies S . $1 <> -infty );
A3: S₁[ 0 ] by A2;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
assume A6: n + 1 <= len F ; :: thesis: S . (n + 1) <> -infty
then A7: S . (n + 1) = (S . n) + (F . (n + 1)) by A2, NAT_1:13;
n + 1 in dom F by A6, NAT_1:11, FINSEQ_3:25;
then F . (n + 1) in rng F by FUNCT_1:3;
hence S . (n + 1) <> -infty by A1, A5, NAT_1:13, A6, A7, XXREAL_3:17; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence Sum F <> -infty by A2; :: thesis: verum

end;

assume F is without+infty ; :: thesis: Sum F <> +infty
then A8: not +infty in rng F by MESFUNC5:def 4;
consider S being sequence of ExtREAL such that
A9: ( Sum F = S . (len F) & S . 0 = 0 & ( for n being Nat st n < len F holds
S . (n + 1) = (S . n) + (F . (n + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len F implies S . $1 <> +infty );
A10: S₁[ 0 ] by A9;
A11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A12: S₁[n] ; :: thesis: S₁[n + 1]
assume A13: n + 1 <= len F ; :: thesis: S . (n + 1) <> +infty
then A14: S . (n + 1) = (S . n) + (F . (n + 1)) by A9, NAT_1:13;
n + 1 in dom F by A13, NAT_1:11, FINSEQ_3:25;
then F . (n + 1) in rng F by FUNCT_1:3;
hence S . (n + 1) <> +infty by A8, A12, NAT_1:13, A13, A14, XXREAL_3:16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A11);
hence Sum F <> +infty by A9; :: thesis: verum