let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ~ (Partial_Sums_in_cod1 f) = Partial_Sums_in_cod2 (~ f) & ~ (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (~ f) )

now :: thesis: for z being Element of [:NAT,NAT:] holds (Partial_Sums_in_cod2 (~ f)) . z = (~ (Partial_Sums_in_cod1 f)) . z

let z be Element of [:NAT,NAT:]; :: thesis: (Partial_Sums_in_cod2 (~ f)) . z = (~ (Partial_Sums_in_cod1 f)) . z
consider n, m being object such that
A1: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A1;
(Partial_Sums_in_cod2 (~ f)) . z = (Partial_Sums_in_cod2 (~ f)) . (n,m) by A1
.= (Partial_Sums_in_cod1 f) . (m,n) by Th39
.= (~ (Partial_Sums_in_cod1 f)) . (n,m) by FUNCT_4:def 8 ;
hence (Partial_Sums_in_cod2 (~ f)) . z = (~ (Partial_Sums_in_cod1 f)) . z by A1; :: thesis: verum

end;

hence ~ (Partial_Sums_in_cod1 f) = Partial_Sums_in_cod2 (~ f) by FUNCT_2:def 8; :: thesis: ~ (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (~ f)

now :: thesis: for z being Element of [:NAT,NAT:] holds (Partial_Sums_in_cod1 (~ f)) . z = (~ (Partial_Sums_in_cod2 f)) . z

let z be Element of [:NAT,NAT:]; :: thesis: (Partial_Sums_in_cod1 (~ f)) . z = (~ (Partial_Sums_in_cod2 f)) . z
consider n, m being object such that
A2: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A2;
(Partial_Sums_in_cod1 (~ f)) . z = (Partial_Sums_in_cod1 (~ f)) . (n,m) by A2
.= (Partial_Sums_in_cod2 f) . (m,n) by Th39
.= (~ (Partial_Sums_in_cod2 f)) . (n,m) by FUNCT_4:def 8 ;
hence (Partial_Sums_in_cod1 (~ f)) . z = (~ (Partial_Sums_in_cod2 f)) . z by A2; :: thesis: verum

end;

hence ~ (Partial_Sums_in_cod2 f) = Partial_Sums_in_cod1 (~ f) by FUNCT_2:def 8; :: thesis: verum