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 that
A1: f is_differentiable_on X and
A2: g is_differentiable_on X ; :: thesis: ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )
reconsider Z = X as Subset of REAL by A1, FDIFF_1:15;
reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:17;
( X c= dom f & X c= dom g ) by A1, A2, FDIFF_1:def 7;
then A3: Z c= (dom f) /\ (dom g) by XBOOLE_1:19;
then A4: Z c= dom (f (#) g) by VALUED_1:def 4;
( Z c= dom (f + g) & Z c= dom (f - g) ) by A3, VALUED_1:12, VALUED_1:def 1;
hence ( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X ) by A1, A2, A4, FDIFF_1:26, FDIFF_1:27, FDIFF_1:29; :: thesis: verum