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 S1[ 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: S1[ 0 ] by MESFUNC9:def 1;
A3: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; :: thesis: S1[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 S1[m + 1] by MESFUNC9:def 1; :: thesis: verum
end;
for m being Nat holds S1[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