let n be natural number ; :: thesis:
let Z be open Subset of REAL ; :: thesis:
assume A1: ( Z c= dom ((#Z n) * tan ) & 1 <= n ) ; :: thesis:
A2: for x being Real st x in Z holds
cos . x <> 0

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then x in dom (sin / cos ) by A1, FUNCT_1:21;
hence cos . x <> 0 by Th1; :: thesis:

end;

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then cos . x <> 0 by A2;
then tan is_differentiable_in x by FDIFF_7:46;
hence (#Z n) * tan is_differentiable_in x by TAYLOR_1:3; :: thesis:

end;

then A5: (#Z n) * tan is_differentiable_on Z by A1, FDIFF_1:16;
for x being Real st x in Z holds
(((#Z n) * tan ) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1))

let x be Real; :: thesis:
assume A6: x in Z ; :: thesis:
then A7: cos . x <> 0 by A2;
then A8: tan is_differentiable_in x by FDIFF_7:46;
consider m being Nat such that
A9: n = m + 1 by A1, NAT_1:6;
set m = n - 1;
(((#Z n) * tan ) `| Z) . x = diff ((#Z n) * tan ),x by A5, A6, FDIFF_1:def 8
.= (n * ((tan . x) #Z (n - 1))) * (diff tan ,x) by A8, TAYLOR_1:3
.= (n * ((tan . x) #Z (n - 1))) * (1 / ((cos . x) ^2 )) by A7, FDIFF_7:46
.= (n * (((sin . x) #Z (n - 1)) / ((cos . x) #Z (n - 1)))) / ((cos . x) ^2 ) by A1, A3, A6, A9, Th3, XBOOLE_1:1
.= ((n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n - 1))) / ((cos . x) ^2 )
.= (n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) ^2 )) by XCMPLX_1:79
.= (n * ((sin . x) #Z (n - 1))) / (((cos . x) #Z (n - 1)) * ((cos . x) #Z 2)) by FDIFF_7:1
.= (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z ((n - 1) + 2)) by A2, A6, PREPOWER:54
.= (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ;
hence (((#Z n) * tan ) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ; :: thesis:

end;

hence ( (#Z n) * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z n) * tan ) `| Z) . x = (n * ((sin . x) #Z (n - 1))) / ((cos . x) #Z (n + 1)) ) ) by A1, A4, FDIFF_1:16; :: thesis: