let n be Element of NAT ; :: thesis: for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let W be non empty set ; :: thesis: for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let f1 be PartFunc of W,(REAL-NS n); :: thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
let g1 be PartFunc of W,(REAL n); :: thesis: ( f1 = g1 implies - f1 = - g1 )
assume A1: f1 = g1 ; :: thesis: - f1 = - g1
dom (- f1) = dom f1 by VFUNCT_1:def 5;
then A2: dom (- f1) = dom (- g1) by A1, Def3;

A3: now :: thesis: for x being Element of W st x in dom (- f1) holds
(- f1) . x = (- g1) . x

let x be Element of W; :: thesis: ( x in dom (- f1) implies (- f1) . x = (- g1) . x )
assume A4: x in dom (- f1) ; :: thesis: (- f1) . x = (- g1) . x
f1 /. x = g1 /. x by A1, REAL_NS1:def 4;
then A5: - (f1 /. x) = - (g1 /. x) by REAL_NS1:4;
A6: (- f1) /. x = - (f1 /. x) by A4, VFUNCT_1:def 5;
(- g1) /. x = - (g1 /. x) by A2, A4, Def3;
then (- f1) . x = (- g1) /. x by A4, A5, A6, PARTFUN1:def 6;
hence (- f1) . x = (- g1) . x by A2, A4, PARTFUN1:def 6; :: thesis: verum

end;

- f1 is PartFunc of W,(REAL n) by REAL_NS1:def 4;
hence - f1 = - g1 by A2, A3, PARTFUN1:5; :: thesis: verum