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

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: verum