let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds - (- f) = f
let f be PartFunc of X,ExtREAL; :: thesis: - (- f) = f
A1: dom f = dom (- f) by MESFUNC1:def 7;
then A2: dom f = dom (- (- f)) by MESFUNC1:def 7;

now :: thesis: for x being object st x in dom f holds
(- (- f)) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (- (- f)) . x = f . x )
assume A3: x in dom f ; :: thesis: (- (- f)) . x = f . x
then (- f) . x = - (f . x) by A1, MESFUNC1:def 7;
then (- (- f)) . x = - (- (f . x)) by A2, A3, MESFUNC1:def 7;
hence (- (- f)) . x = f . x ; :: thesis: verum

end;

hence - (- f) = f by A2, FUNCT_1:2; :: thesis: verum