let X be non empty set ; for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds
( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )
let f1, f2 be Function of X,ExtREAL; ( f2 is V120() & f2 is V121() implies ( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) ) )
assume A1:
( f2 is V120() & f2 is V121() )
; ( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )
( dom f1 = X & dom f2 = X )
by FUNCT_2:def 1;
then A2:
dom (f1 - f2) = X /\ X
by A1, Th23;
hence
f1 - f2 is Function of X,ExtREAL
by FUNCT_2:def 1; for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x)
thus
for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x)
by A2, MESFUNC1:def 4; verum