let g1, g2 be PartFunc of Z,(REAL n); :: thesis: ( dom g1 = dom f & ( for c being set st c in dom g1 holds
g1 /. c = - (f /. c) ) & dom g2 = dom f & ( for c being set st c in dom g2 holds
g2 /. c = - (f /. c) ) implies g1 = g2 )
assume that
A1: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = - (f /. x) ) ) and
A2: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = - (f /. x) ) ) ; :: thesis: g1 = g2

now

let x be Element of Z; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume P10: x in dom g1 ; :: thesis: g1 . x = g2 . x
then P12: g1 /. x = - (f /. x) by A1;
g1 /. x = g2 /. x by A2, P12, A1, P10;
then g1 . x = g2 /. x by P10, PARTFUN1:def 6;
hence g1 . x = g2 . x by A1, A2, P10, PARTFUN1:def 6; :: thesis: verum

end;

hence g1 = g2 by A1, A2, PARTFUN1:5; :: thesis: verum