let X be non empty set ; :: thesis: for A being set

for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

let A be set ; :: thesis: for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

let f be PartFunc of X,ExtREAL; :: thesis: - (f | A) = (- f) | A

- (f | A) = (- 1) (#) (f | A) by MESFUNC2:9;

then - (f | A) = ((- 1) (#) f) | A by Th2;

hence - (f | A) = (- f) | A by MESFUNC2:9; :: thesis: verum

for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

let A be set ; :: thesis: for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

let f be PartFunc of X,ExtREAL; :: thesis: - (f | A) = (- f) | A

- (f | A) = (- 1) (#) (f | A) by MESFUNC2:9;

then - (f | A) = ((- 1) (#) f) | A by Th2;

hence - (f | A) = (- f) | A by MESFUNC2:9; :: thesis: verum