:: by Noboru Endou

::

:: Received July 1, 2015

:: Copyright (c) 2015-2018 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 ;

ex b_{1} being Function of X,REAL st

( b_{1} is nonnegative & b_{1} is nonpositive )

end;
cluster non empty V7() V10(X) V11( REAL ) Function-like total V32(X, REAL ) complex-valued ext-real-valued real-valued nonnegative nonpositive for Function of ,;

existence ex b

( b

proof end;

registration

let X be non empty set ;

ex b_{1} being Function of X,ExtREAL st

( b_{1} is V183() & b_{1} is V184() & b_{1} is nonnegative & b_{1} is nonpositive )

end;
cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued nonnegative nonpositive V183() V184() for Function of ,;

existence ex b

( b

proof 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 ;

correctness

coherence

for b_{1} being Function of X,ExtREAL st b_{1} is nonnegative holds

b_{1} is V183();

coherence

for b_{1} being Function of X,ExtREAL st b_{1} is nonpositive holds

b_{1} is V184();

not for b_{1} being V184() Function of X,ExtREAL holds b_{1} is V183()

end;
correctness

coherence

for b

b

proof end;

correctness coherence

for b

b

proof end;

cluster non empty V7() V10(X) V11( ExtREAL ) Function-like total V32(X, ExtREAL ) ext-real-valued V183() V184() for Function of ,;

existence not for b

proof 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;

end;
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;

registration

let X be non empty set ;

let f be V183() Function of X,ExtREAL;

correctness

coherence

- f is without+infty ;

end;
let f be V183() Function of X,ExtREAL;

correctness

coherence

- f is without+infty ;

proof end;

registration

let X be non empty set ;

let f be V184() Function of X,ExtREAL;

correctness

coherence

- f is without-infty ;

end;
let f be V184() Function of X,ExtREAL;

correctness

coherence

- f is without-infty ;

proof end;

registration

let X be non empty set ;

let f be nonnegative Function of X,ExtREAL;

correctness

coherence

- f is nonpositive ;

end;
let f be nonnegative Function of X,ExtREAL;

correctness

coherence

- f is nonpositive ;

proof end;

registration

let X be non empty set ;

let f be nonpositive Function of X,ExtREAL;

correctness

coherence

- f is nonnegative ;

end;
let f be nonpositive Function of X,ExtREAL;

correctness

coherence

- f is nonnegative ;

proof end;

registration

let A, B be non empty set ;

let f be V183() Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is without-infty ;

end;
let f be V183() Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is without-infty ;

proof end;

registration

let A, B be non empty set ;

let f be V184() Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is without+infty ;

end;
let f be V184() Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is without+infty ;

proof end;

registration

let A, B be non empty set ;

let f be nonnegative Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is nonnegative ;

end;
let f be nonnegative Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is nonnegative ;

proof end;

registration

let A, B be non empty set ;

let f be nonpositive Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is nonpositive ;

end;
let f be nonpositive Function of [:A,B:],ExtREAL;

correctness

coherence

~ f is nonpositive ;

proof end;

registration

let seq be nonnegative ExtREAL_sequence;

correctness

coherence

Partial_Sums seq is nonnegative ;

by MESFUNC9:16;

end;
correctness

coherence

Partial_Sums seq is nonnegative ;

by MESFUNC9:16;

registration

let seq be nonpositive ExtREAL_sequence;

correctness

coherence

Partial_Sums seq is nonpositive ;

end;
correctness

coherence

Partial_Sums seq is nonpositive ;

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

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;

end;
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;

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;

end;
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;

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;

end;
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;

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;

end;
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;

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) ) )

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 )

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 )

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 )

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

end;
let n, m be Nat;

:: original: .

redefine func f . (n,m) -> Element of ExtREAL ;

coherence

f . (n,m) is Element of ExtREAL

proof 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))

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))

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)) )

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)

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)

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) )

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

coherence

for b_{1} being ExtREAL_sequence st b_{1} is convergent_to_+infty holds

b_{1} is convergent ;

by MESFUNC5:def 11;

coherence

for b_{1} being ExtREAL_sequence st b_{1} is convergent_to_-infty holds

b_{1} is convergent ;

by MESFUNC5:def 11;

coherence

for b_{1} being ExtREAL_sequence st b_{1} is convergent_to_finite_number holds

b_{1} is convergent ;

by MESFUNC5:def 11;

end;

cluster Function-like V32( omega , ExtREAL ) convergent_to_+infty -> convergent for ExtREAL_sequence;

correctness coherence

for b

b

by MESFUNC5:def 11;

