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) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )