let X be non empty set ; :: thesis: for f1, f2 being without-infty Function of X,ExtREAL holds
( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )
let f1, f2 be without-infty Function of X,ExtREAL; :: thesis: ( f1 + f2 = f1 - (- f2) & - (f1 + f2) = (- f1) - f2 )
thus f1 + f2 = f1 - (- f2) by Lm3; :: thesis: - (f1 + f2) = (- f1) - f2
A1: dom (- f1) = X by FUNCT_2:def 1;
A2: dom (- f2) = X by FUNCT_2:def 1;
A3: dom (- (f1 + f2)) = X by FUNCT_2:def 1;

now :: thesis: for x being Element of X holds (- (f1 + f2)) . x = ((- f1) - f2) . x

let x be Element of X; :: thesis: (- (f1 + f2)) . x = ((- f1) - f2) . x
(- (f1 + f2)) . x = - ((f1 + f2) . x) by A3, MESFUNC1:def 7
.= - ((f1 . x) + (f2 . x)) by Th7
.= (- (f1 . x)) - (f2 . x) by XXREAL_3:25
.= ((- f1) . x) + (- (f2 . x)) by A1, MESFUNC1:def 7
.= ((- f1) . x) + ((- f2) . x) by A2, MESFUNC1:def 7
.= ((- f1) + (- f2)) . x by Th7 ;
hence (- (f1 + f2)) . x = ((- f1) - f2) . x by Lm5; :: thesis: verum

end;

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