cluster Function-like V32( omega , ExtREAL ) convergent_to_-infty -> convergent for ExtREAL_sequence;

correctness coherence

for b

b

by MESFUNC5:def 11;

cluster Function-like V32( omega , ExtREAL ) convergent_to_finite_number -> convergent for ExtREAL_sequence;

correctness coherence

for b

b

by MESFUNC5:def 11;

registration

ex b_{1} being ExtREAL_sequence st b_{1} is convergent

ex b_{1} being V183() ExtREAL_sequence st b_{1} is convergent

ex b_{1} being V184() ExtREAL_sequence st b_{1} is convergent
end;

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued convergent for ExtREAL_sequence;

existence ex b

proof end;

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V183() convergent for ExtREAL_sequence;

existence ex b

proof end;

cluster non empty V7() V10( omega ) V11( ExtREAL ) Function-like total V32( omega , ExtREAL ) ext-real-valued V184() convergent for ExtREAL_sequence;

existence ex b

proof 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) )

( ( 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 )

( 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 )

( 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 )

( 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 )

( 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 )

( 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) )

( 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) ) ) )

( ( 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) ) ) )

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 )

( 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 )

( 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 )

( 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)

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)

cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq)

proof end;

definition

let Eseq be Function of [:NAT,NAT:],ExtREAL;

end;
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;

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_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 );

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) );

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 );

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;

end;
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 ;

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 ;

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 ;

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 ;

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 ;

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 ;

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 ;

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 ;

for m being Element of NAT holds ProjMap1 (f,m) is convergent ;

:: 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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 ) )

( ( ( 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)

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)

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))

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))

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 ) )

( ( 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 ) )

