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 2, [#] REAL & ( for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 ) ) )
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 2, [#] REAL & ( for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 ) ) ) )
assume AS1: for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ; :: thesis: ( f is_differentiable_on 2, [#] REAL & ( for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 ) ) )
then P1: ( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) ) by LM412;
P2: for x being Real holds (f `| ([#] REAL)) . x = ((e * B) * (cos . (e * x))) + ((- (e * A)) * (sin . (e * x)))

proof

let x be Real; :: thesis: (f `| ([#] REAL)) . x = ((e * B) * (cos . (e * x))) + ((- (e * A)) * (sin . (e * x)))
thus (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) by AS1, LM412
.= ((e * B) * (cos . (e * x))) + ((- (e * A)) * (sin . (e * x))) ; :: thesis: verum

end;

P4: rng (f `| ([#] REAL)) c= REAL ;
D0: dom f = REAL by FUNCT_2:def 1;
dom (f `| ([#] REAL)) = [#] REAL by FDIFF_1:def 7, P1;
then P30: f `| ([#] REAL) is Function of REAL,REAL by P4, FUNCT_2:2;
X1: for i being Nat st i <= 2 - 1 holds
(diff (f,([#] REAL))) . i is_differentiable_on [#] REAL

proof

let i be Nat; :: thesis: ( i <= 2 - 1 implies (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL )
assume i <= 2 - 1 ; :: thesis: (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL
then i <= 0 + 1 ;

per cases then ( i = 0 or i = 1 ) by NAT_1:8;

suppose i = 0 ; :: thesis: (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL

then (diff (f,([#] REAL))) . i = f | ([#] REAL) by TAYLOR_1:def 5
.= f by D0, RELAT_1:69 ;
hence (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL by AS1, LM412; :: thesis: verum

end;

suppose i = 1 ; :: thesis: (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL

then (diff (f,([#] REAL))) . i = (diff (f,([#] REAL))) . (0 + 1)
.= ((diff (f,([#] REAL))) . 0) `| ([#] REAL) by TAYLOR_1:def 5
.= (f | ([#] REAL)) `| ([#] REAL) by TAYLOR_1:def 5
.= f `| ([#] REAL) by D0, RELAT_1:69 ;
hence (diff (f,([#] REAL))) . i is_differentiable_on [#] REAL by P30, LM412, P2; :: thesis: verum

end;

end;

end;

hence f is_differentiable_on 2, [#] REAL ; :: thesis: for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 )
let x be Real; :: thesis: ( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 )
thus (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) by AS1, LM412; :: thesis: ( ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 )
thus P90: ((f `| ([#] REAL)) `| ([#] REAL)) . x = - (e * (((e * B) * (sin . (e * x))) - ((- (e * A)) * (cos . (e * x))))) by P30, LM412, P2
.= - ((e * e) * ((A * (cos . (e * x))) + (B * (sin . (e * x)))))
.= - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) by SQUARE_1:def 1 ; :: thesis: (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0
P92: (diff (f,([#] REAL))) . (1 + 1) = ((diff (f,([#] REAL))) . 1) `| ([#] REAL) by TAYLOR_1:def 5;
P93: (diff (f,([#] REAL))) . 1 = (diff (f,([#] REAL))) . (0 + 1)
.= ((diff (f,([#] REAL))) . 0) `| ([#] REAL) by TAYLOR_1:def 5
.= (f | ([#] REAL)) `| ([#] REAL) by TAYLOR_1:def 5
.= f `| ([#] REAL) by D0, RELAT_1:69 ;
(diff (f,([#] REAL))) . 1 is_differentiable_on [#] REAL by X1;
then dom ((diff (f,([#] REAL))) . 2) = [#] REAL by P92, FDIFF_1:def 7;
then P91: ((diff (f,([#] REAL))) . 2) /. x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) by XREAL_0:def 1, PARTFUN1:def 6, P92, P93, P90;
f /. x = f . x by D0, XREAL_0:def 1, PARTFUN1:def 6;
then (e ^2) * (f /. x) = (e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x)))) by AS1;
hence (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 by P91; :: thesis: verum