let A, e be Real; :: thesis: 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; :: thesis: ( 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)))) ; :: thesis: ( 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

proof

let x be Real; :: thesis: ( x in Z implies E . x = (e * x) + 0 )
assume AS2: x in Z ; :: thesis: E . x = (e * x) + 0
hence E . x = e * ((id ([#] REAL)) . x) by VALUED_1:def 5, P2
.= (e * x) + 0 by AS2, FUNCT_1:18 ;
:: thesis: verum

end;

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; :: thesis: ( x in Z implies ( sin * E is_differentiable_in x & diff ((sin * E),x) = e * (cos . (E . x)) ) )
assume P70: x in Z ; :: thesis: ( 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; :: thesis: 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))

proof

let x be Real; :: thesis: ( x in Z implies ((A (#) (sin * E)) `| Z) . x = (A * e) * (cos . (e * x)) )
assume P90: x in Z ; :: thesis: ((A (#) (sin * E)) `| Z) . x = (A * e) * (cos . (e * x))
then P91: E . x = (e * x) + 0 by P3;
thus ((A (#) (sin * E)) `| Z) . x = A * (diff ((sin * E),x)) by P90, P8, P6, FDIFF_1:20
.= A * (e * (cos . (E . x))) by P7, P90
.= (A * e) * (cos . (e * x)) by P91 ; :: thesis: verum

end;

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; :: thesis: verum