let p be FinSequence of ExtREAL ; :: thesis: ( not -infty in rng p & +infty in rng p implies Sum p = +infty )
assume A1: not -infty in rng p ; :: thesis: ( not +infty in rng p or Sum p = +infty )
assume +infty in rng p ; :: thesis: Sum p = +infty
then ex n being object st
( n in dom p & p . n = +infty ) by FUNCT_1:def 3;
then consider m being Nat such that
A2: m in dom p and
A3: p . m = +infty ;
m in Seg (len p) by A2, FINSEQ_1:def 3;
then A4: len p >= m by FINSEQ_1:1;
consider f being sequence of ExtREAL such that
A5: Sum p = f . (len p) and
A6: f . 0 = 0. and
A7: for i being Nat st i < len p holds
f . (i + 1) = (f . i) + (p . (i + 1)) by EXTREAL1:def 2;
A8: for n being Nat st n in dom p holds
-infty < p . n

proof

let n be Nat; :: thesis: ( n in dom p implies -infty < p . n )
assume n in dom p ; :: thesis: -infty < p . n
then p . n in rng p by FUNCT_1:def 3;
hence -infty < p . n by A1, XXREAL_0:6; :: thesis: verum

end;

defpred S₁[ Nat] means ( $1 <= len p implies ( ( $1 < m implies -infty < 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 -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) )
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A12: i < len p by A11, NAT_1:13;

now :: thesis: ( ( i + 1 < m & -infty < f . (i + 1) ) or ( i + 1 >= m & ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) )

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

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

1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len p) by A11, FINSEQ_1:1;
then i + 1 in dom p by FINSEQ_1:def 3;
then A13: -infty < p . (i + 1) by A8;
A14: -infty + -infty = -infty by XXREAL_3:def 2;
-infty + -infty < (f . i) + (p . (i + 1)) by A10, A11, A13, NAT_1:13, XXREAL_3:64;
hence -infty < f . (i + 1) by A7, A12, A14; :: thesis: verum

end;

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

now :: thesis: ( ( i + 1 = m & f . (i + 1) = +infty ) or ( i + 1 <> m & f . (i + 1) = +infty ) )

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

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

f . (i + 1) = (f . i) + (p . (i + 1)) by A7, A12;
hence f . (i + 1) = +infty by A3, A10, A11, A16, NAT_1:13, XXREAL_3:def 2; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;

end;

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

end;

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