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 ! )

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:18;
#Z n is_differentiable_on n,Z by Th29;
then A4: (diff (#Z n),Z) . m is_differentiable_on Z by TAYLOR_1:def 6;
A6: 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 A4, FDIFF_1:def 8 ;
A7: dom (a (#) ((diff (#Z n),Z) . n)) = dom ((diff (#Z n),Z) . n) by VALUED_1:def 5;
((diff (a (#) (#Z n)),Z) . n) . x = (a (#) ((diff (#Z n),Z) . n)) . x by Th13, Th29
.= a * (((diff (#Z n),Z) . n) . x) by A6, A1, A7, VALUED_1:def 5
.= a * (n ! ) by Th28, A1 ;
hence ((diff (a (#) (#Z n)),Z) . n) . x = a * (n ! ) ; :: thesis: verum

end;

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

dom (#Z 0 ) = REAL by FUNCT_2:def 1;
then A12: 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 A9, Th13, Th29
.= (a (#) ((#Z 0 ) | Z)) . x by TAYLOR_1:def 5
.= ((a (#) (#Z 0 )) | Z) . x by RFUNCT_1:65
.= (a (#) (#Z 0 )) . x by A1, FUNCT_1:72
.= a * ((#Z 0 ) . x) by A12, VALUED_1:def 5
.= a * (x #Z 0 ) by TAYLOR_1:def 1
.= a * (n ! ) by A9, NEWTON:18, PREPOWER:44 ;
hence ((diff (a (#) (#Z n)),Z) . n) . x = a * (n ! ) ; :: thesis: verum

end;

end;