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:18;
reconsider l = (n + 1) - n as Element of NAT ;
A2: 0 + n < n + 1 by XREAL_1:8;
A3: n ! <> 0 by NEWTON:23;
A4: #Z 1 is_differentiable_on Z by Th8, FDIFF_1:34;
then A5: ((n + 1) ! ) (#) (#Z 1) is_differentiable_on Z by FDIFF_2:19;
Z c= dom (#Z 1) by A4, FDIFF_1:def 7;
then A6: 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:19, NEWTON:def 3
.= ((((((n + 1) ! ) / 1) (#) (#Z 1)) | Z) `| Z) . x by A3, XCMPLX_1:93
.= ((((n + 1) ! ) (#) (#Z 1)) `| Z) . x by A5, FDIFF_2:16
.= ((n + 1) ! ) * (diff (#Z 1),x) by A1, A4, A6, FDIFF_1:28
.= ((n + 1) ! ) * (1 * (x #Z (1 - 1))) by TAYLOR_1:2
.= ((n + 1) ! ) * 1 by PREPOWER:44
.= m ! ;
hence ((diff (#Z m),Z) . m) . x = m ! ; :: thesis: verum

end;

suppose A7: 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:72
.= x #Z 0 by TAYLOR_1:def 1
.= m ! by A7, NEWTON:18, PREPOWER:44 ;
hence ((diff (#Z m),Z) . m) . x = m ! ; :: thesis: verum

end;

end;