let n be Element of NAT ; :: thesis: for f1 being PartFunc of REAL,(REAL n) holds (- 1) (#) f1 = - f1
let f1 be PartFunc of REAL,(REAL n); :: thesis: (- 1) (#) f1 = - f1
F: dom ((- 1) (#) f1) = dom f1 by VALUED_2:def 39;
then A1: dom ((- 1) (#) f1) = dom (- f1) by Def5;

now

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

end;

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