let r, x 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 ! ) ) )
assume A1: 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 ! ) )
abs (0 - 0 ) = 0 by ABSVALUE:7;
then A3: 0 in ].(0 - r),(0 + r).[ by A1, RCOMP_1:8;
A4: (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 Th3, 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 Th6, A3 ;
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 A4; :: thesis: verum