let A be open Subset of REAL; 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; ( 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
; ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )
A4:
A c= dom f1
by A1;
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; (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)
then A10:
dom ((f2 * f1) `| A) = A
by FDIFF_1:def 7;
A11:
now for x0 being Element of REAL st x0 in dom ((f2 * f1) `| A) holds
((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0let x0 be
Element of
REAL ;
( 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)
;
((f2 * f1) `| A) . x0 = (((f2 `| (f1 .: A)) * f1) (#) (f1 `| A)) . x0then 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
;
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; verum