let A be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A holds
( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A implies ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) ) )
assume that
A1: f1 is_differentiable_on A and
A2: f1 .: A is open Subset of REAL and
A3: f2 is_differentiable_on f1 .: A ; :: thesis: ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )
A4: A c= dom f1 by A1;

A5: now :: thesis: for x0 being Real st x0 in A holds
( f1 is_differentiable_in x0 & x0 in dom f1 & f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )

let x0 be Real; :: thesis: ( x0 in A implies ( f1 is_differentiable_in x0 & x0 in dom f1 & f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 ) )
assume A6: x0 in A ; :: thesis: ( f1 is_differentiable_in x0 & x0 in dom f1 & f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
hence A7: f1 is_differentiable_in x0 by A1, FDIFF_1:9; :: thesis: ( x0 in dom f1 & f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
thus x0 in dom f1 by A4, A6; :: thesis: ( f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
thus f1 . x0 in f1 .: A by A4, A6, FUNCT_1:def 6; :: thesis: ( f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
hence f2 is_differentiable_in f1 . x0 by A2, A3, FDIFF_1:9; :: thesis: f2 * f1 is_differentiable_in x0
hence f2 * f1 is_differentiable_in x0 by A7, Th13; :: thesis: verum

end;

f1 .: A c= dom f2 by A3;
then A8: A c= dom (f2 * f1) by A4, FUNCT_3:3;
for x0 being Real st x0 in A holds
f2 * f1 is_differentiable_in x0 by A5;
hence A9: f2 * f1 is_differentiable_on A by A8, FDIFF_1:9; :: thesis: (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)
then A10: dom ((f2 * f1) `| A) = A by FDIFF_1:def 7;

A11: now :: thesis: for x0 being Element of REAL st x0 in dom ((f2 * f1) `| A) holds
((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in dom ((f2 * f1) `| A) implies ((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0 )
assume A12: x0 in dom ((f2 * f1) `| A) ; :: thesis: ((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0
then A13: f1 is_differentiable_in x0 by A5, A10;
A14: x0 in dom f1 by A5, A10, A12;
A15: f1 . x0 in f1 .: A by A5, A10, A12;
A16: f2 is_differentiable_in f1 . x0 by A5, A10, A12;
thus ((f2 * f1) `| A) . x0 = diff ((f2 * f1),x0) by A9, A10, A12, FDIFF_1:def 7
.= (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A13, A16, Th13
.= (diff (f2,(f1 . x0))) * ((f1 `| A) . x0) by A1, A10, A12, FDIFF_1:def 7
.= ((f2 `| (f1 .: A)) . (f1 . x0)) * ((f1 `| A) . x0) by A3, A15, FDIFF_1:def 7
.= (((f2 `| (f1 .: A)) * f1) . x0) * ((f1 `| A) . x0) by A14, FUNCT_1:13
.= (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0 by VALUED_1:5 ; :: thesis: verum

end;

dom (f2 `| (f1 .: A)) = f1 .: A by A3, FDIFF_1:def 7;
then A c= dom ((f2 `| (f1 .: A)) * f1) by A4, FUNCT_1:101;
then dom ((f2 * f1) `| A) = (dom ((f2 `| (f1 .: A)) * f1)) /\ A by A10, XBOOLE_1:28
.= (dom ((f2 `| (f1 .: A)) * f1)) /\ (dom (f1 `| A)) by A1, FDIFF_1:def 7
.= dom (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) by VALUED_1:def 4 ;
hence (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) by A11, PARTFUN1:5; :: thesis: verum