let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st n >= 1 holds
(diff (#Z n),Z) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z
let Z be open Subset of REAL ; :: thesis: ( n >= 1 implies (diff (#Z n),Z) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z )
assume A1: n >= 1 ; :: thesis: (diff (#Z n),Z) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z
reconsider m = n - 1 as Element of NAT by A1, INT_1:18;
A3: #Z n is_differentiable_on Z by Th18, FDIFF_1:34;
A4: #Z m is_differentiable_on Z by Th18, FDIFF_1:34;
then A5: (m + 1) (#) (#Z m) is_differentiable_on Z by FDIFF_2:19;
(diff (#Z n),Z) . 2 = (diff (#Z n),Z) . (1 + 1)
.= ((diff (#Z n),Z) . (1 + 0 )) `| Z by TAYLOR_1:def 5
.= (((diff (#Z n),Z) . 0 ) `| Z) `| Z by TAYLOR_1:def 5
.= (((#Z n) | Z) `| Z) `| Z by TAYLOR_1:def 5
.= ((#Z n) `| Z) `| Z by A3, FDIFF_2:16
.= (((m + 1) (#) (#Z ((m + 1) - 1))) | Z) `| Z by Th19
.= ((m + 1) (#) (#Z m)) `| Z by A5, FDIFF_2:16
.= (m + 1) (#) ((#Z m) `| Z) by A4, FDIFF_2:19
.= (m + 1) (#) ((m (#) (#Z (m - 1))) | Z) by Th19
.= ((m + 1) (#) (m (#) (#Z (m - 1)))) | Z by RFUNCT_1:65
.= ((n * (n - 1)) (#) (#Z (n - 2))) | Z by RFUNCT_1:29 ;
hence (diff (#Z n),Z) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z ; :: thesis: verum