:: Extended Real Valued Double Sequence and Its Convergence
:: by Noboru Endou
::
:: Received July 1, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


Lm1: for X being set
for x being object holds (X --> 0.) . x = 0
proof end;

registration
let X be non empty set ;
cluster non empty V7() V10(X) V11( REAL ) Function-like total V32(X, REAL ) complex-valued ext-real-valued real-valued nonnegative nonpositive for Element of bool [:X,REAL:];
existence
ex b1 being Function of X,REAL st
( b1 is nonnegative & b1 is nonpositive )
proof end;
end;

registration
let X be non empty set ;
cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued nonnegative nonpositive V183() V184() for Element of bool [:X,ExtREAL:];
existence
ex b1 being Function of X,ExtREAL st
( b1 is V183() & b1 is V184() & b1 is nonnegative & b1 is nonpositive )
proof end;
end;

Lm2: for X being non empty set holds
( X --> 0. is V183() Function of X,ExtREAL & X --> 0. is V184() Function of X,ExtREAL )
proof end;

registration
let X be non empty set ;
cluster Function-like V32(X, ExtREAL ) nonnegative -> V183() for Element of bool [:X,ExtREAL:];
correctness
coherence
for b1 being Function of X,ExtREAL st b1 is nonnegative holds
b1 is V183();
proof end;
cluster Function-like V32(X, ExtREAL ) nonpositive -> V184() for Element of bool [:X,ExtREAL:];
correctness
coherence
for b1 being Function of X,ExtREAL st b1 is nonpositive holds
b1 is V184();
proof end;
cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued V183() V184() for Element of bool [:X,ExtREAL:];
existence
not for b1 being V184() Function of X,ExtREAL holds b1 is V183()
proof end;
end;

definition
let X be non empty set ;
let f be Function of X,ExtREAL;
:: original: -
redefine func - f -> Function of X,ExtREAL;
correctness
coherence
- f is Function of X,ExtREAL;
proof end;
end;

registration
let X be non empty set ;
let f be V183() Function of X,ExtREAL;
cluster - f -> V184() ;
correctness
coherence
- f is without+infty ;
proof end;
end;

registration
let X be non empty set ;
let f be V184() Function of X,ExtREAL;
cluster - f -> V183() ;
correctness
coherence
- f is without-infty ;
proof end;
end;

registration
let X be non empty set ;
let f be nonnegative Function of X,ExtREAL;
cluster - f -> nonpositive ;
correctness
coherence
- f is nonpositive ;
proof end;
end;

registration
let X be non empty set ;
let f be nonpositive Function of X,ExtREAL;
cluster - f -> nonnegative ;
correctness
coherence
- f is nonnegative ;
proof end;
end;

registration
let A, B be non empty set ;
let f be V183() Function of [:A,B:],ExtREAL;
cluster ~ f -> without-infty ;
correctness
coherence
~ f is without-infty ;
proof end;
end;

registration
let A, B be non empty set ;
let f be V184() Function of [:A,B:],ExtREAL;
cluster ~ f -> without+infty ;
correctness
coherence
~ f is without+infty ;
proof end;
end;

registration
let A, B be non empty set ;
let f be nonnegative Function of [:A,B:],ExtREAL;
cluster ~ f -> nonnegative ;
correctness
coherence
~ f is nonnegative ;
proof end;
end;

registration
let A, B be non empty set ;
let f be nonpositive Function of [:A,B:],ExtREAL;
cluster ~ f -> nonpositive ;
correctness
coherence
~ f is nonpositive ;
proof end;
end;

theorem Th1: :: DBLSEQ_3:1
for seq being ExtREAL_sequence holds Partial_Sums (- seq) = - (Partial_Sums seq)
proof end;

theorem Th2: :: DBLSEQ_3:2
for X being non empty set
for f being PartFunc of X,ExtREAL holds - (- f) = f
proof end;

theorem :: DBLSEQ_3:3
for X, Y being non empty set
for f being Function of [:X,Y:],ExtREAL holds ~ (- f) = - (~ f)
proof end;

registration
let seq be nonnegative ExtREAL_sequence;
cluster Partial_Sums seq -> nonnegative ;
correctness
coherence
Partial_Sums seq is nonnegative ;
by MESFUNC9:16;
end;

registration
let seq be nonpositive ExtREAL_sequence;
cluster Partial_Sums seq -> nonpositive ;
correctness
coherence
Partial_Sums seq is nonpositive ;
proof end;
end;

theorem Th4: :: DBLSEQ_3:4
for seq being nonnegative ExtREAL_sequence
for m being Nat holds seq . m <= (Partial_Sums seq) . m
proof end;

theorem :: DBLSEQ_3:5
for seq being nonpositive ExtREAL_sequence
for m being Nat holds seq . m >= (Partial_Sums seq) . m
proof end;

theorem :: DBLSEQ_3:6
for X being non empty set
for f being V183() V184() Function of X,ExtREAL holds f is Function of X,REAL
proof end;

definition
let X be non empty set ;
let f1, f2 be V183() Function of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V183() Function of X,ExtREAL;
correctness
coherence
f1 + f2 is V183() Function of X,ExtREAL;
proof end;
end;

definition
let X be non empty set ;
let f1, f2 be V184() Function of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V184() Function of X,ExtREAL;
correctness
coherence
f1 + f2 is V184() Function of X,ExtREAL;
proof end;
end;

definition
let X be non empty set ;
let f1 be V183() Function of X,ExtREAL;
let f2 be V184() Function of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V183() Function of X,ExtREAL;
correctness
coherence
f1 - f2 is V183() Function of X,ExtREAL;
proof end;
end;

