let X, Y be non empty set ; for f being Function of [:X,Y:],ExtREAL holds ~ (- f) = - (~ f)
let f be Function of [:X,Y:],ExtREAL; ~ (- f) = - (~ f)
now for z being Element of [:Y,X:] holds (~ (- f)) . z = (- (~ f)) . zlet z be
Element of
[:Y,X:];
(~ (- f)) . z = (- (~ f)) . zconsider 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;
verum end;
hence
~ (- f) = - (~ f)
by FUNCT_2:def 8; verum