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 (#) cos),Z)) . n) . x = r * (cos . (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 (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2)))
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) )
assume A1: x in Z ; :: thesis: ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2)))
A2: cos is_differentiable_on n,Z by TAYLOR_2:21;

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (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 (cos,Z)) . i is_differentiable_on Z by A2;
dom ((diff (cos,Z)) . n) = dom ((diff (cos,Z)) . (i + 1))
.= dom (((diff (cos,Z)) . i) `| Z) by TAYLOR_1:def 5
.= Z by A3, FDIFF_1:def 7 ;
then A4: x in dom (r (#) ((diff (cos,Z)) . n)) by A1, VALUED_1:def 5;
((diff ((r (#) cos),Z)) . n) . x = (r (#) ((diff (cos,Z)) . n)) . x by A2, Th21
.= r * (((diff (cos,Z)) . n) . x) by A4, VALUED_1:def 5
.= r * (cos . (x + ((n * PI) / 2))) by A1, Th14 ;
hence ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) ; :: thesis: verum

end;

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

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

end;

end;