let f be nonnegative Function of [:NAT,NAT:],ExtREAL; 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 ; ( 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
; for n being Nat holds f . (n,m) is Real
given N being Nat such that A3:
f . (N,m) is not Real
; 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 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)) . klet g be
Real;
( 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
;
ex N being Nat st
for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . ktake N =
N;
for k being Nat st N <= k holds
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . khereby verum
let k be
Nat;
( N <= k implies g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b1 )assume A7:
N <= k
;
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b1per cases
( N = 0 or N <> 0 )
;
suppose A8:
N = 0
;
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b1(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;
verum end; suppose
N <> 0
;
g <= (ProjMap2 ((Partial_Sums_in_cod1 f),m)) . b1then 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;
verum end;
end; end;
hence
contradiction
by A2, MESFUNC5:def 9; verum