let n, m be Element of NAT ; :: thesis: for Z being open Subset of REAL st n > m holds
(diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z
let Z be open Subset of REAL; :: thesis: ( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z )
defpred S₁[ Nat] means ( n > $1 implies (diff ((#Z n),Z)) . $1 = (((n choose $1) * ($1 !)) (#) (#Z (n - $1))) | Z );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
assume A3: n > k + 1 ; :: thesis: (diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z
then A4: n - k > (k + 1) - k by XREAL_1:9;
A5: (k + 1) + (- 1) <= n + 0 by A3, XREAL_1:7;
then reconsider l = n - k as Element of NAT by INT_1:5;
l >= (k + 1) - k by A3, XREAL_1:9;
then A6: ( (k + 1) ! > 0 & l -' 1 = (n - k) - 1 ) by XREAL_1:233;
reconsider s = n - (k + 1) as Element of NAT by A3, INT_1:5;
A7: #Z l is_differentiable_on Z by Th8, FDIFF_1:26;
then A8: ((n choose k) * (k !)) (#) (#Z l) is_differentiable_on Z by FDIFF_2:19;
0 + k < 1 + k by XREAL_1:6;
then (diff ((#Z n),Z)) . (k + 1) = ((((n choose k) * (k !)) (#) (#Z l)) | Z) `| Z by A2, A3, TAYLOR_1:def 5, XXREAL_0:2
.= (((n choose k) * (k !)) (#) (#Z l)) `| Z by A8, FDIFF_2:16
.= ((n choose k) * (k !)) (#) ((#Z l) `| Z) by A7, FDIFF_2:19
.= ((n choose k) * (k !)) (#) ((l (#) (#Z (l - 1))) | Z) by Th28
.= (((n choose k) * (k !)) (#) (l (#) (#Z (l - 1)))) | Z by RFUNCT_1:49
.= ((((n choose k) * (k !)) * l) (#) (#Z (l - 1))) | Z by RFUNCT_1:17
.= (((((n !) / ((k !) * (l !))) * (k !)) * (n - k)) (#) (#Z (l - 1))) | Z by A5, NEWTON:def 3
.= ((((n !) / (l !)) * l) (#) (#Z (l - 1))) | Z by XCMPLX_1:92
.= (((n !) / ((l -' 1) !)) (#) (#Z (l - 1))) | Z by A4, Lm1
.= ((((n !) / ((s !) * ((k + 1) !))) * ((k + 1) !)) (#) (#Z ((n - k) - 1))) | Z by A6, XCMPLX_1:92
.= (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z by A3, NEWTON:def 3 ;
hence (diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z ; :: thesis: verum

end;

A9: S₁[ 0 ]

proof

assume n > 0 ; :: thesis: (diff ((#Z n),Z)) . 0 = (((n choose 0) * (0 !)) (#) (#Z (n - 0))) | Z
(diff ((#Z n),Z)) . 0 = (#Z n) | Z by TAYLOR_1:def 5
.= ((1 * 1) (#) (#Z n)) | Z by RFUNCT_1:21
.= (((n choose 0) * (0 !)) (#) (#Z (n - 0))) | Z by NEWTON:12, NEWTON:19 ;
hence (diff ((#Z n),Z)) . 0 = (((n choose 0) * (0 !)) (#) (#Z (n - 0))) | Z ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A1);
hence ( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z ) ; :: thesis: verum