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:8;
reconsider Z = Z as open Subset of REAL by A1, FDIFF_1:10;
( X c= dom f & X c= dom g ) by A1, A2;
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:18, FDIFF_1:19, FDIFF_1:21; :: thesis: verum