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 that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in f1 . x0 ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )
consider N2 being Neighbourhood of f1 . x0 such that
A3: N2 c= dom f2 by A2;
f1 is_continuous_in x0 by A1, FDIFF_1:24;
then consider N3 being Neighbourhood of x0 such that
A4: f1 .: N3 c= N2 by FCONT_1:5;
consider N1 being Neighbourhood of x0 such that
A5: N1 c= dom f1 by A1;
consider N being Neighbourhood of x0 such that
A6: N c= N1 and
A7: N c= N3 by RCOMP_1:17;
N c= dom (f2 * f1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom (f2 * f1) )
assume A8: x in N ; :: thesis: x in dom (f2 * f1)
then reconsider x9 = x as Real ;
A9: x in N1 by A6, A8;
then f1 . x9 in f1 .: N3 by A5, A7, A8, FUNCT_1:def 6;
then f1 . x9 in N2 by A4;
hence x in dom (f2 * f1) by A5, A3, A9, FUNCT_1:11; :: thesis: verum
end;
hence ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) ) by A1, A2, Lm2; :: thesis: verum