let x, a be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) )
assume A1: x in Z ; :: thesis: ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)
reconsider xx = x as Element of REAL by XREAL_0:def 1;

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

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

then 0 < 0 + n ;
then 1 <= n by NAT_1:19;
then reconsider m = n - 1 as Element of NAT by INT_1:5;
A2: dom (a (#) ((diff ((#Z n),Z)) . n)) = dom ((diff ((#Z n),Z)) . n) by VALUED_1:def 5;
#Z n is_differentiable_on n,Z by Th38;
then A3: (diff ((#Z n),Z)) . m is_differentiable_on Z ;
A4: dom ((diff ((#Z n),Z)) . n) = dom ((diff ((#Z n),Z)) . (m + 1))
.= dom (((diff ((#Z n),Z)) . m) `| Z) by TAYLOR_1:def 5
.= Z by A3, FDIFF_1:def 7 ;
((diff ((a (#) (#Z n)),Z)) . n) . x = (a (#) ((diff ((#Z n),Z)) . n)) . x by Th21, Th38
.= a * (((diff ((#Z n),Z)) . n) . x) by A1, A4, A2, VALUED_1:def 5
.= a * (n !) by A1, Th37 ;
hence ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) ; :: thesis: verum

end;

suppose A5: n = 0 ; :: thesis: ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)

dom (#Z 0) = REAL by FUNCT_2:def 1;
then A6: dom (a (#) (#Z 0)) = REAL by VALUED_1:def 5;
((diff ((a (#) (#Z n)),Z)) . n) . x = (a (#) ((diff ((#Z 0),Z)) . 0)) . x by A5, Th21, Th38
.= (a (#) ((#Z 0) | Z)) . x by TAYLOR_1:def 5
.= ((a (#) (#Z 0)) | Z) . x by RFUNCT_1:49
.= (a (#) (#Z 0)) . x by A1, FUNCT_1:49
.= a * ((#Z 0) . xx) by A6, VALUED_1:def 5
.= a * (x #Z 0) by TAYLOR_1:def 1
.= a * (n !) by A5, NEWTON:12, PREPOWER:34 ;
hence ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) ; :: thesis: verum

end;

end;