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 A1: ( n > m & x in Z ) ; :: thesis: ((diff (#Z n),Z) . m) . x = ((n choose m) * (m ! )) * (x #Z (n - m))
A2: dom (#Z (n - m)) = REAL by FUNCT_2:def 1;
A3: dom (((n choose m) * (m ! )) (#) (#Z (n - m))) = REAL by A2, VALUED_1:def 5;
A5: dom ((((n choose m) * (m ! )) (#) (#Z (n - m))) | Z) = REAL /\ Z by A3, RELAT_1:90
.= Z by XBOOLE_1:28 ;
((diff (#Z n),Z) . m) . x = ((((n choose m) * (m ! )) (#) (#Z (n - m))) | Z) . x by Th23, A1
.= (((n choose m) * (m ! )) (#) (#Z (n - m))) . x by A5, A1, FUNCT_1:70
.= ((n choose m) * (m ! )) * ((#Z (n - m)) . x) 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