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 & dom ((- 1) (#) f) = dom f ) by MESFUNC1:def 6, MESFUNC1:def 7;
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 A2: x in dom f ; :: thesis: (- f) . x = ((- 1) (#) f) . x
then ( (- f) . x = - (f . x) & ((- 1) (#) f) . x = (R_EAL (- 1)) * (f . x) ) by A1, MESFUNC1:def 6, MESFUNC1:def 7;
then ((- 1) (#) f) . x = (- (R_EAL 1)) * (f . x) by SUPINF_2:3
.= - ((R_EAL 1) * (f . x)) by XXREAL_3:103
.= - (f . x) by XXREAL_3:92 ;
hence (- f) . x = ((- 1) (#) f) . x by A1, A2, MESFUNC1:def 7; :: thesis: verum

end;

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