:: 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{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Function of F₁(),F₂(), F₄( set , set , Nat) -> Element of F₂() } :

ex g being Function of [:F₁(),NAT:],F₂() st
for a being Element of F₁() holds
( g . (a,0) = F₃() . a & ( for n being Nat holds g . (a,(n + 1)) = F₄((g . (a,n)),a,n) ) )

proof end;

scheme :: DBLSEQ_2:sch 2
RecEx2D1R{ F₁() -> non empty set , F₂() -> Function of F₁(),REAL, F₃( set , set , Nat) -> real number } :

ex g being Function of [:F₁(),NAT:],REAL st
for a being Element of F₁() holds
( g . (a,0) = F₂() . a & ( for n being natural number holds g . (a,(n + 1)) = F₃((g . (a,n)),a,n) ) )

proof end;

scheme :: DBLSEQ_2:sch 3
RecEx2D2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Function of F₁(),F₂(), F₄( set , set , Nat) -> Element of F₂() } :

ex g being Function of [:NAT,F₁():],F₂() st
for a being Element of F₁() holds
( g . (0,a) = F₃() . a & ( for n being Nat holds g . ((n + 1),a) = F₄((g . (n,a)),a,n) ) )

proof end;

scheme :: DBLSEQ_2:sch 4
RecEx2D2R{ F₁() -> non empty set , F₂() -> Function of F₁(),REAL, F₃( set , set , Nat) -> real number } :

ex g being Function of [:NAT,F₁():],REAL st
for a being Element of F₁() holds
( g . (0,a) = F₂() . a & ( for n being Nat holds g . ((n + 1),a) = F₃((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 b₁ being Function of [:NAT,NAT:],REAL st
for n, m being Nat holds
( b₁ . (n,0) = Rseq . (n,0) & b₁ . (n,(m + 1)) = (b₁ . (n,m)) + (Rseq . (n,(m + 1))) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds
( b₁ . (n,0) = Rseq . (n,0) & b₁ . (n,(m + 1)) = (b₁ . (n,m)) + (Rseq . (n,(m + 1))) ) ) & ( for n, m being Nat holds
( b₂ . (n,0) = Rseq . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (n,m)) + (Rseq . (n,(m + 1))) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefCS defines Partial_Sums_in_cod2 DBLSEQ_2:def 2 :
for Rseq, b₂ being Function of [:NAT,NAT:],REAL holds
( b₂ = Partial_Sums_in_cod2 Rseq iff for n, m being Nat holds
( b₂ . (n,0) = Rseq . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (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 b₁ being Function of [:NAT,NAT:],REAL st
for n, m being Nat holds
( b₁ . (0,m) = Rseq . (0,m) & b₁ . ((n + 1),m) = (b₁ . (n,m)) + (Rseq . ((n + 1),m)) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds
( b₁ . (0,m) = Rseq . (0,m) & b₁ . ((n + 1),m) = (b₁ . (n,m)) + (Rseq . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( b₂ . (0,m) = Rseq . (0,m) & b₂ . ((n + 1),m) = (b₂ . (n,m)) + (Rseq . ((n + 1),m)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefRS defines Partial_Sums_in_cod1 DBLSEQ_2:def 3 :
for Rseq, b₂ being Function of [:NAT,NAT:],REAL holds
( b₂ = Partial_Sums_in_cod1 Rseq iff for n, m being Nat holds
( b₂ . (0,m) = Rseq . (0,m) & b₂ . ((n + 1),m) = (b₂ . (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;