let X, Y be non empty set ; :: thesis: for f being Function of [:X,Y:],ExtREAL holds ~ (- f) = - (~ f)
let f be Function of [:X,Y:],ExtREAL; :: thesis: ~ (- f) = - (~ f)

now :: thesis: for z being Element of [:Y,X:] holds (~ (- f)) . z = (- (~ f)) . z

let z be Element of [:Y,X:]; :: thesis: (~ (- f)) . z = (- (~ f)) . z
consider y, x being object such that
A1: ( y in Y & x in X & z = [y,x] ) by ZFMISC_1:def 2;
A2: ( dom (- f) = [:X,Y:] & dom (- (~ f)) = [:Y,X:] ) by FUNCT_2:def 1;
reconsider y = y as Element of Y by A1;
reconsider x = x as Element of X by A1;
reconsider z1 = [x,y] as Element of [:X,Y:] by ZFMISC_1:87;
(~ (- f)) . z = (~ (- f)) . (y,x) by A1;
then (~ (- f)) . z = (- f) . (x,y) by FUNCT_4:def 8;
then (~ (- f)) . z = - (f . z1) by A2, MESFUNC1:def 7;
then (~ (- f)) . z = - (f . (x,y)) ;
then (~ (- f)) . z = - ((~ f) . (y,x)) by FUNCT_4:def 8;
hence (~ (- f)) . z = (- (~ f)) . z by A1, A2, MESFUNC1:def 7; :: thesis: verum

end;

hence ~ (- f) = - (~ f) by FUNCT_2:def 8; :: thesis: verum