let x, x0 be Real; :: thesis: for n, m being Element of NAT
for Z being open Subset of REAL st x0 in Z & n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st x0 in Z & n > m holds
( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
let Z be open Subset of REAL; :: thesis: ( x0 in Z & n > m implies ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n ) )
assume that
A1: x0 in Z and
A2: n > m ; :: thesis: ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )
A3: (Taylor ((#Z n),Z,x0,x)) . n = ((((diff ((#Z n),Z)) . n) . x0) * ((x - x0) |^ n)) / (n !) by TAYLOR_1:def 7
.= (((x - x0) |^ n) * (n !)) / (n !) by A1, Th37
.= (x - x0) |^ n by XCMPLX_1:89 ;
(Taylor ((#Z n),Z,x0,x)) . m = ((((diff ((#Z n),Z)) . m) . x0) * ((x - x0) |^ m)) / (m !) by TAYLOR_1:def 7
.= ((((n choose m) * (m !)) * (x0 #Z (n - m))) * ((x - x0) |^ m)) / (m !) by A1, A2, Th36
.= (((n choose m) * ((x0 #Z (n - m)) * ((x - x0) |^ m))) * (m !)) / (m !)
.= ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) by XCMPLX_1:89 ;
hence ( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n ) by A3; :: thesis: verum