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