let Rseq be 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)) )
let n, m be Nat; ( (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)) )
set RPS = Partial_Sums Rseq;
set CPS = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq);
set ROW = Partial_Sums_in_cod1 Rseq;
set COL = Partial_Sums_in_cod2 Rseq;
defpred S1[ Nat] means (Partial_Sums Rseq) . ((n + 1),$1) = ((Partial_Sums_in_cod2 Rseq) . ((n + 1),$1)) + ((Partial_Sums Rseq) . (n,$1));
a1:
(Partial_Sums Rseq) . (n,0) = (Partial_Sums_in_cod1 Rseq) . (n,0)
by DefCS;
(Partial_Sums Rseq) . ((n + 1),0) =
(Partial_Sums_in_cod1 Rseq) . ((n + 1),0)
by DefCS
.=
((Partial_Sums_in_cod1 Rseq) . (n,0)) + (Rseq . ((n + 1),0))
by DefRS
;
then a3:
S1[ 0 ]
by a1, DefCS;
a4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
a6:
(Partial_Sums_in_cod2 Rseq) . (
(n + 1),
(k + 1))
= ((Partial_Sums_in_cod2 Rseq) . ((n + 1),k)) + (Rseq . ((n + 1),(k + 1)))
by DefCS;
(Partial_Sums Rseq) . (
n,
(k + 1))
= ((Partial_Sums Rseq) . (n,k)) + ((Partial_Sums_in_cod1 Rseq) . (n,(k + 1)))
by DefCS;
then ((Partial_Sums_in_cod2 Rseq) . ((n + 1),(k + 1))) + ((Partial_Sums Rseq) . (n,(k + 1))) =
((Partial_Sums Rseq) . ((n + 1),k)) + ((Rseq . ((n + 1),(k + 1))) + ((Partial_Sums_in_cod1 Rseq) . (n,(k + 1))))
by A5, a6
.=
((Partial_Sums Rseq) . ((n + 1),k)) + ((Partial_Sums_in_cod1 Rseq) . ((n + 1),(k + 1)))
by DefRS
;
hence
S1[
k + 1]
by DefCS;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(a3, a4);
hence
(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))
defpred S2[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,(m + 1)) = ((Partial_Sums_in_cod1 Rseq) . ($1,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,m));
b1:
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) = (Partial_Sums_in_cod2 Rseq) . (0,m)
by DefRS;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,(m + 1)) =
(Partial_Sums_in_cod2 Rseq) . (0,(m + 1))
by DefRS
.=
((Partial_Sums_in_cod2 Rseq) . (0,m)) + (Rseq . (0,(m + 1)))
by DefCS
;
then b3:
S2[ 0 ]
by b1, DefRS;
b4:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume B5:
S2[
k]
;
S2[k + 1]
b6:
(Partial_Sums_in_cod1 Rseq) . (
(k + 1),
(m + 1))
= ((Partial_Sums_in_cod1 Rseq) . (k,(m + 1))) + (Rseq . ((k + 1),(m + 1)))
by DefRS;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (
(k + 1),
m)
= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,m)) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),m))
by DefRS;
then ((Partial_Sums_in_cod1 Rseq) . ((k + 1),(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),m)) =
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,(m + 1))) + ((Rseq . ((k + 1),(m + 1))) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),m)))
by B5, b6
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,(m + 1))) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),(m + 1)))
by DefCS
;
hence
S2[
k + 1]
by DefRS;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(b3, b4);
hence
(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))
; verum