let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for n, m being Nat holds
( (Partial_Sums_in_cod1 f) . (n,m) = (Partial_Sums_in_cod2 (~ f)) . (m,n) & (Partial_Sums_in_cod2 f) . (n,m) = (Partial_Sums_in_cod1 (~ f)) . (m,n) )
let n, m be Nat; :: thesis: ( (Partial_Sums_in_cod1 f) . (n,m) = (Partial_Sums_in_cod2 (~ f)) . (m,n) & (Partial_Sums_in_cod2 f) . (n,m) = (Partial_Sums_in_cod1 (~ f)) . (m,n) )
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
defpred S1[ Nat] means (Partial_Sums_in_cod1 f) . ($1,m) = (Partial_Sums_in_cod2 (~ f)) . (m,$1);
(Partial_Sums_in_cod1 f) . (0,m) = f . (0,m) by DefRSM
.= (~ f) . (m1,0) by FUNCT_4:def 8 ;
then A2: S1[ 0 ] by DefCSM;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
(Partial_Sums_in_cod1 f) . ((k + 1),m) = ((Partial_Sums_in_cod1 f) . (k,m)) + (f . ((k + 1),m)) by DefRSM
.= ((Partial_Sums_in_cod2 (~ f)) . (m,k)) + ((~ f) . (m1,(k + 1))) by A4, FUNCT_4:def 8 ;
hence S1[k + 1] by DefCSM; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
 hence (Partial_Sums_in_cod1 f) . (n,m) = (Partial_Sums_in_cod2 (~ f)) . (m,n) ; :: thesis: (Partial_Sums_in_cod2 f) . (n,m) = (Partial_Sums_in_cod1 (~ f)) . (m,n)
defpred S2[ Nat] means (Partial_Sums_in_cod2 f) . (n,$1) = (Partial_Sums_in_cod1 (~ f)) . ($1,n);
(Partial_Sums_in_cod2 f) . (n,0) = f . (n,0) by DefCSM
.= (~ f) . (0,n1) by FUNCT_4:def 8 ;
then A5: S2[ 0 ] by DefRSM;
A6: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A7: S2[k] ; :: thesis: S2[k + 1]
(Partial_Sums_in_cod2 f) . (n,(k + 1)) = ((Partial_Sums_in_cod2 f) . (n,k)) + (f . (n,(k + 1))) by DefCSM
.= ((Partial_Sums_in_cod1 (~ f)) . (k,n)) + ((~ f) . ((k + 1),n1)) by A7, FUNCT_4:def 8 ;
hence S2[k + 1] by DefRSM; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A5, A6);
 hence (Partial_Sums_in_cod2 f) . (n,m) = (Partial_Sums_in_cod1 (~ f)) . (m,n) ; :: thesis: verum