definition
let X be non empty set ;
let f1 be V184() Function of X,ExtREAL;
let f2 be V183() Function of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V184() Function of X,ExtREAL;
correctness
coherence
f1 - f2 is V184() Function of X,ExtREAL;
proof end;
end;

theorem Th7: :: DBLSEQ_3:7
for X being non empty set
for x being Element of X
for f1, f2 being Function of X,ExtREAL holds
( ( f1 is V183() & f2 is V183() implies (f1 + f2) . x = (f1 . x) + (f2 . x) ) & ( f1 is V184() & f2 is V184() implies (f1 + f2) . x = (f1 . x) + (f2 . x) ) & ( f1 is V183() & f2 is V184() implies (f1 - f2) . x = (f1 . x) - (f2 . x) ) & ( f1 is V184() & f2 is V183() implies (f1 - f2) . x = (f1 . x) - (f2 . x) ) )
proof end;

Lm3: for X being non empty set
for f1, f2 being V183() Function of X,ExtREAL holds f1 + f2 = f1 - (- f2)
proof end;

Lm4: for X being non empty set
for f1, f2 being V184() Function of X,ExtREAL holds f1 + f2 = f1 - (- f2)
proof end;

Lm5: for X being non empty set
for f1 being V183() Function of X,ExtREAL
for f2 being V184() Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) )
proof end;

theorem Th8: :: DBLSEQ_3:8
for X being non empty set
for f1, f2 being V183() Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )
proof end;

theorem Th9: :: DBLSEQ_3:9
for X being non empty set
for f1, f2 being V184() Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )
proof end;

theorem Th10: :: DBLSEQ_3:10
for X being non empty set
for f1 being V183() Function of X,ExtREAL
for f2 being V184() Function of X,ExtREAL holds
( f1 - f2 = f1 + (- f2) & f2 - f1 = f2 + (- f1) & - (f1 - f2) = (- f1) + f2 & - (f2 - f1) = (- f2) + f1 )
proof end;

definition
let f be Function of [:NAT,NAT:],ExtREAL;
let n, m be Nat;
:: original: .
redefine func f . (n,m) -> Element of ExtREAL ;
coherence
f . (n,m) is Element of ExtREAL
proof end;
end;

theorem Th11: :: DBLSEQ_3:11
for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds (f1 + f2) . (n,m) = (f1 . (n,m)) + (f2 . (n,m))
proof end;

theorem :: DBLSEQ_3:12
for f1, f2 being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds (f1 + f2) . (n,m) = (f1 . (n,m)) + (f2 . (n,m))
proof end;

theorem :: DBLSEQ_3:13
for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (f1 - f2) . (n,m) = (f1 . (n,m)) - (f2 . (n,m)) & (f2 - f1) . (n,m) = (f2 . (n,m)) - (f1 . (n,m)) )
proof end;

theorem :: DBLSEQ_3:14
for X, Y being non empty set
for f1, f2 being V183() Function of [:X,Y:],ExtREAL holds ~ (f1 + f2) = (~ f1) + (~ f2)
proof end;

theorem :: DBLSEQ_3:15
for X, Y being non empty set
for f1, f2 being V184() Function of [:X,Y:],ExtREAL holds ~ (f1 + f2) = (~ f1) + (~ f2)
proof end;

theorem :: DBLSEQ_3:16
for X, Y being non empty set
for f1 being V183() Function of [:X,Y:],ExtREAL
for f2 being V184() Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
proof end;

registration
cluster Function-like V32( omega , ExtREAL ) convergent_to_+infty -> convergent for Element of bool [:omega,ExtREAL:];
correctness
coherence
for b1 being ExtREAL_sequence st b1 is convergent_to_+infty holds
b1 is convergent ;
by MESFUNC5:def 11;
cluster Function-like V32( omega , ExtREAL ) convergent_to_-infty -> convergent for Element of bool [:omega,ExtREAL:];
correctness
coherence
for b1 being ExtREAL_sequence st b1 is convergent_to_-infty holds
b1 is convergent ;
by MESFUNC5:def 11;
cluster Function-like V32( omega , ExtREAL ) convergent_to_finite_number -> convergent for Element of bool [:omega,ExtREAL:];
correctness
coherence
for b1 being ExtREAL_sequence st b1 is convergent_to_finite_number holds
b1 is convergent ;
by MESFUNC5:def 11;
end;

registration
cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued convergent for Element of bool [:omega,ExtREAL:];
existence
ex b1 being ExtREAL_sequence st b1 is convergent
proof end;
cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V183() convergent for Element of bool [:omega,ExtREAL:];
existence
ex b1 being V183() ExtREAL_sequence st b1 is convergent
proof end;
cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V184() convergent for Element of bool [:omega,ExtREAL:];
existence
ex b1 being V184() ExtREAL_sequence st b1 is convergent
proof end;
end;

Lm6: for seq being convergent ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & - seq is convergent & lim (- seq) = - (lim seq) )
proof end;

