let x, r be Real; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( x in Z implies ((diff (r (#) sin ),Z) . n) . x = r * (sin . (x + ((n * PI ) / 2))) )
assume A1: x in Z ; :: thesis: ((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 ; :: thesis: ((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:18;
A5: (diff sin ,Z) . i is_differentiable_on Z by A2, TAYLOR_1:def 6;
dom ((diff sin ,Z) . n) = dom ((diff sin ,Z) . (i + 1))
.= dom (((diff sin ,Z) . i) `| Z) by TAYLOR_1:def 5
.= Z by A5, FDIFF_1:def 8 ;
then A8: 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 Th13, A2
.= r * (((diff sin ,Z) . n) . x) by A8, VALUED_1:def 5
.= r * (sin . (x + ((n * PI ) / 2))) by Th3, A1 ;
hence ((diff (r (#) sin ),Z) . n) . x = r * (sin . (x + ((n * PI ) / 2))) ; :: thesis: verum

end;

suppose A9: n = 0 ; :: thesis: ((diff (r (#) sin ),Z) . n) . x = r * (sin . (x + ((n * PI ) / 2)))

A10: dom (r (#) (sin | Z)) = dom (sin | Z) by VALUED_1:def 5
.= Z by LemX ;
((diff (r (#) sin ),Z) . n) . x = (r (#) ((diff sin ,Z) . 0 )) . x by A9, Th13, A2
.= (r (#) (sin | Z)) . x by TAYLOR_1:def 5
.= r * ((sin | Z) . x) by A10, A1, VALUED_1:def 5
.= r * (sin . (x + ((n * PI ) / 2))) by A9, A1, FUNCT_1:72 ;
hence ((diff (r (#) sin ),Z) . n) . x = r * (sin . (x + ((n * PI ) / 2))) ; :: thesis: verum

end;

end;