let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums_in_cod2 (- f) = - (Partial_Sums_in_cod2 f) & Partial_Sums_in_cod1 (- f) = - (Partial_Sums_in_cod1 f) )
A1: ( dom (- (Partial_Sums_in_cod2 f)) = [:NAT,NAT:] & dom (- (Partial_Sums_in_cod1 f)) = [:NAT,NAT:] ) by FUNCT_2:def 1;
A2: dom (- f) = [:NAT,NAT:] by FUNCT_2:def 1;
for z being Element of [:NAT,NAT:] holds (- (Partial_Sums_in_cod2 f)) . z = (Partial_Sums_in_cod2 (- f)) . z

proof

let z be Element of [:NAT,NAT:]; :: thesis: (- (Partial_Sums_in_cod2 f)) . z = (Partial_Sums_in_cod2 (- f)) . z
consider n, m being object such that
A3: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A3;
defpred S₁[ Nat] means (Partial_Sums_in_cod2 (- f)) . (n,$1) = - ((Partial_Sums_in_cod2 f) . (n,$1));
reconsider z0 = [n,0] as Element of [:NAT,NAT:] by ZFMISC_1:87;
A4: [n,0] in [:NAT,NAT:] by ZFMISC_1:87;
(Partial_Sums_in_cod2 (- f)) . (n,0) = (- f) . (n,0) by DefCSM
.= - (f . (n,0)) by A4, A2, MESFUNC1:def 7 ;
then A5: S₁[ 0 ] by DefCSM;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: [n,(k + 1)] in [:NAT,NAT:] by ZFMISC_1:87;
thus (Partial_Sums_in_cod2 (- f)) . (n,(k + 1)) = ((Partial_Sums_in_cod2 (- f)) . (n,k)) + ((- f) . (n,(k + 1))) by DefCSM
.= (- ((Partial_Sums_in_cod2 f) . (n,k))) - (f . (n,(k + 1))) by A7, A8, A2, MESFUNC1:def 7
.= - (((Partial_Sums_in_cod2 f) . (n,k)) + (f . (n,(k + 1)))) by XXREAL_3:25
.= - ((Partial_Sums_in_cod2 f) . (n,(k + 1))) by DefCSM ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then (Partial_Sums_in_cod2 (- f)) . (n,m) = - ((Partial_Sums_in_cod2 f) . (n,m)) ;
hence (- (Partial_Sums_in_cod2 f)) . z = (Partial_Sums_in_cod2 (- f)) . z by A3, A1, MESFUNC1:def 7; :: thesis: verum

end;

hence Partial_Sums_in_cod2 (- f) = - (Partial_Sums_in_cod2 f) by FUNCT_2:def 8; :: thesis: Partial_Sums_in_cod1 (- f) = - (Partial_Sums_in_cod1 f)
for z being Element of [:NAT,NAT:] holds (- (Partial_Sums_in_cod1 f)) . z = (Partial_Sums_in_cod1 (- f)) . z

proof

let z be Element of [:NAT,NAT:]; :: thesis: (- (Partial_Sums_in_cod1 f)) . z = (Partial_Sums_in_cod1 (- f)) . z
consider n, m being object such that
A3: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A3;
defpred S₁[ Nat] means (Partial_Sums_in_cod1 (- f)) . ($1,m) = - ((Partial_Sums_in_cod1 f) . ($1,m));
reconsider z0 = [0,m] as Element of [:NAT,NAT:] by ZFMISC_1:87;
A4: [0,m] in [:NAT,NAT:] by ZFMISC_1:87;
(Partial_Sums_in_cod1 (- f)) . (0,m) = (- f) . (0,m) by DefRSM
.= - (f . (0,m)) by A4, A2, MESFUNC1:def 7 ;
then A5: S₁[ 0 ] by DefRSM;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: [(k + 1),m] in [:NAT,NAT:] by ZFMISC_1:87;
thus (Partial_Sums_in_cod1 (- f)) . ((k + 1),m) = ((Partial_Sums_in_cod1 (- f)) . (k,m)) + ((- f) . ((k + 1),m)) by DefRSM
.= (- ((Partial_Sums_in_cod1 f) . (k,m))) - (f . ((k + 1),m)) by A7, A8, A2, MESFUNC1:def 7
.= - (((Partial_Sums_in_cod1 f) . (k,m)) + (f . ((k + 1),m))) by XXREAL_3:25
.= - ((Partial_Sums_in_cod1 f) . ((k + 1),m)) by DefRSM ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then (Partial_Sums_in_cod1 (- f)) . (n,m) = - ((Partial_Sums_in_cod1 f) . (n,m)) ;
hence (- (Partial_Sums_in_cod1 f)) . z = (Partial_Sums_in_cod1 (- f)) . z by A3, A1, MESFUNC1:def 7; :: thesis: verum

end;

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