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