let Rseq be Function of [:NAT,NAT:],REAL; ( Rseq is nonnegative-yielding implies ( ( 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) ) ) )
assume A1:
Rseq is nonnegative-yielding
; ( ( 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) ) )
A2:
now for i1, i2, j being natural number st i1 <= i2 holds
(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j)let i1,
i2,
j be
natural number ;
( i1 <= i2 implies (Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j) )assume
i1 <= i2
;
(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j)then consider k being
Nat such that A3:
i2 = i1 + k
by NAT_1:10;
defpred S1[
Nat]
means ( $1
<= k implies
(Partial_Sums_in_cod1 Rseq) . (
i1,
j)
<= (Partial_Sums_in_cod1 Rseq) . (
(i1 + $1),
j) );
A4:
S1[
0 ]
;
A5:
for
l being
Nat st
S1[
l] holds
S1[
l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume A6:
S1[
l]
;
S1[l + 1]
now ( l + 1 <= k implies (Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . ((i1 + (l + 1)),j) )assume A7:
l + 1
<= k
;
(Partial_Sums_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . ((i1 + (l + 1)),j)
(Partial_Sums_in_cod1 Rseq) . (
((i1 + l) + 1),
j)
= ((Partial_Sums_in_cod1 Rseq) . ((i1 + l),j)) + (Rseq . (((i1 + l) + 1),j))
by DefRS;
then
(Partial_Sums_in_cod1 Rseq) . (
(i1 + l),
j)
<= (Partial_Sums_in_cod1 Rseq) . (
((i1 + l) + 1),
j)
by A1, XREAL_1:31;
hence
(Partial_Sums_in_cod1 Rseq) . (
i1,
j)
<= (Partial_Sums_in_cod1 Rseq) . (
(i1 + (l + 1)),
j)
by A6, A7, NAT_1:13, XXREAL_0:2;
verum end;
hence
S1[
l + 1]
;
verum
end;
for
l being
Nat holds
S1[
l]
from NAT_1:sch 2(A4, A5);
hence
(Partial_Sums_in_cod1 Rseq) . (
i1,
j)
<= (Partial_Sums_in_cod1 Rseq) . (
i2,
j)
by A3;
verum end;
now for i, j1, j2 being natural number st j1 <= j2 holds
(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2)let i,
j1,
j2 be
natural number ;
( j1 <= j2 implies (Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2) )assume
j1 <= j2
;
(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2)then consider k being
Nat such that B3:
j2 = j1 + k
by NAT_1:10;
defpred S1[
Nat]
means ( $1
<= k implies
(Partial_Sums_in_cod2 Rseq) . (
i,
j1)
<= (Partial_Sums_in_cod2 Rseq) . (
i,
(j1 + $1)) );
B4:
S1[
0 ]
;
B5:
for
l being
Nat st
S1[
l] holds
S1[
l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume B6:
S1[
l]
;
S1[l + 1]
now ( l + 1 <= k implies (Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,(j1 + (l + 1))) )assume B7:
l + 1
<= k
;
(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,(j1 + (l + 1)))
(Partial_Sums_in_cod2 Rseq) . (
i,
((j1 + l) + 1))
= ((Partial_Sums_in_cod2 Rseq) . (i,(j1 + l))) + (Rseq . (i,((j1 + l) + 1)))
by DefCS;
then
(Partial_Sums_in_cod2 Rseq) . (
i,
(j1 + l))
<= (Partial_Sums_in_cod2 Rseq) . (
i,
((j1 + l) + 1))
by A1, XREAL_1:31;
hence
(Partial_Sums_in_cod2 Rseq) . (
i,
j1)
<= (Partial_Sums_in_cod2 Rseq) . (
i,
(j1 + (l + 1)))
by B6, B7, NAT_1:13, XXREAL_0:2;
verum end;
hence
S1[
l + 1]
;
verum
end;
for
l being
Nat holds
S1[
l]
from NAT_1:sch 2(B4, B5);
hence
(Partial_Sums_in_cod2 Rseq) . (
i,
j1)
<= (Partial_Sums_in_cod2 Rseq) . (
i,
j2)
by B3;
verum end;
hence
( ( 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) ) )
by A2; verum