let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for n, m being Nat holds
( (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) & (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) )

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) & (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) )
defpred S₁[ Nat] means (Partial_Sums_in_cod2 Rseq) . (n,$1) = (Partial_Sums_in_cod1 (~ Rseq)) . ($1,n);
Z: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
(Partial_Sums_in_cod2 Rseq) . (n,0) = Rseq . (n,0) by DefCS;
then (Partial_Sums_in_cod2 Rseq) . (n,0) = (~ Rseq) . (0,n) by Z, FUNCT_4:def 8;
then a1: S₁[ 0 ] by DefRS;

a2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (Partial_Sums_in_cod2 Rseq) . (n,(k + 1)) = ((Partial_Sums_in_cod1 (~ Rseq)) . (k,n)) + (Rseq . (n,(k + 1))) by DefCS
.= ((Partial_Sums_in_cod1 (~ Rseq)) . (k,n)) + ((~ Rseq) . ((k + 1),n)) by FUNCT_4:def 8, Z ;
hence S₁[k + 1] by DefRS; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(a1, a2);
hence (Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) ; :: thesis: (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n)
Z: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
defpred S₂[ Nat] means (Partial_Sums_in_cod1 Rseq) . ($1,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,$1);
(Partial_Sums_in_cod1 Rseq) . (0,m) = Rseq . (0,m) by DefRS;
then (Partial_Sums_in_cod1 Rseq) . (0,m) = (~ Rseq) . (m,0) by Z, FUNCT_4:def 8;
then a4: S₂[ 0 ] by DefCS;

a5: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
then (Partial_Sums_in_cod1 Rseq) . ((k + 1),m) = ((Partial_Sums_in_cod2 (~ Rseq)) . (m,k)) + (Rseq . ((k + 1),m)) by DefRS
.= ((Partial_Sums_in_cod2 (~ Rseq)) . (m,k)) + ((~ Rseq) . (m,(k + 1))) by Z, FUNCT_4:def 8 ;
hence S₂[k + 1] by DefCS; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(a4, a5);
hence (Partial_Sums_in_cod1 Rseq) . (n,m) = (Partial_Sums_in_cod2 (~ Rseq)) . (m,n) ; :: thesis: verum

end;