let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f = - g holds

g = - f

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f = - g implies g = - f )

assume f = - g ; :: thesis: g = - f

then f = (- 1) (#) g by MESFUNC2:9;

then - f = (- 1) (#) ((- 1) (#) g) by MESFUNC2:9;

then - f = ((- 1) * (- 1)) (#) g by Th35;

hence g = - f by MESFUNC2:1; :: thesis: verum

g = - f

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f = - g implies g = - f )

assume f = - g ; :: thesis: g = - f

then f = (- 1) (#) g by MESFUNC2:9;

then - f = (- 1) (#) ((- 1) (#) g) by MESFUNC2:9;

then - f = ((- 1) * (- 1)) (#) g by Th35;

hence g = - f by MESFUNC2:1; :: thesis: verum