let X, Y be non empty set ; :: thesis: for f1 being without-infty Function of [:X,Y:],ExtREAL
for f2 being without+infty Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
let f1 be without-infty Function of [:X,Y:],ExtREAL; :: thesis: for f2 being without+infty Function of [:X,Y:],ExtREAL holds
( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )
let f2 be without+infty Function of [:X,Y:],ExtREAL; :: thesis: ( ~ (f1 - f2) = (~ f1) - (~ f2) & ~ (f2 - f1) = (~ f2) - (~ f1) )

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

let z be Element of [:Y,X:]; :: thesis: (~ (f1 - f2)) . z = ((~ f1) - (~ f2)) . z
consider y, x being object such that
A1: ( y in Y & x in X & z = [y,x] ) by ZFMISC_1:def 2;
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;
(~ (f1 - f2)) . z = (~ (f1 - f2)) . (y,x) by A1;
then (~ (f1 - f2)) . z = (f1 - f2) . (x,y) by FUNCT_4:def 8;
then A2: (~ (f1 - f2)) . z = (f1 . z1) - (f2 . z1) by Th7;
( f1 . z1 = f1 . (x,y) & f2 . z1 = f2 . (x,y) ) ;
then ( f1 . z1 = (~ f1) . (y,x) & f2 . z1 = (~ f2) . (y,x) ) by FUNCT_4:def 8;
hence (~ (f1 - f2)) . z = ((~ f1) - (~ f2)) . z by A1, A2, Th7; :: thesis: verum

end;

hence ~ (f1 - f2) = (~ f1) - (~ f2) by FUNCT_2:def 8; :: thesis: ~ (f2 - f1) = (~ f2) - (~ f1)

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

let z be Element of [:Y,X:]; :: thesis: (~ (f2 - f1)) . z = ((~ f2) - (~ f1)) . z
consider y, x being object such that
A1: ( y in Y & x in X & z = [y,x] ) by ZFMISC_1:def 2;
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;
(~ (f2 - f1)) . z = (~ (f2 - f1)) . (y,x) by A1;
then (~ (f2 - f1)) . z = (f2 - f1) . (x,y) by FUNCT_4:def 8;
then A2: (~ (f2 - f1)) . z = (f2 . z1) - (f1 . z1) by Th7;
( f1 . z1 = f1 . (x,y) & f2 . z1 = f2 . (x,y) ) ;
then ( f1 . z1 = (~ f1) . (y,x) & f2 . z1 = (~ f2) . (y,x) ) by FUNCT_4:def 8;
hence (~ (f2 - f1)) . z = ((~ f2) - (~ f1)) . z by A1, A2, Th7; :: thesis: verum

end;

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