let x, r be Real; :: thesis: for n being Element of NAT st r > 0 holds
( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
let n be Element of NAT ; :: thesis: ( r > 0 implies ( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) ) )
A1: |.(0 - 0).| = 0 by ABSVALUE:2;
assume r > 0 ; :: thesis: ( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )
then A2: 0 in ].(0 - r),(0 + r).[ by A1, RCOMP_1:1;
A3: (Maclaurin (cos,].(- r),r.[,x)) . n = (Taylor (cos,].(- r),r.[,0,x)) . n by TAYLOR_2:def 1
.= ((((diff (cos,].(- r),r.[)) . n) . 0) * ((x - 0) |^ n)) / (n !) by TAYLOR_1:def 7
.= ((cos . (0 + ((n * PI) / 2))) * (x |^ n)) / (n !) by A2, Th14 ;
(Maclaurin (sin,].(- r),r.[,x)) . n = (Taylor (sin,].(- r),r.[,0,x)) . n by TAYLOR_2:def 1
.= ((((diff (sin,].(- r),r.[)) . n) . 0) * ((x - 0) |^ n)) / (n !) by TAYLOR_1:def 7
.= ((sin . (0 + ((n * PI) / 2))) * (x |^ n)) / (n !) by A2, Th11 ;
hence ( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) ) by A3; :: thesis: verum