let X be set ; :: thesis: for f, g being PartFunc of REAL , REAL st f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )
let f, g be PartFunc of REAL , REAL ; :: thesis: ( f is_differentiable_on X & g is_differentiable_on X implies ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) )
assume A1: ( f is_differentiable_on X & g is_differentiable_on X ) ; :: thesis: ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )
then reconsider Z = X as Subset of REAL by FDIFF_1:15;
reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:17;
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) & X c= dom g & ( for x being Real st x in X holds
g | X is_differentiable_in x ) ) by A1, FDIFF_1:def 7;
then Z c= (dom f) /\ (dom g) by XBOOLE_1:19;
then ( Z c= dom (f + g) & Z c= dom (f - g) & Z c= dom (f (#) g) ) by VALUED_1:12, VALUED_1:def 1, VALUED_1:def 4;
hence ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) by A1, FDIFF_1:26, FDIFF_1:27, FDIFF_1:29; :: thesis: verum