:: Double Series and Sums
:: by Noboru Endou
::
:: Received March 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


definition
let f be Function of [:NAT,NAT:],REAL;
redefine attr f is nonnegative-yielding means :: DBLSEQ_2:def 1
 for i, j being Nat holds f . (i,j) >= 0 ;
compatibility
( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 )
proof end;
end;

:: deftheorem defines nonnegative-yielding DBLSEQ_2:def 1 :
for f being Function of [:NAT,NAT:],REAL holds
( f is nonnegative-yielding iff for i, j being Nat holds f . (i,j) >= 0 );

theorem :: DBLSEQ_2:1
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing holds
( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is V115() ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is V115() ) )
proof end;

theorem :: DBLSEQ_2:2
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is convergent_in_cod1 holds
lim_in_cod1 Rseq is V115()
proof end;

theorem :: DBLSEQ_2:3
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is convergent_in_cod2 holds
lim_in_cod2 Rseq is V115()
proof end;

theorem :: DBLSEQ_2:4
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is non-decreasing & Rseq is P-convergent holds
for n, m being Nat holds Rseq . (n,m) <= P-lim Rseq
proof end;

theorem lmADD: :: DBLSEQ_2:5
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds
( dom (Rseq1 + Rseq2) = [:NAT,NAT:] & dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for n, m being Nat holds (Rseq1 + Rseq2) . (n,m) = (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for n, m being Nat holds (Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )
proof end;

theorem :: DBLSEQ_2:6
for C, D, E being non empty set
for f being Function of [:C,D:],E ex g being Function of [:D,C:],E st
for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d)
proof end;

theorem :: DBLSEQ_2:7
for C, D, E being set
for f being Function of [:C,D:],E holds f = ~ (~ f) by FUNCT_4:53;

scheme :: DBLSEQ_2:sch 1
RecEx2D1{ F1() -> non empty set , F2() -> non empty set , F3() -> Function of F1(),F2(), F4( set , set , Nat) -> Element of F2() } :
ex g being Function of [:F1(),NAT:],F2() st
for a being Element of F1() holds
( g . (a,0) = F3() . a & ( for n being Nat holds g . (a,(n + 1)) = F4((g . (a,n)),a,n) ) )
proof end;

scheme :: DBLSEQ_2:sch 2
RecEx2D1R{ F1() -> non empty set , F2() -> Function of F1(),REAL, F3( set , set , Nat) -> real number } :
ex g being Function of [:F1(),NAT:],REAL st
for a being Element of F1() holds
( g . (a,0) = F2() . a & ( for n being natural number holds g . (a,(n + 1)) = F3((g . (a,n)),a,n) ) )
proof end;

scheme :: DBLSEQ_2:sch 3
RecEx2D2{ F1() -> non empty set , F2() -> non empty set , F3() -> Function of F1(),F2(), F4( set , set , Nat) -> Element of F2() } :
ex g being Function of [:NAT,F1():],F2() st
for a being Element of F1() holds
( g . (0,a) = F3() . a & ( for n being Nat holds g . ((n + 1),a) = F4((g . (n,a)),a,n) ) )
proof end;

scheme :: DBLSEQ_2:sch 4
RecEx2D2R{ F1() -> non empty set , F2() -> Function of F1(),REAL, F3( set , set , Nat) -> real number } :
ex g being Function of [:NAT,F1():],REAL st
for a being Element of F1() holds
( g . (0,a) = F2() . a & ( for n being Nat holds g . ((n + 1),a) = F3((g . (n,a)),a,n) ) )
proof end;

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

:: deftheorem DefCS defines Partial_Sums_in_cod2 DBLSEQ_2:def 2 :
for Rseq, b2 being Function of [:NAT,NAT:],REAL holds
( b2 = Partial_Sums_in_cod2 Rseq iff for n, m being Nat holds
( b2 . (n,0) = Rseq . (n,0) & b2 . (n,(m + 1)) = (b2 . (n,m)) + (Rseq . (n,(m + 1))) ) );

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

:: deftheorem DefRS defines Partial_Sums_in_cod1 DBLSEQ_2:def 3 :
for Rseq, b2 being Function of [:NAT,NAT:],REAL holds
( b2 = Partial_Sums_in_cod1 Rseq iff for n, m being Nat holds
( b2 . (0,m) = Rseq . (0,m) & b2 . ((n + 1),m) = (b2 . (n,m)) + (Rseq . ((n + 1),m)) ) );

theorem thADD: :: DBLSEQ_2:8
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds
( Partial_Sums_in_cod2 (Rseq1 + Rseq2) = (Partial_Sums_in_cod2 Rseq1) + (Partial_Sums_in_cod2 Rseq2) & Partial_Sums_in_cod1 (Rseq1 + Rseq2) = (Partial_Sums_in_cod1 Rseq1) + (Partial_Sums_in_cod1 Rseq2) )
proof end;

theorem Tr2: :: DBLSEQ_2:9
for Rseq being Function of [:NAT,NAT:],REAL
for n, m being Nat holds
( (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) & (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) )
proof end;

theorem :: DBLSEQ_2:10
for Rseq being Function of [:NAT,NAT:],REAL holds
( Partial_Sums_in_cod2 Rseq = ~ (Partial_Sums_in_cod1 (~ Rseq)) & Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) & ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )
proof end;

