let x be Real; :: thesis: for n, m being Element of NAT
for Z being open Subset of REAL st n > m & x in Z holds
((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))
let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st n > m & x in Z holds
((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))
let Z be open Subset of REAL; :: thesis: ( n > m & x in Z implies ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) )
assume that
A1: n > m and
A2: x in Z ; :: thesis: ((diff ((#Z n),Z)) . m) . x = ((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;
then A4: dom ((((n choose m) * (m !)) (#) (#Z (n - m))) | Z) = REAL /\ Z by RELAT_1:61
.= Z by XBOOLE_1:28 ;
reconsider xx = x as Element of REAL by XREAL_0:def 1;
((diff ((#Z n),Z)) . m) . x = ((((n choose m) * (m !)) (#) (#Z (n - m))) | Z) . x by A1, Th32
.= (((n choose m) * (m !)) (#) (#Z (n - m))) . x by A2, A4, FUNCT_1:47
.= ((n choose m) * (m !)) * ((#Z (n - m)) . xx) by A3, VALUED_1:def 5
.= ((n choose m) * (m !)) * (x #Z (n - m)) by TAYLOR_1:def 1 ;
hence ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) ; :: thesis: verum