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 S₁[ 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: S₁[ 0 ] by DefRSM;
a2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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 S₁[k + 1] by MESFUNC9:def 1; :: thesis: verum

end;

for k being Nat holds S₁[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 S₂[ 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: S₂[ 0 ] by DefCSM;
a4: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[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 S₂[k + 1] by MESFUNC9:def 1; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(a3, a4);
hence (Partial_Sums_in_cod2 f) . (m,n) = (Partial_Sums (ProjMap1 (f,m))) . n ; :: thesis: verum