let x0, x 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 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 Th3, A1 ;
(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 Th6, A1 ;
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