theorem Th41: :: HFDIFF_1:41

for x, x0 being Real
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 )