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 A1: ( f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A ) ; :: thesis: ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )
then A2: A c= dom f1 by FDIFF_1:16;
f1 .: A c= dom f2 by A1, FDIFF_1:16;
then A3: A c= dom (f2 * f1) by A2, FUNCT_3:3;

A4: now

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 A5: 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 A6: f1 is_differentiable_in x0 by A1, FDIFF_1:16; :: 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 A2, A5; :: 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 A2, A5, FUNCT_1:def 12; :: thesis: ( f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
hence f2 is_differentiable_in f1 . x0 by A1, FDIFF_1:16; :: thesis: f2 * f1 is_differentiable_in x0
hence f2 * f1 is_differentiable_in x0 by A6, Th13; :: thesis: verum

end;

then for x0 being Real st x0 in A holds
f2 * f1 is_differentiable_in x0 ;
hence A7: f2 * f1 is_differentiable_on A by A3, FDIFF_1:16; :: thesis: (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)
then A8: dom ((f2 * f1) `| A) = A by FDIFF_1:def 8;
dom (f2 `| (f1 .: A)) = f1 .: A by A1, FDIFF_1:def 8;
then A c= dom ((f2 `| (f1 .: A)) * f1) by A2, FUNCT_1:171;
then A9: dom ((f2 * f1) `| A) = (dom ((f2 `| (f1 .: A)) * f1)) /\ A by A8, XBOOLE_1:28
.= (dom ((f2 `| (f1 .: A)) * f1)) /\ (dom (f1 `| A)) by A1, FDIFF_1:def 8
.= dom (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) by VALUED_1:def 4 ;

now

let x0 be Real; :: thesis: ( x0 in dom ((f2 * f1) `| A) implies ((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0 )
assume A10: x0 in dom ((f2 * f1) `| A) ; :: thesis: ((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0
then A11: ( f1 is_differentiable_in x0 & f1 . x0 in f1 .: A & x0 in dom f1 & f2 is_differentiable_in f1 . x0 ) by A4, A8;
thus ((f2 * f1) `| A) . x0 = diff (f2 * f1),x0 by A7, A8, A10, FDIFF_1:def 8
.= (diff f2,(f1 . x0)) * (diff f1,x0) by A11, Th13
.= (diff f2,(f1 . x0)) * ((f1 `| A) . x0) by A1, A8, A10, FDIFF_1:def 8
.= ((f2 `| (f1 .: A)) . (f1 . x0)) * ((f1 `| A) . x0) by A1, A11, FDIFF_1:def 8
.= (((f2 `| (f1 .: A)) * f1) . x0) * ((f1 `| A) . x0) by A11, FUNCT_1:23
.= (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0 by VALUED_1:5 ; :: thesis: verum

end;

hence (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) by A9, PARTFUN1:34; :: thesis: verum