let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f
let f be PartFunc of C,ExtREAL ; :: thesis: - f = (- 1) (#) f
A1: dom (- f) = dom f by MESFUNC1:def 7;
A2: dom ((- 1) (#) f) = dom f by MESFUNC1:def 6;
A3: for x being Element of C st x in dom f holds
(- f) . x = ((- 1) (#) f) . x

proof

let x be Element of C; :: thesis: ( x in dom f implies (- f) . x = ((- 1) (#) f) . x )
assume A4: x in dom f ; :: thesis: (- f) . x = ((- 1) (#) f) . x
A5: ((- 1) (#) f) . x = (R_EAL (- 1)) * (f . x) by A2, A4, MESFUNC1:def 6;
A6: ((- 1) (#) f) . x = (- (R_EAL 1)) * (f . x) by A5, SUPINF_2:3
.= - ((R_EAL 1) * (f . x)) by XXREAL_3:103
.= - (f . x) by XXREAL_3:92 ;
thus (- f) . x = ((- 1) (#) f) . x by A1, A4, A6, MESFUNC1:def 7; :: thesis: verum

end;

thus - f = (- 1) (#) f by A1, A2, A3, PARTFUN1:34; :: thesis: verum