let Rseq be 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 )
let m, n be Element of NAT ; ( (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 )
defpred S1[ Nat] means (Partial_Sums_in_cod1 Rseq) . ($1,n) = (Partial_Sums (ProjMap2 (Rseq,n))) . $1;
(Partial_Sums (ProjMap2 (Rseq,n))) . 0 =
(ProjMap2 (Rseq,n)) . 0
by SERIES_1:def 1
.=
Rseq . (0,n)
by MESFUNC9:def 7
;
then a1:
S1[ 0 ]
by DefRS;
a2:
for k being Nat st S1[k] holds
S1[k + 1]
for k being Nat holds S1[k]
from NAT_1:sch 2(a1, a2);
hence
(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
defpred S2[ Nat] means (Partial_Sums_in_cod2 Rseq) . (m,$1) = (Partial_Sums (ProjMap1 (Rseq,m))) . $1;
(Partial_Sums (ProjMap1 (Rseq,m))) . 0 =
(ProjMap1 (Rseq,m)) . 0
by SERIES_1:def 1
.=
Rseq . (m,0)
by MESFUNC9:def 6
;
then a3:
S2[ 0 ]
by DefCS;
a4:
for k being Nat st S2[k] holds
S2[k + 1]
for k being Nat holds S2[k]
from NAT_1:sch 2(a3, a4);
hence
(Partial_Sums_in_cod2 Rseq) . (m,n) = (Partial_Sums (ProjMap1 (Rseq,m))) . n
; verum