theorem Th47: :: ORDEQ_01:47

for a being Real
for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )