let n be Element of NAT ; :: thesis: for W being non empty set
for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let W be non empty set ; :: thesis: for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
let f1 be PartFunc of W,(REAL n); :: thesis: (- 1) (#) f1 = - f1
A1: dom ((- 1) (#) f1) = dom f1 by VALUED_2:def 39;
then A2: dom ((- 1) (#) f1) = dom (- f1) by Def3;

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

let x be Element of W; :: thesis: ( x in dom ((- 1) (#) f1) implies ((- 1) (#) f1) . x = (- f1) . x )
assume A3: x in dom ((- 1) (#) f1) ; :: thesis: ((- 1) (#) f1) . x = (- f1) . x
A4: f1 . x = f1 /. x by A1, A3, PARTFUN1:def 6;
A5: (- f1) /. x = - (f1 /. x) by A2, A3, Def3;
(f1 [#] (- 1)) . x = (- 1) (#) (f1 . x) by A3, VALUED_2:def 39;
hence ((- 1) (#) f1) . x = (- f1) . x by A4, A2, A3, A5, PARTFUN1:def 6; :: thesis: verum

end;

hence (- 1) (#) f1 = - f1 by A2, PARTFUN1:5; :: thesis: verum