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))
dom (#Z (n - m)) = REAL by FUNCT_2:def 1;
then A3: dom (((n choose m) * (m !)) (#) (#Z (n - m))) = REAL by VALUED_1:def 5;
A4: dom ((diff ((#Z n),Z)) . m) = dom ((((n choose m) * (m !)) (#) (#Z (n - m))) | Z) by A2, Th32
.= REAL /\ Z by A3, RELAT_1:61
.= Z by XBOOLE_1:28 ;
A5: dom (a (#) ((diff ((#Z n),Z)) . m)) = dom ((diff ((#Z n),Z)) . m) by VALUED_1:def 5;
#Z n is_differentiable_on m,Z by A2, Th38, TAYLOR_1:23;
then ((diff ((a (#) (#Z n)),Z)) . m) . x = (a (#) ((diff ((#Z n),Z)) . m)) . x by Th21
.= a * (((diff ((#Z n),Z)) . m) . x) by A1, A4, A5, VALUED_1:def 5
.= a * (((n choose m) * (m !)) * (x #Z (n - m))) by A1, A2, Th36 ;
hence ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) ; :: thesis: verum