let h be Function of REAL,REAL; :: thesis: ( h = f (#) g implies h is differentiable )
assume A3: h = f (#) g ; :: thesis: h is differentiable
let r be Real; :: according to POLYDIFF:def 2 :: thesis: h is_differentiable_in r
( f is_differentiable_in r & g is_differentiable_in r ) by Th9;
hence h is_differentiable_in r by A3, FDIFF_1:16; :: thesis: verum