let Z be open Subset of REAL ; :: thesis: ( Z c= dom tan implies (diff tan ,Z) . 2 = 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z) )
assume A1: Z c= dom tan ; :: thesis: (diff tan ,Z) . 2 = 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z)
A7: tan is_differentiable_on Z by A1, ThB10;
A15: cos ^ is_differentiable_on Z by ThB11, A1;
then A16: (cos ^ ) (#) (cos ^ ) is_differentiable_on Z by FDIFF_2:20;
(diff tan ,Z) . 2 = (diff tan ,Z) . (1 + 1)
.= ((diff tan ,Z) . (1 + 0 )) `| Z by TAYLOR_1:def 5
.= (((diff tan ,Z) . 0 ) `| Z) `| Z by TAYLOR_1:def 5
.= ((tan | Z) `| Z) `| Z by TAYLOR_1:def 5
.= (tan `| Z) `| Z by A7, FDIFF_2:16
.= (((cos ^ ) ^2 ) | Z) `| Z by ThB10, A1
.= ((cos ^ ) (#) (cos ^ )) `| Z by A16, FDIFF_2:16
.= (((cos ^ ) `| Z) (#) (cos ^ )) + (((cos ^ ) `| Z) (#) (cos ^ )) by A15, FDIFF_2:20
.= (1 (#) (((cos ^ ) `| Z) (#) (cos ^ ))) + (((cos ^ ) `| Z) (#) (cos ^ )) by RFUNCT_1:33
.= (1 (#) (((cos ^ ) `| Z) (#) (cos ^ ))) + (1 (#) (((cos ^ ) `| Z) (#) (cos ^ ))) by RFUNCT_1:33
.= (1 + 1) (#) (((cos ^ ) `| Z) (#) (cos ^ )) by ThB2
.= 2 (#) ((((cos ^ ) (#) tan ) | Z) (#) (cos ^ )) by ThB11, A1
.= 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z) by RFUNCT_1:61 ;
hence (diff tan ,Z) . 2 = 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z) ; :: thesis: verum