let x be Real; 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 ; 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; ( 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
; ((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))
; verum