let A, B be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & rng (f1 | A) c= B & f2 is_differentiable_on B holds
( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A) )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_differentiable_on A & rng (f1 | A) c= B & f2 is_differentiable_on B implies ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A) ) )
assume that
A1:
f1 is_differentiable_on A
and
A2:
rng (f1 | A) c= B
and
A3:
f2 is_differentiable_on B
; ( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A) )
A4:
now 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;
( 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
;
( 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:9;
( 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 A1, A5;
( f1 . x0 in f1 .: A & f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )thus
f1 . x0 in f1 .: A
by A1, A5, FUNCT_1:def 6;
( f2 is_differentiable_in f1 . x0 & f2 * f1 is_differentiable_in x0 )
x0 in dom (f1 | A)
by A1, A5, RELAT_1:57;
then
(f1 | A) . x0 in B
by A2, FUNCT_1:3;
then
f1 . x0 in B
by A5, FUNCT_1:49;
hence
f2 is_differentiable_in f1 . x0
by A3, FDIFF_1:9;
f2 * f1 is_differentiable_in x0hence
f2 * f1 is_differentiable_in x0
by A6, FDIFF_2:13;
verum end;
then A9:
f1 .: A c= B
;
B c= dom f2
by A3;
then
f1 .: A c= dom f2
by A7;
then A10:
A c= dom (f2 * f1)
by A1, FUNCT_3:3;
for x0 being Real st x0 in A holds
f2 * f1 is_differentiable_in x0
by A4;
hence A11:
f2 * f1 is_differentiable_on A
by A10, FDIFF_1:9; (f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A)
then A12:
dom ((f2 * f1) `| A) = A
by FDIFF_1:def 7;
A13:
now for x0 being Element of REAL st x0 in dom ((f2 * f1) `| A) holds
((f2 * f1) `| A) . x0 = (((f2 `| B) * f1) (#) (f1 `| A)) . x0let x0 be
Element of
REAL ;
( x0 in dom ((f2 * f1) `| A) implies ((f2 * f1) `| A) . x0 = (((f2 `| B) * f1) (#) (f1 `| A)) . x0 )assume A14:
x0 in dom ((f2 * f1) `| A)
;
((f2 * f1) `| A) . x0 = (((f2 `| B) * f1) (#) (f1 `| A)) . x0then A15:
f1 is_differentiable_in x0
by A4, A12;
A16:
x0 in dom f1
by A4, A12, A14;
f1 . x0 in f1 .: A
by A4, A12, A14;
then A17:
f1 . x0 in B
by A7;
A18:
f2 is_differentiable_in f1 . x0
by A4, A12, A14;
thus ((f2 * f1) `| A) . x0 =
diff (
(f2 * f1),
x0)
by A11, A12, A14, FDIFF_1:def 7
.=
(diff (f2,(f1 . x0))) * (diff (f1,x0))
by A15, A18, FDIFF_2:13
.=
(diff (f2,(f1 . x0))) * ((f1 `| A) . x0)
by A1, A12, A14, FDIFF_1:def 7
.=
((f2 `| B) . (f1 . x0)) * ((f1 `| A) . x0)
by A3, A17, FDIFF_1:def 7
.=
(((f2 `| B) * f1) . x0) * ((f1 `| A) . x0)
by A16, FUNCT_1:13
.=
(((f2 `| B) * f1) (#) (f1 `| A)) . x0
by VALUED_1:5
;
verum end;
dom (f2 `| B) = B
by A3, FDIFF_1:def 7;
then dom ((f2 * f1) `| A) =
(dom ((f2 `| B) * f1)) /\ A
by A12, A1, A9, FUNCT_1:101, XBOOLE_1:28
.=
(dom ((f2 `| B) * f1)) /\ (dom (f1 `| A))
by A1, FDIFF_1:def 7
.=
dom (((f2 `| B) * f1) (#) (f1 `| A))
by VALUED_1:def 4
;
hence
(f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A)
by A13, PARTFUN1:5; verum