theorem Th17: :: DBLSEQ_3:17
for seq being convergent ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( - seq is convergent_to_finite_number implies seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( - seq is convergent_to_-infty implies seq is convergent_to_+infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )
proof end;

theorem Th18: :: DBLSEQ_3:18
for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_+infty holds
( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
proof end;

theorem Th19: :: DBLSEQ_3:19
for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number holds
( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
proof end;

theorem :: DBLSEQ_3:20
for seq1, seq2 being V184() ExtREAL_sequence st seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number holds
( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
proof end;

theorem Th21: :: DBLSEQ_3:21
for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_-infty & seq2 is convergent_to_-infty holds
( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
proof end;

theorem Th22: :: DBLSEQ_3:22
for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number holds
( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
proof end;

theorem Th23: :: DBLSEQ_3:23
for seq1, seq2 being V183() ExtREAL_sequence st seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number holds
( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) )
proof end;

theorem Th24: :: DBLSEQ_3:24
for seq1, seq2 being V184() ExtREAL_sequence holds
( ( seq1 is convergent_to_+infty & seq2 is convergent_to_+infty implies ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) ) & ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) ) )
proof end;

theorem :: DBLSEQ_3:25
for seq1 being V183() ExtREAL_sequence
for seq2 being V184() ExtREAL_sequence holds
( ( seq1 is convergent_to_+infty & seq2 is convergent_to_-infty implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) ) )
proof end;

theorem :: DBLSEQ_3:26
for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_finite_number holds
( seq2 is convergent_to_finite_number & lim seq1 = lim seq2 )
proof end;

theorem :: DBLSEQ_3:27
for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_+infty holds
( seq2 is convergent_to_+infty & lim seq2 = +infty )
proof end;

theorem :: DBLSEQ_3:28
for seq1, seq2 being ExtREAL_sequence st seq2 is subsequence of seq1 & seq1 is convergent_to_-infty holds
( seq2 is convergent_to_-infty & lim seq2 = -infty )
proof end;

theorem :: DBLSEQ_3:29
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds
cod1_major_iterated_lim Rseq = lim (lim_in_cod1 Rseq)
proof end;

theorem :: DBLSEQ_3:30
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds
cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq)
proof end;

definition
let Eseq be Function of [:NAT,NAT:],ExtREAL;
attr Eseq is P-convergent_to_finite_number means :: DBLSEQ_3:def 1
 ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Eseq . (n,m)) - p).| < e;
attr Eseq is P-convergent_to_+infty means :: DBLSEQ_3:def 2
 for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= Eseq . (n,m);
attr Eseq is P-convergent_to_-infty means :: DBLSEQ_3:def 3
 for g being Real st g < 0 holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
Eseq . (n,m) <= g;
end;

:: deftheorem defines P-convergent_to_finite_number DBLSEQ_3:def 1 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_finite_number iff ex p being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Eseq . (n,m)) - p).| < e );

:: deftheorem defines P-convergent_to_+infty DBLSEQ_3:def 2 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_+infty iff for g being Real st 0 < g holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
g <= Eseq . (n,m) );

:: deftheorem defines P-convergent_to_-infty DBLSEQ_3:def 3 :
for Eseq being Function of [:NAT,NAT:],ExtREAL holds
( Eseq is P-convergent_to_-infty iff for g being Real st g < 0 holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
Eseq . (n,m) <= g );

definition
let f be Function of [:NAT,NAT:],ExtREAL;
attr f is convergent_in_cod1_to_+infty means :: DBLSEQ_3:def 4
 for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_+infty ;
attr f is convergent_in_cod1_to_-infty means :: DBLSEQ_3:def 5
 for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_-infty ;
attr f is convergent_in_cod1_to_finite means :: DBLSEQ_3:def 6
 for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_finite_number ;
attr f is convergent_in_cod1 means :: DBLSEQ_3:def 7
 for m being Element of NAT holds ProjMap2 (f,m) is convergent ;
attr f is convergent_in_cod2_to_+infty means :: DBLSEQ_3:def 8
 for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_+infty ;
attr f is convergent_in_cod2_to_-infty means :: DBLSEQ_3:def 9
 for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_-infty ;
attr f is convergent_in_cod2_to_finite means :: DBLSEQ_3:def 10
 for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_finite_number ;
attr f is convergent_in_cod2 means :: DBLSEQ_3:def 11
 for m being Element of NAT holds ProjMap1 (f,m) is convergent ;
end;

:: deftheorem defines convergent_in_cod1_to_+infty DBLSEQ_3:def 4 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_+infty iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_+infty );

:: deftheorem defines convergent_in_cod1_to_-infty DBLSEQ_3:def 5 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_-infty iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_-infty );

:: deftheorem defines convergent_in_cod1_to_finite DBLSEQ_3:def 6 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1_to_finite iff for m being Element of NAT holds ProjMap2 (f,m) is convergent_to_finite_number );

:: deftheorem defines convergent_in_cod1 DBLSEQ_3:def 7 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (f,m) is convergent );

:: deftheorem defines convergent_in_cod2_to_+infty DBLSEQ_3:def 8 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_+infty iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_+infty );

:: deftheorem defines convergent_in_cod2_to_-infty DBLSEQ_3:def 9 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_-infty iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_-infty );

:: deftheorem defines convergent_in_cod2_to_finite DBLSEQ_3:def 10 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_finite iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_finite_number );

:: deftheorem defines convergent_in_cod2 DBLSEQ_3:def 11 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2 iff for m being Element of NAT holds ProjMap1 (f,m) is convergent );

theorem :: DBLSEQ_3:31
for f being Function of [:NAT,NAT:],ExtREAL holds
( ( ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite ) implies f is convergent_in_cod1 ) & ( ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) implies f is convergent_in_cod2 ) )
proof end;

theorem Th32: :: DBLSEQ_3:32
for X, Y, Z being non empty set
for F being Function of [:X,Y:],Z
for x being Element of X holds ProjMap1 (F,x) = ProjMap2 ((~ F),x)
proof end;

