let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Element of NAT st not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_+infty holds
for n being Nat holds f . (n,m) is Real
let m be Element of NAT ; :: thesis: ( not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_+infty implies for n being Nat holds f . (n,m) is Real )
assume A2: not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_+infty ; :: thesis: for n being Nat holds f . (n,m) is Real
given N being Nat such that A3: f . (N,m) is not Real ; :: thesis: contradiction
not f . (N,m) in REAL by A3;
then A4: ( f . (N,m) = +infty or f . (N,m) = -infty ) by XXREAL_0:14;
reconsider N1 = N as Element of NAT by ORDINAL1:def 12;

now :: thesis: for g being Real st 0 < g holds
ex N being Nat st
for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k

let g be Real; :: thesis: ( 0 < g implies ex N being Nat st
for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k )
assume 0 < g ; :: thesis: ex N being Nat st
for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k
take N = N; :: thesis: for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k

hereby :: thesis: verum

let k be Nat; :: thesis: ( N <= k implies g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b₁ )
assume A7: N <= k ; :: thesis: g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b₁

per cases ( N = 0 or N <> 0 ) ;

suppose A8: N = 0 ; :: thesis: g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b₁

(ProjMap2 ((Partial_Sums_in_cod1 f),m)) . N = (Partial_Sums_in_cod1 f) . (N1,m) by MESFUNC9:def 7
.= f . (N,m) by A8, DefRSM ;
then A9: g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . N by A4, SUPINF_2:51, XXREAL_0:3;
(ProjMap2 ((Partial_Sums_in_cod1 f),m)) . N <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k by A7, RINFSUP2:7;
hence g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k by A9, XXREAL_0:2; :: thesis: verum

end;

suppose N <> 0 ; :: thesis: g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b₁

then consider N2 being Nat such that
A11: N = N2 + 1 by NAT_1:6;
reconsider N3 = N2 as Element of NAT by ORDINAL1:def 12;
A12: (Partial_Sums_in_cod1 f) . (N3,m) >= 0 by SUPINF_2:51;
(ProjMap2 ((Partial_Sums_in_cod1 f),m)) . N1 = (Partial_Sums_in_cod1 f) . (N1,m) by MESFUNC9:def 7
.= ((Partial_Sums_in_cod1 f) . (N2,m)) + (f . (N1,m)) by A11, DefRSM ;
then (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . N1 = +infty by A4, SUPINF_2:51, XXREAL_0:4, A12, XXREAL_3:39;
then (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k = +infty by XXREAL_0:4, A7, RINFSUP2:7;
hence g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . k by XXREAL_0:3; :: thesis: verum

end;

end;

end;

end;

hence contradiction by A2, MESFUNC5:def 9; :: thesis: verum