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 n >= 1 ; :: thesis: (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z
then reconsider m = n - 1 as Element of NAT by INT_1:5;
A1: #Z n is_differentiable_on Z by Th8, FDIFF_1:26;
A2: #Z m is_differentiable_on Z by Th8, FDIFF_1:26;
then A3: (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 A1, FDIFF_2:16
.= (((m + 1) (#) (#Z ((m + 1) - 1))) | Z) `| Z by Th28
.= ((m + 1) (#) (#Z m)) `| Z by A3, FDIFF_2:16
.= (m + 1) (#) ((#Z m) `| Z) by A2, FDIFF_2:19
.= (m + 1) (#) ((m (#) (#Z (m - 1))) | Z) by Th28
.= ((m + 1) (#) (m (#) (#Z (m - 1)))) | Z by RFUNCT_1:49
.= ((n * (n - 1)) (#) (#Z (n - 2))) | Z by RFUNCT_1:17 ;
hence (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z ; :: thesis: verum