let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for g being ext-real-valued Function
for n being Nat st ( for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ) holds
( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g )
let g be ext-real-valued Function; :: thesis: for n being Nat st ( for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ) holds
( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g )
let n be Nat; :: thesis: ( ( for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ) implies ( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g ) )
assume A1: for k being Nat holds (Partial_Sums_in_cod1 f) . (n,k) = g . k ; :: thesis: ( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g )

A4: now :: thesis: for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k

let k be Nat; :: thesis: (Partial_Sums f) . (n,k) = (Partial_Sums g) . k
defpred S₁[ Nat] means (Partial_Sums f) . (n,$1) = (Partial_Sums g) . $1;
(Partial_Sums f) . (n,0) = (Partial_Sums_in_cod1 f) . (n,0) by DefCSM
.= g . 0 by A1 ;
then A2: S₁[ 0 ] by MESFUNC9:def 1;
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
(Partial_Sums f) . (n,(m + 1)) = ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)) . (n,m)) + ((Partial_Sums_in_cod1 f) . (n,(m + 1))) by DefCSM
.= ((Partial_Sums g) . m) + (g . (m + 1)) by A1, A4 ;
hence S₁[m + 1] by MESFUNC9:def 1; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A3);
hence (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ; :: thesis: verum

end;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: for k being Element of NAT holds (ProjMap1 ((Partial_Sums f),n1)) . k = (Partial_Sums g) . k

let k be Element of NAT ; :: thesis: (ProjMap1 ((Partial_Sums f),n1)) . k = (Partial_Sums g) . k
(ProjMap1 ((Partial_Sums f),n1)) . k = (Partial_Sums f) . (n,k) by MESFUNC9:def 6;
hence (ProjMap1 ((Partial_Sums f),n1)) . k = (Partial_Sums g) . k by A4; :: thesis: verum

end;

then ProjMap1 ((Partial_Sums f),n1) = Partial_Sums g by FUNCT_2:def 8;
then (lim_in_cod2 (Partial_Sums f)) . n1 = lim (Partial_Sums g) by D1DEF6;
hence ( ( for k being Nat holds (Partial_Sums f) . (n,k) = (Partial_Sums g) . k ) & (lim_in_cod2 (Partial_Sums f)) . n = Sum g ) by A4, MESFUNC9:def 3; :: thesis: verum