let X be non empty set ; :: thesis: 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; :: thesis: ( 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() ) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum