let x be Real; :: thesis: for m being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((#Z m),Z)) . m) . x = m !
let m be Element of NAT ; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff ((#Z m),Z)) . m) . x = m !
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff ((#Z m),Z)) . m) . x = m ! )
assume A1: x in Z ; :: thesis: ((diff ((#Z m),Z)) . m) . x = m !

per cases ( m > 0 or m = 0 ) ;

suppose m > 0 ; :: thesis: ((diff ((#Z m),Z)) . m) . x = m !

then 0 < 0 + m ;
then 1 <= m by NAT_1:19;
then reconsider n = m - 1 as Element of NAT by INT_1:5;
A2: 0 + n < n + 1 by XREAL_1:6;
A3: #Z 1 is_differentiable_on Z by Th8, FDIFF_1:26;
then A4: ((n + 1) !) (#) (#Z 1) is_differentiable_on Z by FDIFF_2:19;
Z c= dom (#Z 1) by A3, FDIFF_1:def 6;
then A5: Z c= dom (((n + 1) !) (#) (#Z 1)) by VALUED_1:def 5;
((diff ((#Z m),Z)) . m) . x = (((diff ((#Z (n + 1)),Z)) . n) `| Z) . x by TAYLOR_1:def 5
.= ((((((n + 1) choose n) * (n !)) (#) (#Z ((n + 1) - n))) | Z) `| Z) . x by A2, Th32
.= (((((((n + 1) !) / ((n !) * 1)) * (n !)) (#) (#Z ((n + 1) - n))) | Z) `| Z) . x by A2, NEWTON:13, NEWTON:def 3
.= ((((((n + 1) !) / 1) (#) (#Z 1)) | Z) `| Z) . x by XCMPLX_1:92
.= ((((n + 1) !) (#) (#Z 1)) `| Z) . x by A4, FDIFF_2:16
.= ((n + 1) !) * (diff ((#Z 1),x)) by A1, A3, A5, FDIFF_1:20
.= ((n + 1) !) * (1 * (x #Z (1 - 1))) by TAYLOR_1:2
.= ((n + 1) !) * 1 by PREPOWER:34
.= m ! ;
hence ((diff ((#Z m),Z)) . m) . x = m ! ; :: thesis: verum

end;

suppose A6: m = 0 ; :: thesis: ((diff ((#Z m),Z)) . m) . x = m !

then ((diff ((#Z m),Z)) . m) . x = ((#Z 0) | Z) . x by TAYLOR_1:def 5
.= (#Z 0) . x by A1, FUNCT_1:49
.= x #Z 0 by TAYLOR_1:def 1
.= m ! by A6, NEWTON:12, PREPOWER:34 ;
hence ((diff ((#Z m),Z)) . m) . x = m ! ; :: thesis: verum

end;

end;