( ( 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;

ex b_{1} being ExtREAL_sequence st

for m being Element of NAT holds b_{1} . m = lim (ProjMap2 (f,m))

for b_{1}, b_{2} being ExtREAL_sequence st ( for m being Element of NAT holds b_{1} . m = lim (ProjMap2 (f,m)) ) & ( for m being Element of NAT holds b_{2} . m = lim (ProjMap2 (f,m)) ) holds

b_{1} = b_{2}

ex b_{1} being ExtREAL_sequence st

for n being Element of NAT holds b_{1} . n = lim (ProjMap1 (f,n))

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Element of NAT holds b_{1} . n = lim (ProjMap1 (f,n)) ) & ( for n being Element of NAT holds b_{2} . n = lim (ProjMap1 (f,n)) ) holds

b_{1} = b_{2}

end;
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 for m being Element of NAT holds it . m = lim (ProjMap2 (f,m));

ex b

for m being Element of NAT holds b

proof end;

uniqueness for b

b

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 for n being Element of NAT holds it . n = lim (ProjMap1 (f,n));

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem D1DEF5 defines lim_in_cod1 DBLSEQ_3:def 12 :

for f being Function of [:NAT,NAT:],ExtREAL

for b_{2} being ExtREAL_sequence holds

( b_{2} = lim_in_cod1 f iff for m being Element of NAT holds b_{2} . m = lim (ProjMap2 (f,m)) );

for f being Function of [:NAT,NAT:],ExtREAL

for b

( b

:: deftheorem D1DEF6 defines lim_in_cod2 DBLSEQ_3:def 13 :

for f being Function of [:NAT,NAT:],ExtREAL

for b_{2} being ExtREAL_sequence holds

( b_{2} = lim_in_cod2 f iff for n being Element of NAT holds b_{2} . n = lim (ProjMap1 (f,n)) );

for f being Function of [:NAT,NAT:],ExtREAL

for b

( b

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) )

( 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;

correctness

coherence

ProjMap1 (F,x) is without+infty ;

end;
let F be V184() Function of [:X,Y:],ExtREAL;

let x be Element of X;

correctness

coherence

ProjMap1 (F,x) is without+infty ;

proof end;

registration

let X, Y be non empty set ;

let F be V184() Function of [:X,Y:],ExtREAL;

let y be Element of Y;

correctness

coherence

ProjMap2 (F,y) is without+infty ;

end;
let F be V184() Function of [:X,Y:],ExtREAL;

let y be Element of Y;

correctness

coherence

ProjMap2 (F,y) is without+infty ;

proof end;

registration

let X, Y be non empty set ;

let F be V183() Function of [:X,Y:],ExtREAL;

let x be Element of X;

correctness

coherence

ProjMap1 (F,x) is without-infty ;

end;
let F be V183() Function of [:X,Y:],ExtREAL;

let x be Element of X;

correctness

coherence

ProjMap1 (F,x) is without-infty ;

proof end;

registration

let X, Y be non empty set ;

let F be V183() Function of [:X,Y:],ExtREAL;

let y be Element of Y;

correctness

coherence

ProjMap2 (F,y) is without-infty ;

end;
let F be V183() Function of [:X,Y:],ExtREAL;

let y be Element of Y;

correctness

coherence

ProjMap2 (F,y) is without-infty ;

proof end;

definition

let f be Function of [:NAT,NAT:],ExtREAL;

ex b_{1} being Function of [:NAT,NAT:],ExtREAL st

for n, m being Nat holds

( b_{1} . (n,0) = f . (n,0) & b_{1} . (n,(m + 1)) = (b_{1} . (n,m)) + (f . (n,(m + 1))) )

for b_{1}, b_{2} being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds

( b_{1} . (n,0) = f . (n,0) & b_{1} . (n,(m + 1)) = (b_{1} . (n,m)) + (f . (n,(m + 1))) ) ) & ( for n, m being Nat holds

( b_{2} . (n,0) = f . (n,0) & b_{2} . (n,(m + 1)) = (b_{2} . (n,m)) + (f . (n,(m + 1))) ) ) holds

b_{1} = b_{2}

end;
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 for n, m being Nat holds

( it . (n,0) = f . (n,0) & it . (n,(m + 1)) = (it . (n,m)) + (f . (n,(m + 1))) );

ex b

for n, m being Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem DefCSM defines Partial_Sums_in_cod2 DBLSEQ_3:def 14 :

for f, b_{2} being Function of [:NAT,NAT:],ExtREAL holds

( b_{2} = Partial_Sums_in_cod2 f iff for n, m being Nat holds

( b_{2} . (n,0) = f . (n,0) & b_{2} . (n,(m + 1)) = (b_{2} . (n,m)) + (f . (n,(m + 1))) ) );

for f, b

( b

( b

definition

let f be Function of [:NAT,NAT:],ExtREAL;

ex b_{1} being Function of [:NAT,NAT:],ExtREAL st

for n, m being Nat holds

( b_{1} . (0,m) = f . (0,m) & b_{1} . ((n + 1),m) = (b_{1} . (n,m)) + (f . ((n + 1),m)) )

for b_{1}, b_{2} being Function of [:NAT,NAT:],ExtREAL st ( for n, m being Nat holds

( b_{1} . (0,m) = f . (0,m) & b_{1} . ((n + 1),m) = (b_{1} . (n,m)) + (f . ((n + 1),m)) ) ) & ( for n, m being Nat holds

( b_{2} . (0,m) = f . (0,m) & b_{2} . ((n + 1),m) = (b_{2} . (n,m)) + (f . ((n + 1),m)) ) ) holds

b_{1} = b_{2}

end;
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 for n, m being Nat holds

( it . (0,m) = f . (0,m) & it . ((n + 1),m) = (it . (n,m)) + (f . ((n + 1),m)) );

ex b

for n, m being Nat holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem DefRSM defines Partial_Sums_in_cod1 DBLSEQ_3:def 15 :

for f, b_{2} being Function of [:NAT,NAT:],ExtREAL holds

( b_{2} = Partial_Sums_in_cod1 f iff for n, m being Nat holds

( b_{2} . (0,m) = f . (0,m) & b_{2} . ((n + 1),m) = (b_{2} . (n,m)) + (f . ((n + 1),m)) ) );

for f, b

( b

( b

registration

let f be V183() Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

Partial_Sums_in_cod2 f is without-infty ;

end;
correctness

coherence

Partial_Sums_in_cod2 f is without-infty ;

proof end;

registration

let f be V184() Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

Partial_Sums_in_cod2 f is without+infty ;

end;
correctness

coherence

Partial_Sums_in_cod2 f is without+infty ;

proof end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

for b_{1} being Function of [:NAT,NAT:],ExtREAL st b_{1} = Partial_Sums_in_cod2 f holds

b_{1} is nonnegative ;

end;
correctness

coherence

for b

b

proof end;

registration

let f be nonpositive Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

for b_{1} being Function of [:NAT,NAT:],ExtREAL st b_{1} = Partial_Sums_in_cod2 f holds

b_{1} is nonpositive ;

end;
correctness

coherence

for b

b

proof end;

registration

let f be V183() Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

Partial_Sums_in_cod1 f is without-infty ;

end;
correctness

coherence

Partial_Sums_in_cod1 f is without-infty ;

proof end;

registration

let f be V184() Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

Partial_Sums_in_cod1 f is without+infty ;

end;
correctness

coherence

Partial_Sums_in_cod1 f is without+infty ;

proof end;

registration

let f be nonnegative Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

for b_{1} being Function of [:NAT,NAT:],ExtREAL st b_{1} = Partial_Sums_in_cod1 f holds

b_{1} is nonnegative ;

end;
correctness

coherence

for b

b

proof end;

registration

let f be nonpositive Function of [:NAT,NAT:],ExtREAL;

correctness

coherence

for b_{1} being Function of [:NAT,NAT:],ExtREAL st b_{1} = Partial_Sums_in_cod1 f holds

b_{1} is nonpositive ;

end;
correctness

coherence

for b

b

proof end;

definition

let f be Function of [:NAT,NAT:],ExtREAL;

coherence

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f) is Function of [:NAT,NAT:],ExtREAL;

;

end;
func Partial_Sums f -> Function of [:NAT,NAT:],ExtREAL equals :: DBLSEQ_3:def 16

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);

correctness Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f);

coherence

Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f) is Function of [:NAT,NAT:],ExtREAL;

;

:: 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);

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) )

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) )

