let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums_in_cod2 Rseq = ~ (Partial_Sums_in_cod1 (~ Rseq)) & Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) & ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )
now :: thesis: for n, m being Element of NAT holds (Partial_Sums_in_cod2 Rseq) . (n,m) = (~ (Partial_Sums_in_cod1 (~ Rseq))) . (n,m)
let n, m be Element of NAT ; :: thesis: (Partial_Sums_in_cod2 Rseq) . (n,m) = (~ (Partial_Sums_in_cod1 (~ Rseq))) . (n,m)
(Partial_Sums_in_cod2 Rseq) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (m,n) by Tr2;
hence (Partial_Sums_in_cod2 Rseq) . (n,m) = (~ (Partial_Sums_in_cod1 (~ Rseq))) . (n,m) by FUNCT_4:def 8; :: thesis: verum
end;
hence Partial_Sums_in_cod2 Rseq = ~ (Partial_Sums_in_cod1 (~ Rseq)) by BINOP_1:2; :: thesis: ( Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) & ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )
now :: thesis: for n, m being Element of NAT holds (Partial_Sums_in_cod2 (~ Rseq)) . (n,m) = (~ (Partial_Sums_in_cod1 Rseq)) . (n,m)
let n, m be Element of NAT ; :: thesis: (Partial_Sums_in_cod2 (~ Rseq)) . (n,m) = (~ (Partial_Sums_in_cod1 Rseq)) . (n,m)
(Partial_Sums_in_cod2 (~ Rseq)) . (n,m) = (Partial_Sums_in_cod1 Rseq) . (m,n) by Tr2;
hence (Partial_Sums_in_cod2 (~ Rseq)) . (n,m) = (~ (Partial_Sums_in_cod1 Rseq)) . (n,m) by FUNCT_4:def 8; :: thesis: verum
end;
hence a1: Partial_Sums_in_cod2 (~ Rseq) = ~ (Partial_Sums_in_cod1 Rseq) by BINOP_1:2; :: thesis: ( ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) & ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq )
now :: thesis: for n, m being Element of NAT holds (~ (Partial_Sums_in_cod2 Rseq)) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (n,m)
let n, m be Element of NAT ; :: thesis: (~ (Partial_Sums_in_cod2 Rseq)) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (n,m)
(~ (Partial_Sums_in_cod2 Rseq)) . (n,m) = (Partial_Sums_in_cod2 Rseq) . (m,n) by FUNCT_4:def 8;
hence (~ (Partial_Sums_in_cod2 Rseq)) . (n,m) = (Partial_Sums_in_cod1 (~ Rseq)) . (n,m) by Tr2; :: thesis: verum
end;
hence ~ (Partial_Sums_in_cod2 Rseq) = Partial_Sums_in_cod1 (~ Rseq) by BINOP_1:2; :: thesis: ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq
now :: thesis: for n, m being Element of NAT holds (~ (Partial_Sums_in_cod2 (~ Rseq))) . (n,m) = (Partial_Sums_in_cod1 Rseq) . (n,m)
let n, m be Element of NAT ; :: thesis: (~ (Partial_Sums_in_cod2 (~ Rseq))) . (n,m) = (Partial_Sums_in_cod1 Rseq) . (n,m)
(~ (Partial_Sums_in_cod2 (~ Rseq))) . (n,m) = (~ (Partial_Sums_in_cod1 Rseq)) . (m,n) by a1, FUNCT_4:def 8;
hence (~ (Partial_Sums_in_cod2 (~ Rseq))) . (n,m) = (Partial_Sums_in_cod1 Rseq) . (n,m) by FUNCT_4:def 8; :: thesis: verum
end;
hence ~ (Partial_Sums_in_cod2 (~ Rseq)) = Partial_Sums_in_cod1 Rseq by BINOP_1:2; :: thesis: verum