let p be FinSequence of ExtREAL ; :: thesis: ( ( for n being Nat st n in dom p holds
0. <= p . n ) & ex n being Nat st
( n in dom p & p . n = +infty ) implies Sum p = +infty )
assume that
A1: for n being Nat st n in dom p holds
0. <= p . n and
A2: ex n being Nat st
( n in dom p & p . n = +infty ) ; :: thesis: Sum p = +infty
consider m being Nat such that
A3: ( m in dom p & p . m = +infty ) by A2;
consider f being Function of NAT ,ExtREAL such that
A4: ( Sum p = f . (len p) & f . 0 = 0. & ( for i being Element of NAT st i < len p holds
f . (i + 1) = (f . i) + (p . (i + 1)) ) ) by CONVFUN1:def 5;
defpred S₁[ Nat] means ( $1 <= len p implies ( ( $1 < m implies 0. <= f . $1 ) & ( $1 >= m implies f . $1 = +infty ) ) );
A5: S₁[ 0 ] by A3, A4, FINSEQ_3:27;
A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
assume A8: i + 1 <= len p ; :: thesis: ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )
reconsider i = i as Element of NAT by ORDINAL1:def 13;

now

per cases ( i + 1 < m or i + 1 >= m ) ;

case A9: i + 1 < m ; :: thesis: ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )

A10: i <= i + 1 by NAT_1:11;
i < len p by A8, NAT_1:13;
then A11: f . (i + 1) = (f . i) + (p . (i + 1)) by A4;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A8, FINSEQ_1:3;
then i + 1 in dom p by FINSEQ_1:def 3;
then 0. <= p . (i + 1) by A1;
hence ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) by A7, A8, A9, A10, A11, XXREAL_0:2; :: thesis: verum

end;

case A12: i + 1 >= m ; :: thesis: ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )

now

per cases ( i + 1 = m or i + 1 <> m ) ;

case A13: i + 1 = m ; :: thesis: f . (i + 1) = +infty

i < len p by A8, NAT_1:13;
then f . (i + 1) = (f . i) + (p . (i + 1)) by A4;
hence f . (i + 1) = +infty by A3, A7, A8, A13, NAT_1:13, XXREAL_3:def 2; :: thesis: verum

end;

case i + 1 <> m ; :: thesis: f . (i + 1) = +infty

then A14: i + 1 > m by A12, XXREAL_0:1;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A8, FINSEQ_1:3;
then i + 1 in dom p by FINSEQ_1:def 3;
then A15: p . (i + 1) <> -infty by A1;
i < len p by A8, NAT_1:13;
then f . (i + 1) = (f . i) + (p . (i + 1)) by A4;
hence f . (i + 1) = +infty by A7, A8, A14, A15, NAT_1:13, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

hence ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; :: thesis: verum

end;

A16: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
m in Seg (len p) by A3, FINSEQ_1:def 3;
then len p >= m by FINSEQ_1:3;
hence Sum p = +infty by A4, A16; :: thesis: verum