theorem Th33: :: DBLSEQ_3:33
for X, Y, Z being non empty set
for F being Function of [:X,Y:],Z
for y being Element of Y holds ProjMap2 (F,y) = ProjMap1 ((~ F),y)
proof end;

theorem Th34: :: DBLSEQ_3:34
for X, Y being non empty set
for F being Function of [:X,Y:],ExtREAL
for x being Element of X holds ProjMap1 ((- F),x) = - (ProjMap1 (F,x))
proof end;

theorem Th35: :: DBLSEQ_3:35
for X, Y being non empty set
for F being Function of [:X,Y:],ExtREAL
for y being Element of Y holds ProjMap2 ((- F),y) = - (ProjMap2 (F,y))
proof end;

theorem Th36: :: DBLSEQ_3:36
for f being Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1_to_+infty implies ~ f is convergent_in_cod2_to_+infty ) & ( ~ f is convergent_in_cod2_to_+infty implies f is convergent_in_cod1_to_+infty ) & ( f is convergent_in_cod2_to_+infty implies ~ f is convergent_in_cod1_to_+infty ) & ( ~ f is convergent_in_cod1_to_+infty implies f is convergent_in_cod2_to_+infty ) & ( f is convergent_in_cod1_to_-infty implies ~ f is convergent_in_cod2_to_-infty ) & ( ~ f is convergent_in_cod2_to_-infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod2_to_-infty implies ~ f is convergent_in_cod1_to_-infty ) & ( ~ f is convergent_in_cod1_to_-infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod1_to_finite implies ~ f is convergent_in_cod2_to_finite ) & ( ~ f is convergent_in_cod2_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_finite implies ~ f is convergent_in_cod1_to_finite ) & ( ~ f is convergent_in_cod1_to_finite implies f is convergent_in_cod2_to_finite ) )
proof end;

theorem :: DBLSEQ_3:37
for f being Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1_to_+infty implies - f is convergent_in_cod1_to_-infty ) & ( - f is convergent_in_cod1_to_-infty implies f is convergent_in_cod1_to_+infty ) & ( f is convergent_in_cod1_to_-infty implies - f is convergent_in_cod1_to_+infty ) & ( - f is convergent_in_cod1_to_+infty implies f is convergent_in_cod1_to_-infty ) & ( f is convergent_in_cod1_to_finite implies - f is convergent_in_cod1_to_finite ) & ( - f is convergent_in_cod1_to_finite implies f is convergent_in_cod1_to_finite ) & ( f is convergent_in_cod2_to_+infty implies - f is convergent_in_cod2_to_-infty ) & ( - f is convergent_in_cod2_to_-infty implies f is convergent_in_cod2_to_+infty ) & ( f is convergent_in_cod2_to_-infty implies - f is convergent_in_cod2_to_+infty ) & ( - f is convergent_in_cod2_to_+infty implies f is convergent_in_cod2_to_-infty ) & ( f is convergent_in_cod2_to_finite implies - f is convergent_in_cod2_to_finite ) & ( - f is convergent_in_cod2_to_finite implies f is convergent_in_cod2_to_finite ) )
proof end;

definition
let f be Function of [:NAT,NAT:],ExtREAL;
func lim_in_cod1 f -> ExtREAL_sequence means :D1DEF5: :: DBLSEQ_3:def 12
 for m being Element of NAT holds it . m = lim (ProjMap2 (f,m));
existence
ex b1 being ExtREAL_sequence st
for m being Element of NAT holds b1 . m = lim (ProjMap2 (f,m))
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for m being Element of NAT holds b1 . m = lim (ProjMap2 (f,m)) ) & ( for m being Element of NAT holds b2 . m = lim (ProjMap2 (f,m)) ) holds
b1 = b2
proof end;
func lim_in_cod2 f -> ExtREAL_sequence means :D1DEF6: :: DBLSEQ_3:def 13
 for n being Element of NAT holds it . n = lim (ProjMap1 (f,n));
