let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for m, n being Element of NAT holds
( (Partial_Sums_in_cod1 f) . (m,n) = (Partial_Sums (ProjMap2 (f,n))) . m & (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n )
let m, n be Element of NAT ; :: thesis: ( (Partial_Sums_in_cod1 f) . (m,n) = (Partial_Sums (ProjMap2 (f,n))) . m & (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n )
defpred S1[ Nat] means (Partial_Sums_in_cod1 f) . ($1,n) = (Partial_Sums (ProjMap2 (f,n))) . $1;
(Partial_Sums (ProjMap2 (f,n))) . 0 = (ProjMap2 (f,n)) . 0 by MESFUNC9:def 1
.= f . (0,n) by MESFUNC9:def 7 ;
then a1: S1[ 0 ] by DefRSM;
a2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then (Partial_Sums_in_cod1 f) . ((k + 1),n) = ((Partial_Sums (ProjMap2 (f,n))) . k) + (f . ((k + 1),n)) by DefRSM
.= ((Partial_Sums (ProjMap2 (f,n))) . k) + ((ProjMap2 (f,n)) . (k + 1)) by MESFUNC9:def 7 ;
hence S1[k + 1] by MESFUNC9:def 1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(a1, a2);
 hence (Partial_Sums_in_cod1 f) . (m,n) = (Partial_Sums (ProjMap2 (f,n))) . m ; :: thesis: (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n
defpred S2[ Nat] means (Partial_Sums_in_cod2 f) . (m,$1) = (Partial_Sums (ProjMap1 (f,m))) . $1;
(Partial_Sums (ProjMap1 (f,m))) . 0 = (ProjMap1 (f,m)) . 0 by MESFUNC9:def 1
.= f . (m,0) by MESFUNC9:def 6 ;
then a3: S2[ 0 ] by DefCSM;
a4: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then (Partial_Sums_in_cod2 f) . (m,(k + 1)) = ((Partial_Sums (ProjMap1 (f,m))) . k) + (f . (m,(k + 1))) by DefCSM
.= ((Partial_Sums (ProjMap1 (f,m))) . k) + ((ProjMap1 (f,m)) . (k + 1)) by MESFUNC9:def 6 ;
hence S2[k + 1] by MESFUNC9:def 1; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(a3, a4);
 hence (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n ; :: thesis: verum