let A, e be Real; :: thesis: for f being PartFunc of REAL,REAL st f = A (#) (cos * (e (#) (id ([#] REAL)))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = - ((A * e) * (sin . (e * x))) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f = A (#) (cos * (e (#) (id ([#] REAL)))) implies ( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = - ((A * e) * (sin . (e * x))) ) ) )
assume AS1: f = A (#) (cos * (e (#) (id ([#] REAL)))) ; :: thesis: ( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = - ((A * e) * (sin . (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 (cos * E) = [#] REAL by FUNCT_2:def 1;
P6: dom (A (#) (cos * E)) = [#] REAL by FUNCT_2:def 1;
P7: for x being Real st x in Z holds
( cos * E is_differentiable_in x & diff ((cos * E),x) = - (e * (sin . (E . x))) )

proof

let x be Real; :: thesis: ( x in Z implies ( cos * E is_differentiable_in x & diff ((cos * E),x) = - (e * (sin . (E . x))) ) )
assume P70: x in Z ; :: thesis: ( cos * E is_differentiable_in x & diff ((cos * E),x) = - (e * (sin . (E . x))) )
then P71: E is_differentiable_in x by P4, FDIFF_1:9;
P73: ( cos is_differentiable_in E . x & diff (cos,(E . x)) = - (sin . (E . x)) ) by SIN_COS:63;
then diff ((cos * E),x) = (- (sin . (E . x))) * (diff (E,x)) by FDIFF_2:13, P71
.= (- (sin . (E . x))) * ((E `| Z) . x) by FDIFF_1:def 7, P4, P70
.= (- (sin . (E . x))) * e by P2, P3, FDIFF_1:23, P70
.= - (e * (sin . (E . x))) ;
hence ( cos * E is_differentiable_in x & diff ((cos * E),x) = - (e * (sin . (E . x))) ) by P73, FDIFF_2:13, P71; :: thesis: verum

end;

then for x being Real st x in Z holds
cos * E is_differentiable_in x ;
then P8: cos * E is_differentiable_on Z by P5, FDIFF_1:9;
for x being Real st x in Z holds
((A (#) (cos * E)) `| Z) . x = - ((A * e) * (sin . (e * x)))

proof

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