let A, B, e be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) holds
( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) )
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) implies ( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) ) )
assume AS1: for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ; :: thesis: ( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) )
reconsider f1 = A (#) (cos * (e (#) (id ([#] REAL)))), f2 = B (#) (sin * (e (#) (id ([#] REAL)))) as PartFunc of REAL,REAL ;
reconsider Z = [#] REAL as open Subset of REAL ;
reconsider E = e (#) (id ([#] REAL)) as Function of REAL,REAL ;
P00: ( [#] REAL = dom E & rng E c= [#] REAL ) by FUNCT_2:def 1;
E01: for x being Real st x in Z holds
E . x = e * x

proof

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

end;

P4: dom (f1 + f2) = Z by FUNCT_2:def 1;
P01: dom f1 = Z by FUNCT_2:def 1;
dom f2 = Z by FUNCT_2:def 1;
then P6: dom f = (dom f1) /\ (dom f2) by FUNCT_2:def 1, P01;
for x being object st x in dom f holds
f . x = (f1 . x) + (f2 . x)

proof

let x be object ; :: thesis: ( x in dom f implies f . x = (f1 . x) + (f2 . x) )
assume P50: x in dom f ; :: thesis: f . x = (f1 . x) + (f2 . x)
then reconsider r = x as Real ;
thus f . x = (A * (cos . (e * r))) + (B * (sin . (e * r))) by AS1
.= (A * (cos . (E . r))) + (B * (sin . (e * r))) by E01, P50
.= (A * (cos . (E . r))) + (B * (sin . (E . r))) by E01, P50
.= (A * ((cos * E) . r)) + (B * (sin . (E . r))) by FUNCT_1:13, P50, P00
.= (A * ((cos * E) . r)) + (B * ((sin * E) . r)) by FUNCT_1:13, P50, P00
.= (f1 . r) + (B * ((sin * E) . r)) by VALUED_1:6
.= (f1 . x) + (f2 . x) by VALUED_1:6 ; :: thesis: verum

end;

then P1: f = f1 + f2 by P6, VALUED_1:def 1;
P2: ( f1 is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f1 `| ([#] REAL)) . x = - ((A * e) * (sin . (e * x))) ) ) by LM410;
P3: ( f2 is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f2 `| ([#] REAL)) . x = (B * e) * (cos . (e * x)) ) ) by LM411;
for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x)))))

proof

let x be Real; :: thesis: (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x)))))
P60: x in Z by XREAL_0:def 1;
(f `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by XREAL_0:def 1, FDIFF_1:18, P1, P2, P3, P4
.= ((f1 `| ([#] REAL)) . x) + (diff (f2,x)) by P2, P60, FDIFF_1:def 7
.= ((f1 `| ([#] REAL)) . x) + ((f2 `| ([#] REAL)) . x) by P3, P60, FDIFF_1:def 7
.= (- ((e * A) * (sin . (e * x)))) + ((f2 `| ([#] REAL)) . x) by LM410, XREAL_0:def 1
.= (- (e * (A * (sin . (e * x))))) + ((B * e) * (cos . (e * x))) by LM411, XREAL_0:def 1
.= - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ;
hence (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ; :: thesis: verum

end;

hence ( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) ) by FDIFF_1:18, P1, P2, P3, P4; :: thesis: verum