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;
A3: (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 A3, FDIFF_1:def 8 ;
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))) ; :: thesis: verum

end;

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

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

end;

end;