existence
ex b1 being ExtREAL_sequence st
for n being Element of NAT holds b1 . n = lim (ProjMap1 (f,n))
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT holds b1 . n = lim (ProjMap1 (f,n)) ) & ( for n being Element of NAT holds b2 . n = lim (ProjMap1 (f,n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem D1DEF5 defines lim_in_cod1 DBLSEQ_3:def 12 :
for f being Function of [:NAT,NAT:],ExtREAL
for b2 being ExtREAL_sequence holds
( b2 = lim_in_cod1 f iff for m being Element of NAT holds b2 . m = lim (ProjMap2 (f,m)) );

:: deftheorem D1DEF6 defines lim_in_cod2 DBLSEQ_3:def 13 :
for f being Function of [:NAT,NAT:],ExtREAL
for b2 being ExtREAL_sequence holds
( b2 = lim_in_cod2 f iff for n being Element of NAT holds b2 . n = lim (ProjMap1 (f,n)) );

theorem Th38: :: DBLSEQ_3:38
for f being Function of [:NAT,NAT:],ExtREAL holds
( lim_in_cod1 f = lim_in_cod2 (~ f) & lim_in_cod2 f = lim_in_cod1 (~ f) )
proof end;

registration
let X, Y be non empty set ;
let F be V184() Function of [:X,Y:],ExtREAL;
let x be Element of X;
cluster ProjMap1 (F,x) -> V184() ;
correctness
coherence
ProjMap1 (F,x) is without+infty ;
proof end;
end;

registration
let X, Y be non empty set ;
let F be V184() Function of [:X,Y:],ExtREAL;
let y be Element of Y;
cluster ProjMap2 (F,y) -> V184() ;
correctness
coherence
ProjMap2 (F,y) is without+infty ;
proof end;
end;

registration
let X, Y be non empty set ;
let F be V183() Function of [:X,Y:],ExtREAL;
let x be Element of X;
cluster ProjMap1 (F,x) -> V183() ;
correctness
coherence
ProjMap1 (F,x) is without-infty ;
proof end;
end;

registration
let X, Y be non empty set ;
let F be V183() Function of [:X,Y:],ExtREAL;
let y be Element of Y;
cluster ProjMap2 (F,y) -> V183() ;
correctness
coherence
ProjMap2 (F,y) is without-infty ;
proof end;
end;

definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums_in_cod2 f -> Function of [:NAT,NAT:],ExtREAL means :DefCSM: :: DBLSEQ_3:def 14
 for n, m being Nat holds
( it . (n,0) = f . (n,0) & it . (n,(m + 1)) = (it . (n,m)) + (f . (n,(m + 1))) );
existence
ex b1 being Function of [:NAT,NAT:],ExtREAL st
for n, m being Nat holds
( b1 . (n,0) = f . (n,0) & b1 . (n,(m + 1)) = (b1 . (n,m)) + (f . (n,(m + 1))) )
proof end;
uniqueness
for b1, b2 being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds
( b1 . (n,0) = f . (n,0) & b1 . (n,(m + 1)) = (b1 . (n,m)) + (f . (n,(m + 1))) ) ) & ( for n, m being Nat holds
( b2 . (n,0) = f . (n,0) & b2 . (n,(m + 1)) = (b2 . (n,m)) + (f . (n,(m + 1))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefCSM defines Partial_Sums_in_cod2 DBLSEQ_3:def 14 :
for f, b2 being Function of [:NAT,NAT:],ExtREAL holds
( b2 = Partial_Sums_in_cod2 f iff for n, m being Nat holds
( b2 . (n,0) = f . (n,0) & b2 . (n,(m + 1)) = (b2 . (n,m)) + (f . (n,(m + 1))) ) );

definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums_in_cod1 f -> Function of [:NAT,NAT:],ExtREAL means :DefRSM: :: DBLSEQ_3:def 15
 for n, m being Nat holds
( it . (0,m) = f . (0,m) & it . ((n + 1),m) = (it . (n,m)) + (f . ((n + 1),m)) );
existence
ex b1 being Function of [:NAT,NAT:],ExtREAL st
for n, m being Nat holds
( b1 . (0,m) = f . (0,m) & b1 . ((n + 1),m) = (b1 . (n,m)) + (f . ((n + 1),m)) )
proof end;
uniqueness
for b1, b2 being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds
( b1 . (0,m) = f . (0,m) & b1 . ((n + 1),m) = (b1 . (n,m)) + (f . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( b2 . (0,m) = f . (0,m) & b2 . ((n + 1),m) = (b2 . (n,m)) + (f . ((n + 1),m)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefRSM defines Partial_Sums_in_cod1 DBLSEQ_3:def 15 :
for f, b2 being Function of [:NAT,NAT:],ExtREAL holds
( b2 = Partial_Sums_in_cod1 f iff for n, m being Nat holds
( b2 . (0,m) = f . (0,m) & b2 . ((n + 1),m) = (b2 . (n,m)) + (f . ((n + 1),m)) ) );

registration
let f be V183() Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> V183() ;
correctness
coherence
Partial_Sums_in_cod2 f is without-infty ;
proof end;
end;

registration
let f be V184() Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> V184() ;
correctness
coherence
Partial_Sums_in_cod2 f is without+infty ;
proof end;
end;

registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL;
correctness
coherence
for b1 being Function of [:NAT,NAT:],ExtREAL st b1 = Partial_Sums_in_cod2 f holds
b1 is nonnegative ;
proof end;
end;

registration
let f be nonpositive Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod2 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL;
correctness
coherence
for b1 being Function of [:NAT,NAT:],ExtREAL st b1 = Partial_Sums_in_cod2 f holds
b1 is nonpositive ;
proof end;
end;

registration
let f be V183() Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> V183() ;
correctness
coherence
Partial_Sums_in_cod1 f is without-infty ;
proof end;
end;

registration
let f be V184() Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> V184() ;
correctness
coherence
Partial_Sums_in_cod1 f is without+infty ;
proof end;
end;

registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> nonnegative for Function of [:NAT,NAT:],ExtREAL;
correctness
coherence
for b1 being Function of [:NAT,NAT:],ExtREAL st b1 = Partial_Sums_in_cod1 f holds
b1 is nonnegative ;
proof end;
end;

registration
let f be nonpositive Function of [:NAT,NAT:],ExtREAL;
cluster Partial_Sums_in_cod1 f -> nonpositive for Function of [:NAT,NAT:],ExtREAL;
correctness
coherence
for b1 being Function of [:NAT,NAT:],ExtREAL st b1 = Partial_Sums_in_cod1 f holds
b1 is nonpositive ;
proof end;
end;

definition
let f be Function of [:NAT,NAT:],ExtREAL;
func Partial_Sums f -> Function of [:NAT,NAT:],ExtREAL equals :: DBLSEQ_3:def 16
 Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);
correctness
coherence
Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f) is Function of [:NAT,NAT:],ExtREAL;
;
end;

:: deftheorem defines Partial_Sums DBLSEQ_3:def 16 :
for f being Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);

theorem Th39: :: DBLSEQ_3:39
for f being Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (Partial_Sums_in_cod1 f) . (n,m) = (Partial_Sums_in_cod2 (~ f)) . (m,n) & (Partial_Sums_in_cod2 f) . (n,m) = (Partial_Sums_in_cod1 (~ f)) . (m,n) )
proof end;

theorem Th40: :: DBLSEQ_3:40
for f being Function of [:NAT,NAT:],ExtREAL holds
( ~ (Partial_Sums_in_cod1 f) = Partial_Sums_in_cod2 (~ f) & ~ (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (~ f) )
proof end;

theorem :: DBLSEQ_3:41
for f being Function of [:NAT,NAT:],ExtREAL
for g being ext-real-valued Function
for n being Nat st ( for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ) holds
( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g )
proof end;

theorem Th42: :: DBLSEQ_3:42
for f being Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (- f) = - (Partial_Sums_in_cod2 f) & Partial_Sums_in_cod1 (- f) = - (Partial_Sums_in_cod1 f) )
proof end;

theorem Th43: :: DBLSEQ_3:43
for f being Function of [:NAT,NAT:],ExtREAL
for m, n being Element of NAT holds
( (Partial_Sums_in_cod1 f) . (m,n) = (Partial_Sums (ProjMap2 (f,n))) . m & (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n )
proof end;

theorem Th44: :: DBLSEQ_3:44
for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2) )
proof end;

theorem Th45: :: DBLSEQ_3:45
for f1, f2 being V184() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2) )
proof end;

theorem Th46: :: DBLSEQ_3:46
for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod2 (f1 - f2) = (Partial_Sums_in_cod2 f1) - (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 - f2) = (Partial_Sums_in_cod1 f1) - (Partial_Sums_in_cod1 f2) & Partial_Sums_in_cod2 (f2 - f1) = (Partial_Sums_in_cod2 f2) - (Partial_Sums_in_cod2 f1) & Partial_Sums_in_cod1 (f2 - f1) = (Partial_Sums_in_cod1 f2) - (Partial_Sums_in_cod1 f1) )
proof end;

theorem Th47: :: DBLSEQ_3:47
for f being V183() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
proof end;

theorem :: DBLSEQ_3:48
for f being V184() Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
proof end;

Lm7: for f being V183() Function of [:NAT,NAT:],ExtREAL
for m, n being Nat holds (Partial_Sums f) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n)
proof end;

