let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; ( ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) implies 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) ) )
set RS1 = Partial_Sums_in_cod1 Rseq1;
set RS2 = Partial_Sums_in_cod1 Rseq2;
set CS1 = Partial_Sums_in_cod2 Rseq1;
set CS2 = Partial_Sums_in_cod2 Rseq2;
assume a1:
for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m)
; 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) )
let i, j be Nat; ( (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) )
defpred S1[ Nat] means (Partial_Sums_in_cod1 Rseq1) . ($1,j) <= (Partial_Sums_in_cod1 Rseq2) . ($1,j);
( (Partial_Sums_in_cod1 Rseq1) . (0,j) = Rseq1 . (0,j) & (Partial_Sums_in_cod1 Rseq2) . (0,j) = Rseq2 . (0,j) )
by DefRS;
then a2:
S1[ 0 ]
by a1;
a3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
then a4:
(
(Partial_Sums_in_cod1 Rseq1) . (
k,
j)
<= (Partial_Sums_in_cod1 Rseq2) . (
k,
j) &
Rseq1 . (
(k + 1),
j)
<= Rseq2 . (
(k + 1),
j) )
by a1;
(
(Partial_Sums_in_cod1 Rseq1) . (
(k + 1),
j)
= ((Partial_Sums_in_cod1 Rseq1) . (k,j)) + (Rseq1 . ((k + 1),j)) &
(Partial_Sums_in_cod1 Rseq2) . (
(k + 1),
j)
= ((Partial_Sums_in_cod1 Rseq2) . (k,j)) + (Rseq2 . ((k + 1),j)) )
by DefRS;
hence
S1[
k + 1]
by a4, XREAL_1:7;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(a2, a3);
hence
(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)
defpred S2[ Nat] means (Partial_Sums_in_cod2 Rseq1) . (i,$1) <= (Partial_Sums_in_cod2 Rseq2) . (i,$1);
( (Partial_Sums_in_cod2 Rseq1) . (i,0) = Rseq1 . (i,0) & (Partial_Sums_in_cod2 Rseq2) . (i,0) = Rseq2 . (i,0) )
by DefCS;
then a5:
S2[ 0 ]
by a1;
a6:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume
S2[
k]
;
S2[k + 1]
then a7:
(
(Partial_Sums_in_cod2 Rseq1) . (
i,
k)
<= (Partial_Sums_in_cod2 Rseq2) . (
i,
k) &
Rseq1 . (
i,
(k + 1))
<= Rseq2 . (
i,
(k + 1)) )
by a1;
(
(Partial_Sums_in_cod2 Rseq1) . (
i,
(k + 1))
= ((Partial_Sums_in_cod2 Rseq1) . (i,k)) + (Rseq1 . (i,(k + 1))) &
(Partial_Sums_in_cod2 Rseq2) . (
i,
(k + 1))
= ((Partial_Sums_in_cod2 Rseq2) . (i,k)) + (Rseq2 . (i,(k + 1))) )
by DefCS;
hence
S2[
k + 1]
by a7, XREAL_1:7;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(a5, a6);
hence
(Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j)
; verum