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;
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 A3: x in dom f ; :: thesis: (- f) . x = ((- 1) (#) f) . x
then A4: ((- 1) (#) f) . x = (- 1) * (f . x) by A2, MESFUNC1:def 6;
((- 1) (#) f) . x = ((- jj) (#) f) . x
.= (- 1.) * (f . x) by SUPINF_2:2, A4
.= - (1. * (f . x)) by XXREAL_3:92
.= - (1 * (f . x))
.= - (f . x) by XXREAL_3:81 ;
hence (- f) . x = ((- 1) (#) f) . x by A1, A3, MESFUNC1:def 7; :: thesis: verum

end;

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