definition
let Rseq be Function of [:NAT,NAT:],REAL;
func Partial_Sums Rseq -> Function of [:NAT,NAT:],REAL equals :: DBLSEQ_2:def 4
 Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);
correctness
coherence
Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq) is Function of [:NAT,NAT:],REAL;
;
end;

:: deftheorem defines Partial_Sums DBLSEQ_2:def 4 :
for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq);

theorem ThRS: :: DBLSEQ_2:11
for Rseq being Function of [:NAT,NAT:],REAL
for n, m being Nat holds
( (Partial_Sums Rseq) . ((n + 1),m) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),m)) + ((Partial_Sums Rseq) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m)) )
proof end;

th103: for Rseq being Function of [:NAT,NAT:],REAL
for m, n being Nat holds (Partial_Sums Rseq) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n)
proof end;

theorem th103a: :: DBLSEQ_2:12
for Rseq being Function of [:NAT,NAT:],REAL holds Partial_Sums Rseq = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)
proof end;

theorem thRS2: :: DBLSEQ_2:13
for Rseq being Function of [:NAT,NAT:],REAL
for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums Rseq) . ((n + 1),(m + 1))) - ((Partial_Sums Rseq) . (n,(m + 1)))) - ((Partial_Sums Rseq) . ((n + 1),m))) + ((Partial_Sums Rseq) . (n,m))
proof end;

theorem :: DBLSEQ_2:14
for Rseq being Function of [:NAT,NAT:],REAL
for n, m being Nat holds Rseq . ((n + 1),(m + 1)) = ((((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),(m + 1))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((n + 1),m))) - ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n,m))
proof end;

theorem :: DBLSEQ_2:15
for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is P-convergent holds
( Rseq is P-convergent & P-lim Rseq = 0 )
proof end;

theorem lm74: :: DBLSEQ_2:16
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL holds Partial_Sums (Rseq1 + Rseq2) = (Partial_Sums Rseq1) + (Partial_Sums Rseq2)
proof end;

theorem :: DBLSEQ_2:17
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq1 is P-convergent & Partial_Sums Rseq2 is P-convergent holds
Partial_Sums (Rseq1 + Rseq2) is P-convergent
proof end;

theorem th100: :: DBLSEQ_2:18
for Rseq being Function of [:NAT,NAT:],REAL
for m, n being Element of NAT holds
( (Partial_Sums_in_cod1 Rseq) . (m,n) = (Partial_Sums (ProjMap2 (Rseq,n))) . m & (Partial_Sums_in_cod2 Rseq) . (m,n) = (Partial_Sums (ProjMap1 (Rseq,m))) . n )
proof end;

theorem th00: :: DBLSEQ_2:19
for Rseq being Function of [:NAT,NAT:],REAL holds
( ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) & ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),0) )
proof end;

theorem :: DBLSEQ_2:20
for C, D being non empty set
for F1, F2 being Function of [:C,D:],REAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
proof end;

theorem :: DBLSEQ_2:21
for C, D being non empty set
for F1, F2 being Function of [:C,D:],REAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
proof end;

theorem th01a: :: DBLSEQ_2:22
for Rseq being Function of [:NAT,NAT:],REAL holds
( Partial_Sums Rseq is convergent_in_cod1 iff Partial_Sums_in_cod1 Rseq is convergent_in_cod1 )
proof end;

theorem th01b: :: DBLSEQ_2:23
for Rseq being Function of [:NAT,NAT:],REAL holds
( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )
proof end;

theorem th02a: :: DBLSEQ_2:24
for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod1 holds
for k being Nat holds (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1))
proof end;

theorem th02b: :: DBLSEQ_2:25
for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod2 holds
for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))
proof end;

theorem th03a: :: DBLSEQ_2:26
for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod1 holds
lim_in_cod1 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 Rseq))
proof end;

