let x, r be Real; for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))
let n be Element of NAT ; for Z being open Subset of REAL st x in Z holds
((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))
let Z be open Subset of REAL; ( x in Z implies ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) )
assume A1:
x in Z
; ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))
A2:
sin is_differentiable_on n,Z
by TAYLOR_2:21;
per cases
( n > 0 or n = 0 )
;
suppose
n > 0
;
((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))then
0 < 0 + n
;
then
1
<= n
by NAT_1:19;
then reconsider i =
n - 1 as
Element of
NAT by INT_1:5;
A3:
(diff (sin,Z)) . i is_differentiable_on Z
by A2;
dom ((diff (sin,Z)) . n) =
dom ((diff (sin,Z)) . (i + 1))
.=
dom (((diff (sin,Z)) . i) `| Z)
by TAYLOR_1:def 5
.=
Z
by A3, FDIFF_1:def 7
;
then A4:
x in dom (r (#) ((diff (sin,Z)) . n))
by A1, VALUED_1:def 5;
((diff ((r (#) sin),Z)) . n) . x =
(r (#) ((diff (sin,Z)) . n)) . x
by A2, Th21
.=
r * (((diff (sin,Z)) . n) . x)
by A4, VALUED_1:def 5
.=
r * (sin . (x + ((n * PI) / 2)))
by A1, Th11
;
hence
((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))
;
verum end; end;