let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 implies ( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) ) )
assume A1: ( f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 ) ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) )
then consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f1 by Th11;
consider N2 being Neighbourhood of f1 . x0 such that
A3: N2 c= dom f2 by A1, Th11;
f1 is_continuous_in x0 by A1, FDIFF_1:32;
then consider N3 being Neighbourhood of x0 such that
A4: f1 .: N3 c= N2 by FCONT_1:5;
consider N being Neighbourhood of x0 such that
A5: ( N c= N1 & N c= N3 ) by RCOMP_1:38;
N c= dom (f2 * f1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom (f2 * f1) )
assume A6: x in N ; :: thesis: x in dom (f2 * f1)
then A7: x in N1 by A5;
reconsider x' = x as Real by A6;
f1 . x' in f1 .: N3 by A2, A5, A6, A7, FUNCT_1:def 12;
then f1 . x' in N2 by A4;
hence x in dom (f2 * f1) by A2, A3, A7, FUNCT_1:21; :: thesis: verum

end;

hence ( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 . x0)) * (diff f1,x0) ) by A1, Lm2; :: thesis: verum