theorem th03b: :: DBLSEQ_2:27
for Rseq being Function of [:NAT,NAT:],REAL st Partial_Sums Rseq is convergent_in_cod2 holds
lim_in_cod2 (Partial_Sums Rseq) = Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))
proof end;

theorem lm80: :: DBLSEQ_2:28
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )
proof end;

theorem th80a: :: DBLSEQ_2:29
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
Partial_Sums Rseq is non-decreasing
proof end;

theorem :: DBLSEQ_2:30
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( Partial_Sums Rseq is P-convergent iff ( Partial_Sums Rseq is bounded_below & Partial_Sums Rseq is bounded_above ) )
proof end;

theorem lm84a: :: DBLSEQ_2:31
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
for i, j being Nat holds
( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )
proof end;

theorem lm84: :: DBLSEQ_2:32
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)
proof end;

theorem :: DBLSEQ_2:33
for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) & Partial_Sums Rseq2 is P-convergent holds
Partial_Sums Rseq1 is P-convergent
proof end;

theorem th101: :: DBLSEQ_2:34
for rseq being Real_Sequence
for m being Nat st rseq is nonnegative holds
rseq . m <= (Partial_Sums rseq) . m
proof end;

theorem :: DBLSEQ_2:35
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for m, n being Nat holds
( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) )
proof end;

theorem th1003: :: DBLSEQ_2:36
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2) ) )
proof end;

theorem th105: :: DBLSEQ_2:37
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) )
proof end;

theorem :: DBLSEQ_2:38
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds
(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)
proof end;

theorem th1005: :: DBLSEQ_2:39
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is V115() & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is V115() & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )
proof end;

theorem th1006: :: DBLSEQ_2:40
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )
proof end;

theorem th1006a: :: DBLSEQ_2:41
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )
proof end;

theorem :: DBLSEQ_2:42
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable )
proof end;

theorem :: DBLSEQ_2:43
for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent holds
( P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) & P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) )
proof end;

theorem TMP6: :: DBLSEQ_2:44
for s1, s2 being Real_Sequence st s1 is nonnegative & s1,s2 are_fiberwise_equipotent holds
s2 is nonnegative
proof end;

theorem SH1: :: DBLSEQ_2:45
for X being non empty set
for s being sequence of X
for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n
proof end;

registration
let X be non empty set ;
let s be sequence of X;
let n be Nat;
cluster Shift ((s | (Segm n)),1) -> FinSequence-like ;
coherence
Shift ((s | (Segm n)),1) is FinSequence-like
proof end;
end;

theorem SH2: :: DBLSEQ_2:46
for X being non empty set
for s being sequence of X
for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X
proof end;

theorem SH3: :: DBLSEQ_2:47
for X being non empty set
for s being sequence of X
for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds
(Shift ((s | (Segm n)),1)) . (m + 1) = s . m
proof end;

theorem SH4: :: DBLSEQ_2:48
for X being non empty set
for s being sequence of X holds
( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )
proof end;

theorem SH5: :: DBLSEQ_2:49
for s being Real_Sequence
for n being Nat holds (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))
proof end;

theorem SH6: :: DBLSEQ_2:50
for X being non empty set
for s1, s2 being sequence of X
for n being Nat st s1,s2 are_fiberwise_equipotent holds
ex m being Nat ex fs2 being Subset of (Shift ((s2 | (Segm m)),1)) st Shift ((s1 | (Segm (n + 1))),1),fs2 are_fiberwise_equipotent
proof end;

theorem SH7: :: DBLSEQ_2:51
for X being non empty set
for fs being FinSequence of X
for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent
proof end;

theorem SH8: :: DBLSEQ_2:52
for s1, s2 being Real_Sequence
for n being Nat st s1,s2 are_fiberwise_equipotent & s1 is nonnegative holds
ex m being Nat st (Partial_Sums s1) . n <= (Partial_Sums s2) . m
proof end;

theorem :: DBLSEQ_2:53
for s1, s2 being Real_Sequence st s1,s2 are_fiberwise_equipotent & s1 is nonnegative & s1 is summable holds
( s2 is summable & Sum s1 = Sum s2 )
proof end;

theorem :: DBLSEQ_2:54
for D being non empty set
for Rseq being Function of [:NAT,NAT:],D
for n, m being Nat ex M being Matrix of n + 1,m + 1,D st
for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))
proof end;

theorem :: DBLSEQ_2:55
for n, m being Nat
for Rseq being Function of [:NAT,NAT:],REAL
for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds
(Partial_Sums Rseq) . (n,m) = SumAll M
proof end;