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