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 and
A4: p . m = +infty by A2;
m in Seg (len p) by A3, FINSEQ_1:def 3;
then A5: len p >= m by FINSEQ_1:3;
consider f being Function of NAT ,ExtREAL such that
A6: Sum p = f . (len p) and
A7: f . 0 = 0. and
A8: for i being Element of NAT st i < len p holds
f . (i + 1) = (f . i) + (p . (i + 1)) by EXTREAL1:def 4;
defpred S₁[ Nat] means ( $1 <= len p implies ( ( $1 < m implies 0. <= f . $1 ) & ( $1 >= m implies f . $1 = +infty ) ) );
A9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A10: S₁[i] ; :: thesis: S₁[i + 1]
assume A11: 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 A12: i + 1 < m ; :: thesis: ( ( i + 1 < m implies 0. <= f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )

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

end;

case A14: 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 A15: i + 1 = m ; :: thesis: f . (i + 1) = +infty

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

end;

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

i < len p by A11, NAT_1:13;
then A17: f . (i + 1) = (f . i) + (p . (i + 1)) by A8;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A11, FINSEQ_1:3;
then i + 1 in dom p by FINSEQ_1:def 3;
then A18: p . (i + 1) <> -infty by A1;
i + 1 > m by A14, A16, XXREAL_0:1;
hence f . (i + 1) = +infty by A10, A11, A18, A17, 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;

A19: S₁[ 0 ] by A3, A7, FINSEQ_3:27;
for i being Nat holds S₁[i] from NAT_1:sch 2(A19, A9);
hence Sum p = +infty by A6, A5; :: thesis: verum