let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: Partial_Sums Rseq = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)
now :: thesis: for x being Element of [:NAT,NAT:] holds (Partial_Sums Rseq) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . x
let x be Element of [:NAT,NAT:]; :: thesis: (Partial_Sums Rseq) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . x
consider n, m being object such that
A1: ( n in NAT & m in NAT & x = [n,m] ) by ZFMISC_1:def 2;
reconsider n1 = n, m1 = m as Nat by A1;
(Partial_Sums Rseq) . (n1,m1) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (n1,m1) by th103;
hence (Partial_Sums Rseq) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . x by A1; :: thesis: verum
end;
hence Partial_Sums Rseq = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq) ; :: thesis: verum