Lm8: for f being V183() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)
proof end;

Lm9: for f being V184() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)
proof end;

theorem :: DBLSEQ_3:49
for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) holds
Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by Lm8, Lm9;

theorem :: DBLSEQ_3:50
for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)
proof end;

theorem :: DBLSEQ_3:51
for f1, f2 being V184() Function of [:NAT,NAT:],ExtREAL holds Partial_Sums (f1 + f2) = (Partial_Sums f1) + (Partial_Sums f2)
proof end;

theorem :: DBLSEQ_3:52
for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being V184() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums (f1 - f2) = (Partial_Sums f1) - (Partial_Sums f2) & Partial_Sums (f2 - f1) = (Partial_Sums f2) - (Partial_Sums f1) )
proof end;

theorem :: DBLSEQ_3:53
for f being Function of [:NAT,NAT:],ExtREAL
for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 f),k) = Partial_Sums (ProjMap2 (f,k)) & ProjMap1 ((Partial_Sums_in_cod2 f),k) = Partial_Sums (ProjMap1 (f,k)) )
proof end;

theorem Th54: :: DBLSEQ_3:54
for f being Function of [:NAT,NAT:],ExtREAL st ( not f is V183() or not f is V184() ) holds
( ProjMap1 ((Partial_Sums f),0) = ProjMap1 ((Partial_Sums_in_cod2 f),0) & ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) )
proof end;

theorem :: DBLSEQ_3:55
for C, D being non empty set
for F1, F2 being V183() Function of [:C,D:],ExtREAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
proof end;

theorem :: DBLSEQ_3:56
for C, D being non empty set
for F1, F2 being V183() Function of [:C,D:],ExtREAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
proof end;

theorem :: DBLSEQ_3:57
for C, D being non empty set
for F1, F2 being V184() Function of [:C,D:],ExtREAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
proof end;

theorem :: DBLSEQ_3:58
for C, D being non empty set
for F1, F2 being V184() Function of [:C,D:],ExtREAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
proof end;

theorem :: DBLSEQ_3:59
for C, D being non empty set
for F1 being V183() Function of [:C,D:],ExtREAL
for F2 being V184() Function of [:C,D:],ExtREAL
for c being Element of C holds
( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )
proof end;

theorem :: DBLSEQ_3:60
for C, D being non empty set
for F1 being V183() Function of [:C,D:],ExtREAL
for F2 being V184() Function of [:C,D:],ExtREAL
for d being Element of D holds
( ProjMap2 ((F1 - F2),d) = (ProjMap2 (F1,d)) - (ProjMap2 (F2,d)) & ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d)) )
proof end;

theorem :: DBLSEQ_3:61
for seq being nonnegative ExtREAL_sequence st not Partial_Sums seq is convergent_to_+infty holds
for n being Nat holds seq . n is Real
proof end;

theorem Th62: :: DBLSEQ_3:62
for seq being nonnegative ExtREAL_sequence holds
( not seq is non-decreasing or seq is convergent_to_+infty or seq is convergent_to_finite_number )
proof end;

Lm10: for f being Function of [:NAT,NAT:],ExtREAL
for n being Element of NAT st f is nonnegative holds
( ProjMap1 (f,n) is nonnegative & ProjMap2 (f,n) is nonnegative )
proof end;

registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let n be Element of NAT ;
cluster ProjMap1 (f,n) -> nonnegative ;
correctness
coherence
ProjMap1 (f,n) is nonnegative ;
by Lm10;
cluster ProjMap2 (f,n) -> nonnegative ;
correctness
coherence
ProjMap2 (f,n) is nonnegative ;
by Lm10;
end;

