let f be V183() Function of [:NAT,NAT:],ExtREAL; :: thesis: Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)
now :: thesis: for x being Element of [:NAT,NAT:] holds (Partial_Sums f) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . x
let x be Element of [:NAT,NAT:]; :: thesis: (Partial_Sums f) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . 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 f) . (n1,m1) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n1,m1) by Lm7;
hence (Partial_Sums f) . x = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . x by A1; :: thesis: verum
end;
hence Partial_Sums f = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) by FUNCT_2:63; :: thesis: verum