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

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: f2 - f1 = f2 + (- f1)

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

let x be Element of X; :: thesis: (f2 - f1) . x = (f2 + (- f1)) . x
dom (- f1) = X by FUNCT_2:def 1;
then (- f1) . x = - (f1 . x) by MESFUNC1:def 7;
then (f2 + (- f1)) . x = (f2 . x) - (f1 . x) by Th7;
hence (f2 - f1) . x = (f2 + (- f1)) . x by Th7; :: thesis: verum

end;

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