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 S1[ 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: S1[ 0 ] by DefRS;
a2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[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 S1[k + 1] by DefRS; :: thesis: verum
end;
for k being Nat holds S1[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 S2[ 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: S2[ 0 ] by DefCS;
a5: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[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 S2[k + 1] by DefCS; :: thesis: verum
end;
for k being Nat holds S2[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;