theorem Th63: :: DBLSEQ_3:63
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing
proof end;

theorem Th64: :: DBLSEQ_3:64
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod1 f),n) is non-decreasing
proof end;

registration
let f be nonnegative Function of [:NAT,NAT:],ExtREAL;
let m be Element of NAT ;
cluster ProjMap1 ((Partial_Sums_in_cod2 f),m) -> non-decreasing ;
correctness
coherence
ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing ;
by Th63;
cluster ProjMap2 ((Partial_Sums_in_cod1 f),m) -> non-decreasing ;
correctness
coherence
ProjMap2 ((Partial_Sums_in_cod1 f),m) is non-decreasing ;
by Th64;
end;

theorem Th65: :: DBLSEQ_3:65
for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative ) & ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative ) )
proof end;

theorem :: DBLSEQ_3:66
for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod1 f is convergent_in_cod1 & Partial_Sums_in_cod2 f is convergent_in_cod2 ) by RINFSUP2:37;

theorem :: DBLSEQ_3:67
for f being 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
proof end;

theorem :: DBLSEQ_3:68
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st not ProjMap1 ((Partial_Sums_in_cod2 f),m) is convergent_to_+infty holds
for n being Nat holds f . (m,n) is Real
proof end;

theorem :: DBLSEQ_3:69
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat st ( for i being Nat st i <= n holds
f . (i,m) is Real ) holds
(Partial_Sums_in_cod1 f) . (n,m) < +infty
proof end;

theorem :: DBLSEQ_3:70
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat st ( for i being Nat st i <= m holds
f . (n,i) is Real ) holds
(Partial_Sums_in_cod2 f) . (n,m) < +infty
proof end;

theorem :: DBLSEQ_3:71
for f being V183() Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_-infty holds
ex m being Element of NAT st ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty
proof end;

theorem Th72: :: DBLSEQ_3:72
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( ( for k being Element of NAT st k <= m holds
not ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap1 ((Partial_Sums_in_cod2 f),k)) < +infty )
proof end;

theorem :: DBLSEQ_3:73
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( ( for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )
proof end;

theorem Th74: :: DBLSEQ_3:74
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) )
proof end;

theorem :: DBLSEQ_3:75
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) )
proof end;

theorem Th76: :: DBLSEQ_3:76
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds
( (Partial_Sums_in_cod1 f) . (n,m) >= f . (n,m) & (Partial_Sums_in_cod2 f) . (n,m) >= f . (n,m) )
proof end;

theorem Th77: :: DBLSEQ_3:77
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) holds
( ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m) is convergent_to_+infty & lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty )
proof end;

theorem :: DBLSEQ_3:78
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Element of NAT st ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) holds
( ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) is convergent_to_+infty & lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) = +infty )
proof end;

theorem Th79: :: DBLSEQ_3:79
for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums f is convergent_in_cod1_to_finite iff Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite )
proof end;

theorem Th80: :: DBLSEQ_3:80
for f being nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_finite holds
for m being Element of NAT holds (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m))
proof end;

theorem :: DBLSEQ_3:81
for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums f is convergent_in_cod2_to_finite iff Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite )
proof end;

theorem :: DBLSEQ_3:82
for f being nonnegative Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod2_to_finite holds
for m being Element of NAT holds (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m))
proof end;

:: Fatou's Lemma for Double Sequence
theorem Th83: :: DBLSEQ_3:83
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))
proof end;

theorem :: DBLSEQ_3:84
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds seq . m = lim_inf (ProjMap1 (f,m)) ) holds
Sum seq <= lim_inf (lim_in_cod1 (Partial_Sums_in_cod1 f))
proof end;

theorem Th85: :: DBLSEQ_3:85
for f being Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence
for n, m being Nat holds
( ( ( for i, j being Nat holds f . (i,j) <= seq . i ) implies (Partial_Sums_in_cod1 f) . (n,m) <= (Partial_Sums seq) . n ) & ( ( for i, j being Nat holds f . (i,j) <= seq . j ) implies (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m ) )
proof end;

theorem Th86: :: DBLSEQ_3:86
for seq being ExtREAL_sequence
for r being R_eal st ( for n being Nat holds seq . n <= r ) holds
lim_sup seq <= r
proof end;

theorem Th87: :: DBLSEQ_3:87
for seq being ExtREAL_sequence
for r being R_eal st ( for n being Nat holds r <= seq . n ) holds
r <= lim_inf seq
proof end;

theorem :: DBLSEQ_3:88
for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) ) )
proof end;

theorem Th89: :: DBLSEQ_3:89
for f being Function of [:NAT,NAT:],ExtREAL
for i, j, k being Nat st ( for m being Element of NAT holds ProjMap2 (f,m) is non-decreasing ) & i <= j holds
(Partial_Sums_in_cod2 f) . (i,k) <= (Partial_Sums_in_cod2 f) . (j,k)
proof end;

theorem :: DBLSEQ_3:90
for f being Function of [:NAT,NAT:],ExtREAL
for i, j, k being Nat st ( for n being Element of NAT holds ProjMap1 (f,n) is non-decreasing ) & i <= j holds
(Partial_Sums_in_cod1 f) . (k,i) <= (Partial_Sums_in_cod1 f) . (k,j)
proof end;

:: Moonotone Convergence Theorem for Double Sequence
theorem Th91: :: DBLSEQ_3:91
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds
( ProjMap2 (f,m) is non-decreasing & seq . m = lim (ProjMap2 (f,m)) ) ) holds
( lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) )
proof end;

