let a be Real; :: thesis: 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 !) )
let n be Nat; :: thesis: 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 !) )
let g be Function of REAL,REAL; :: thesis: ( ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) implies for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) ) )
A1: dom g = REAL by FUNCT_2:def 1;
assume A2: for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ; :: thesis: for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = In ((($1 - a) |^ (n + 1)),REAL);
consider f being PartFunc of REAL,REAL such that
A3: for d being Element of REAL holds
( d in dom f iff S₁[d] ) and
A4: for d being Element of REAL st d in dom f holds
f /. d = H₁(d) from PARTFUN2:sch 2();
for x being object st x in REAL holds
x in dom f by A3;
then REAL c= dom f by TARSKI:def 3;
then A5: dom f = REAL by XBOOLE_0:def 10;
A6: for d being Real holds f . d = (d - a) |^ (n + 1)

proof

let d be Real; :: thesis: f . d = (d - a) |^ (n + 1)
A7: d in REAL by XREAL_0:def 1;
f /. d = In (((d - a) |^ (n + 1)),REAL) by A4, A5, A7;
hence f . d = (d - a) |^ (n + 1) by A5, PARTFUN1:def 6, A7; :: thesis: verum

end;

A8: f is Function of REAL,REAL by A5, FUNCT_2:67;
A9: dom ((1 / ((n + 1) !)) (#) f) = dom f by VALUED_1:def 5;

A10: now :: thesis: for x being Element of REAL st x in dom ((1 / ((n + 1) !)) (#) f) holds
((1 / ((n + 1) !)) (#) f) . x = g . x

let x be Element of REAL ; :: thesis: ( x in dom ((1 / ((n + 1) !)) (#) f) implies ((1 / ((n + 1) !)) (#) f) . x = g . x )
assume x in dom ((1 / ((n + 1) !)) (#) f) ; :: thesis: ((1 / ((n + 1) !)) (#) f) . x = g . x
hence ((1 / ((n + 1) !)) (#) f) . x = (1 / ((n + 1) !)) * (f . x) by VALUED_1:def 5
.= (1 / ((n + 1) !)) * ((x - a) |^ (n + 1)) by A6
.= (((x - a) |^ (n + 1)) / ((n + 1) !)) * 1 by XCMPLX_1:75
.= g . x by A2 ;
:: thesis: verum

end;

A11: for x being Real holds
( (1 / ((n + 1) !)) (#) f is_differentiable_in x & diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !) )

proof

let x be Real; :: thesis: ( (1 / ((n + 1) !)) (#) f is_differentiable_in x & diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !) )
A12: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15
.= 1 / (n !) by XCMPLX_1:91 ;
A13: f is_differentiable_in x by A8, A6, Th46;
hence (1 / ((n + 1) !)) (#) f is_differentiable_in x by FDIFF_1:15; :: thesis: diff (((1 / ((n + 1) !)) (#) f),x) = ((x - a) |^ n) / (n !)
thus diff (((1 / ((n + 1) !)) (#) f),x) = (1 / ((n + 1) !)) * (diff (f,x)) by A13, FDIFF_1:15
.= ((diff (f,x)) / ((n + 1) !)) * 1 by XCMPLX_1:75
.= (1 * ((n + 1) * ((x - a) |^ n))) / ((n + 1) !) by A8, A6, Th46
.= 1 * (((x - a) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74
.= ((x - a) |^ n) / (n !) by A12, XCMPLX_1:99 ; :: thesis: verum

end;

(1 / ((n + 1) !)) (#) f = g by A10, PARTFUN1:5, A1, A5, A9;
hence for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) ) by A11; :: thesis: verum