let A, e be Real; for f being PartFunc of REAL,REAL st f = A (#) (sin * (e (#) (id ([#] REAL)))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = (A * e) * (cos . (e * x)) ) )
let f be PartFunc of REAL,REAL; ( f = A (#) (sin * (e (#) (id ([#] REAL)))) implies ( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = (A * e) * (cos . (e * x)) ) ) )
assume AS1:
f = A (#) (sin * (e (#) (id ([#] REAL))))
; ( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = (A * e) * (cos . (e * x)) ) )
reconsider Z = [#] REAL as open Subset of REAL ;
reconsider E = e (#) (id ([#] REAL)) as Function of REAL,REAL ;
P2:
( [#] REAL = dom E & rng E c= [#] REAL )
by FUNCT_2:def 1;
P3:
for x being Real st x in Z holds
E . x = (e * x) + 0
P4:
( E is_differentiable_on Z & ( for x being Real st x in Z holds
(E `| Z) . x = e ) )
by P2, P3, FDIFF_1:23;
P5:
dom (sin * E) = [#] REAL
by FUNCT_2:def 1;
P6:
dom (A (#) (sin * E)) = [#] REAL
by FUNCT_2:def 1;
P7:
for x being Real st x in Z holds
( sin * E is_differentiable_in x & diff ((sin * E),x) = e * (cos . (E . x)) )
proof
let x be
Real;
( x in Z implies ( sin * E is_differentiable_in x & diff ((sin * E),x) = e * (cos . (E . x)) ) )
assume P70:
x in Z
;
( sin * E is_differentiable_in x & diff ((sin * E),x) = e * (cos . (E . x)) )
then P71:
E is_differentiable_in x
by P4, FDIFF_1:9;
P73:
(
sin is_differentiable_in E . x &
diff (
sin,
(E . x))
= cos . (E . x) )
by SIN_COS:64;
then diff (
(sin * E),
x) =
(cos . (E . x)) * (diff (E,x))
by FDIFF_2:13, P71
.=
(cos . (E . x)) * ((E `| Z) . x)
by FDIFF_1:def 7, P4, P70
.=
e * (cos . (E . x))
by P2, P3, FDIFF_1:23, P70
;
hence
(
sin * E is_differentiable_in x &
diff (
(sin * E),
x)
= e * (cos . (E . x)) )
by P73, FDIFF_2:13, P71;
verum
end;
then
for x being Real st x in Z holds
sin * E is_differentiable_in x
;
then P8:
sin * E is_differentiable_on Z
by P5, FDIFF_1:9;
for x being Real st x in Z holds
((A (#) (sin * E)) `| Z) . x = (A * e) * (cos . (e * x))
hence
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = (A * e) * (cos . (e * x)) ) )
by AS1, P8, P6, FDIFF_1:20; verum