theorem :: DBLSEQ_3:92
for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds
( ProjMap1 (f,m) is non-decreasing & seq . m = lim (ProjMap1 (f,m)) ) ) holds
( lim_in_cod1 (Partial_Sums_in_cod1 f) is non-decreasing & Sum seq = lim (lim_in_cod1 (Partial_Sums_in_cod1 f)) )
proof end;

theorem Th93: :: DBLSEQ_3:93
for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent_to_+infty holds
( not f is P-convergent_to_-infty & not f is P-convergent_to_finite_number )
proof end;

theorem Th94: :: DBLSEQ_3:94
for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent_to_-infty holds
( not f is P-convergent_to_+infty & not f is P-convergent_to_finite_number )
proof end;

definition
let f be Function of [:NAT,NAT:],ExtREAL;
attr f is P-convergent means :: DBLSEQ_3:def 17
( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty );
end;

:: deftheorem defines P-convergent DBLSEQ_3:def 17 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is P-convergent iff ( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty ) );

definition
let f be Function of [:NAT,NAT:],ExtREAL;
assume A1: f is P-convergent ;
func P-lim f -> ExtReal means :Def5: :: DBLSEQ_3:def 18
( ex p being Real st
( it = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - it).| < e ) & f is P-convergent_to_finite_number ) or ( it = +infty & f is P-convergent_to_+infty ) or ( it = -infty & f is P-convergent_to_-infty ) );
existence
ex b1 being ExtReal st
( ex p being Real st
( b1 = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b1).| < e ) & f is P-convergent_to_finite_number ) or ( b1 = +infty & f is P-convergent_to_+infty ) or ( b1 = -infty & f is P-convergent_to_-infty ) )
proof end;
uniqueness
for b1, b2 being ExtReal st ( ex p being Real st
( b1 = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b1).| < e ) & f is P-convergent_to_finite_number ) or ( b1 = +infty & f is P-convergent_to_+infty ) or ( b1 = -infty & f is P-convergent_to_-infty ) ) & ( ex p being Real st
( b2 = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b2).| < e ) & f is P-convergent_to_finite_number ) or ( b2 = +infty & f is P-convergent_to_+infty ) or ( b2 = -infty & f is P-convergent_to_-infty ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines P-lim DBLSEQ_3:def 18 :
for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent holds
for b2 being ExtReal holds
( b2 = P-lim f iff ( ex p being Real st
( b2 = p & ( for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((f . (n,m)) - b2).| < e ) & f is P-convergent_to_finite_number ) or ( b2 = +infty & f is P-convergent_to_+infty ) or ( b2 = -infty & f is P-convergent_to_-infty ) ) );

theorem :: DBLSEQ_3:95
for f being Function of [:NAT,NAT:],ExtREAL
for r being Real st ( for n, m being Nat holds f . (n,m) = r ) holds
( f is P-convergent_to_finite_number & P-lim f = r )
proof end;

theorem Th96: :: DBLSEQ_3:96
for f being Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f . (n1,m1) <= f . (n2,m2) ) holds
( f is P-convergent & P-lim f = sup (rng f) )
proof end;

theorem :: DBLSEQ_3:97
for f1, f2 being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds f1 . (n,m) <= f2 . (n,m) ) holds
sup (rng f1) <= sup (rng f2)
proof end;

theorem :: DBLSEQ_3:98
for f being Function of [:NAT,NAT:],ExtREAL
for n, m being Nat holds f . (n,m) <= sup (rng f)
proof end;

theorem :: DBLSEQ_3:99
for f being Function of [:NAT,NAT:],ExtREAL
for K being R_eal st ( for n, m being Nat holds f . (n,m) <= K ) holds
sup (rng f) <= K
proof end;

theorem :: DBLSEQ_3:100
for f being Function of [:NAT,NAT:],ExtREAL
for K being R_eal st K <> +infty & ( for n, m being Nat holds f . (n,m) <= K ) holds
sup (rng f) < +infty
proof end;

theorem Th101: :: DBLSEQ_3:101
for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( sup (rng f) <> +infty iff ex K being Real st
( 0 < K & ( for n, m being Nat holds f . (n,m) <= K ) ) )
proof end;

theorem Th102: :: DBLSEQ_3:102
for f being Function of [:NAT,NAT:],ExtREAL
for c being ExtReal st ( for n, m being Nat holds f . (n,m) = c ) holds
( f is P-convergent & P-lim f = c & P-lim f = sup (rng f) )
proof end;

Lm8: for f being V183() Function of [:NAT,NAT:],ExtREAL holds
( sup (rng f) in REAL or sup (rng f) = +infty )
proof end;

theorem :: DBLSEQ_3:103
for f being Function of [:NAT,NAT:],ExtREAL
for f1, f2 being V183() Function of [:NAT,NAT:],ExtREAL st ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & ( for n, m being Nat holds (f1 . (n,m)) + (f2 . (n,m)) = f . (n,m) ) holds
( f is P-convergent & P-lim f = sup (rng f) & P-lim f = (P-lim f1) + (P-lim f2) & sup (rng f) = (sup (rng f1)) + (sup (rng f2)) )
proof end;

theorem Th104: :: DBLSEQ_3:104
for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( sup (rng f2) = c * (sup (rng f1)) & f2 is V183() )
proof end;

theorem :: DBLSEQ_3:105
for f1 being V183() Function of [:NAT,NAT:],ExtREAL
for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is V183() & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )
proof end;