( ~ (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 )

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) )

( 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 )

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) )

( 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) )

( 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) )

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)) )

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)) )

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;

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) )

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)) )

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) )

( 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))

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))

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))

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))

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)) )

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)) )

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

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 )

( 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 ;

correctness

coherence

ProjMap1 (f,n) is nonnegative ;

by Lm10;

correctness

coherence

ProjMap2 (f,n) is nonnegative ;

by Lm10;

end;
let n be Element of NAT ;

correctness

coherence

ProjMap1 (f,n) is nonnegative ;

by Lm10;

correctness

coherence

ProjMap2 (f,n) is nonnegative ;

by Lm10;

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

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

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 ;

correctness

coherence

ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing ;

by Th63;

correctness

coherence

ProjMap2 ((Partial_Sums_in_cod1 f),m) is non-decreasing ;

by Th64;

end;
let m be Element of NAT ;

correctness

coherence

ProjMap1 ((Partial_Sums_in_cod2 f),m) is non-decreasing ;

by Th63;

correctness

coherence

ProjMap2 ((Partial_Sums_in_cod1 f),m) is non-decreasing ;

by Th64;

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 ) )

( ( 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;

( 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

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

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

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

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

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 )

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 )

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 ) )

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 ) )

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) )

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 )

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 )

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 )

( 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))

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 )

( 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))

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))

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))

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 ) )

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

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

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) ) )

( ( 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)

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)

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)) )

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)) )

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 )

( 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 )

( 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;

end;
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 );

( f is P-convergent_to_finite_number or f is P-convergent_to_+infty or f is P-convergent_to_-infty );

:: 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 ) );

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 ;

ex b_{1} being ExtReal st

( ex p being Real st

( b_{1} = 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)) - b_{1}).| < e ) & f is P-convergent_to_finite_number ) or ( b_{1} = +infty & f is P-convergent_to_+infty ) or ( b_{1} = -infty & f is P-convergent_to_-infty ) )

for b_{1}, b_{2} being ExtReal st ( ex p being Real st

( b_{1} = 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)) - b_{1}).| < e ) & f is P-convergent_to_finite_number ) or ( b_{1} = +infty & f is P-convergent_to_+infty ) or ( b_{1} = -infty & f is P-convergent_to_-infty ) ) & ( ex p being Real st

( b_{2} = 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)) - b_{2}).| < e ) & f is P-convergent_to_finite_number ) or ( b_{2} = +infty & f is P-convergent_to_+infty ) or ( b_{2} = -infty & f is P-convergent_to_-infty ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

( ex p being Real st

( b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((f . (n,m)) - b

proof end;

uniqueness for b

( b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((f . (n,m)) - b

( b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((f . (n,m)) - b

b

proof 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 b_{2} being ExtReal holds

( b_{2} = P-lim f iff ( ex p being Real st

( b_{2} = 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)) - b_{2}).| < e ) & f is P-convergent_to_finite_number ) or ( b_{2} = +infty & f is P-convergent_to_+infty ) or ( b_{2} = -infty & f is P-convergent_to_-infty ) ) );

for f being Function of [:NAT,NAT:],ExtREAL st f is P-convergent holds

for b

( b

( b

ex N being Nat st

for n, m being Nat st n >= N & m >= N holds

|.((f . (n,m)) - b

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 )

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) )

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)

sup (rng f1) <= sup (rng f2)

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

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

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 ) ) )

( 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) )

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)) )

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() )

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) )

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;