let x, a be Real; :: thesis: for n, m being Element of NAT
for Z being open Subset of REAL st x in Z & n > m holds
((diff (a (#) (#Z n)),Z) . m) . x = ((a * (n choose m)) * (m ! )) * (x #Z (n - m))
let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st x in Z & n > m holds
((diff (a (#) (#Z n)),Z) . m) . x = ((a * (n choose m)) * (m ! )) * (x #Z (n - m))
let Z be open Subset of REAL ; :: thesis: ( x in Z & n > m implies ((diff (a (#) (#Z n)),Z) . m) . x = ((a * (n choose m)) * (m ! )) * (x #Z (n - m)) )
assume that
A1: x in Z and
A2: n > m ; :: thesis: ((diff (a (#) (#Z n)),Z) . m) . x = ((a * (n choose m)) * (m ! )) * (x #Z (n - m))
A3: #Z n is_differentiable_on m,Z by A2, Th29, TAYLOR_1:23;
dom (#Z (n - m)) = REAL by FUNCT_2:def 1;
then A5: dom (((n choose m) * (m ! )) (#) (#Z (n - m))) = REAL by VALUED_1:def 5;
A9: dom ((diff (#Z n),Z) . m) = dom ((((n choose m) * (m ! )) (#) (#Z (n - m))) | Z) by Th23, A2
.= REAL /\ Z by A5, RELAT_1:90
.= Z by XBOOLE_1:28 ;
A10: dom (a (#) ((diff (#Z n),Z) . m)) = dom ((diff (#Z n),Z) . m) by VALUED_1:def 5;
((diff (a (#) (#Z n)),Z) . m) . x = (a (#) ((diff (#Z n),Z) . m)) . x by Th13, A3
.= a * (((diff (#Z n),Z) . m) . x) by A9, A1, A10, VALUED_1:def 5
.= a * (((n choose m) * (m ! )) * (x #Z (n - m))) by A1, A2, Th27 ;
hence ((diff (a (#) (#Z n)),Z) . m) . x = ((a * (n choose m)) * (m ! )) * (x #Z (n - m)) ; :: thesis: verum