let x, x0 be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL st x0 in Z holds
( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st x0 in Z holds
( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )
let Z be open Subset of REAL; :: thesis: ( x0 in Z implies ( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) ) )
assume A1: x0 in Z ; :: thesis: ( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )
A2: (Taylor (cos,Z,x0,x)) . n = ((((diff (cos,Z)) . n) . x0) * ((x - x0) |^ n)) / (n !) by TAYLOR_1:def 7
.= ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) by A1, Th14 ;
(Taylor (sin,Z,x0,x)) . n = ((((diff (sin,Z)) . n) . x0) * ((x - x0) |^ n)) / (n !) by TAYLOR_1:def 7
.= ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) by A1, Th11 ;
hence ( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) ) by A2; :: thesis: verum