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

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
dom (- f2) = X by FUNCT_2:def 1;
then (- f2) . x = - (f2 . x) by MESFUNC1:def 7;
then (f1 - (- f2)) . x = (f1 . x) - (- (f2 . x)) by Th7;
hence (f1 + f2) . x = (f1 - (- f2)) . x by Th7; :: thesis: verum

end;

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