let n be Element of NAT ; :: thesis: for f1 being PartFunc of REAL, the carrier of (REAL-NS n)
for g1 being PartFunc of REAL,(REAL n) st f1 = g1 holds
- f1 = - g1
let f1 be PartFunc of REAL, the carrier of (REAL-NS n); :: thesis: for g1 being PartFunc of REAL,(REAL n) st f1 = g1 holds
- f1 = - g1
let g1 be PartFunc of REAL,(REAL n); :: thesis: ( f1 = g1 implies - f1 = - g1 )
assume AS: f1 = g1 ; :: thesis: - f1 = - g1
dom (- f1) = dom f1 by VFUNCT_1:def 5;
then A2: dom (- f1) = dom (- g1) by AS, Def5;

B1: now

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

end;

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