let x0, r be Real; :: thesis: for n being Element of NAT st n >= 1 & x0 in ].0 ,r.[ holds
((diff ((#Z n) ^ ),].0 ,r.[) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
let n be Element of NAT ; :: thesis: ( n >= 1 & x0 in ].0 ,r.[ implies ((diff ((#Z n) ^ ),].0 ,r.[) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) )
assume that
A1: n >= 1 and
A2: x0 in ].0 ,r.[ ; :: thesis: ((diff ((#Z n) ^ ),].0 ,r.[) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0)
A3: (#Z n) ^ is_differentiable_on ].0 ,r.[ by Th34;
reconsider m = - n as Element of REAL ;
A: (#Z (n + 1)) ^ is_differentiable_on ].0 ,r.[ by Th34;
then A4: m (#) ((#Z (n + 1)) ^ ) is_differentiable_on ].0 ,r.[ by FDIFF_2:19;
A5: n + 1 >= 1 + 0 by XREAL_1:9;
A6: dom (m (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ ) by VALUED_1:def 5;
B: ].0 ,r.[ c= REAL \ {0 } by Lm2;
then A7: ].0 ,r.[ c= dom ((- n) (#) ((#Z (n + 1)) ^ )) by A6, Th36, A5;
(n + 1) + 1 >= 1 + 0 by XREAL_1:9;
then A8: ].0 ,r.[ c= dom ((#Z (n + 2)) ^ ) by Th36, B;
A9: dom ((- (n + 1)) (#) (((#Z (n + 2)) ^ ) | ].0 ,r.[)) = dom (((#Z (n + 2)) ^ ) | ].0 ,r.[) by VALUED_1:def 5
.= (dom ((#Z (n + 2)) ^ )) /\ ].0 ,r.[ by FUNCT_1:68
.= ].0 ,r.[ by A8, XBOOLE_1:28 ;
((diff ((#Z n) ^ ),].0 ,r.[) . 2) . x0 = ((diff ((#Z n) ^ ),].0 ,r.[) . (1 + 1)) . x0
.= (((diff ((#Z n) ^ ),].0 ,r.[) . (1 + 0 )) `| ].0 ,r.[) . x0 by TAYLOR_1:def 5
.= ((((diff ((#Z n) ^ ),].0 ,r.[) . 0 ) `| ].0 ,r.[) `| ].0 ,r.[) . x0 by TAYLOR_1:def 5
.= (((((#Z n) ^ ) | ].0 ,r.[) `| ].0 ,r.[) `| ].0 ,r.[) . x0 by TAYLOR_1:def 5
.= ((((#Z n) ^ ) `| ].0 ,r.[) `| ].0 ,r.[) . x0 by A3, FDIFF_2:16
.= (((m (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) `| ].0 ,r.[) . x0 by Th37, A1
.= ((m (#) ((#Z (n + 1)) ^ )) `| ].0 ,r.[) . x0 by A4, FDIFF_2:16
.= m * (diff ((#Z (n + 1)) ^ ),x0) by A2, A, A7, FDIFF_1:28
.= m * ((((#Z (n + 1)) ^ ) `| ].0 ,r.[) . x0) by A2, A, FDIFF_1:def 8
.= m * ((((- (n + 1)) (#) ((#Z ((n + 1) + 1)) ^ )) | ].0 ,r.[) . x0) by Th37, A5
.= m * (((- (n + 1)) (#) (((#Z (n + 2)) ^ ) | ].0 ,r.[)) . x0) by RFUNCT_1:65
.= m * ((- (n + 1)) * ((((#Z (n + 2)) ^ ) | ].0 ,r.[) . x0)) by A9, A2, VALUED_1:def 5
.= (n * (n + 1)) * ((((#Z (n + 2)) ^ ) | ].0 ,r.[) . x0)
.= (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) by A2, FUNCT_1:72 ;
hence ((diff ((#Z n) ^ ),].0 ,r.[) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^ ) . x0) ; :: thesis: verum