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
A3: ( dom g1 = dom f & ( for x being set st x in dom g1 holds
g1 /. x = - (f /. x) ) ) and
A4: ( dom g2 = dom f & ( for x being set st x in dom g2 holds
g2 /. x = - (f /. x) ) ) ; :: thesis: g1 = g2

now :: thesis: for x being Element of Z st x in dom g1 holds
g1 . x = g2 . x

let x be Element of Z; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A5: x in dom g1 ; :: thesis: g1 . x = g2 . x
then A6: g1 /. x = - (f /. x) by A3;
g1 /. x = g2 /. x by A4, A6, A3, A5;
then g1 . x = g2 /. x by A5, PARTFUN1:def 6;
hence g1 . x = g2 . x by A3, A4, A5, PARTFUN1:def 6; :: thesis: verum

end;

hence g1 = g2 by A3, A4, PARTFUN1:5; :: thesis: verum