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)
then A2: tan is_differentiable_on Z by Th56;
A3: cos ^ is_differentiable_on Z by A1, Th57;
then A4: (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 A2, FDIFF_2:16
.= (((cos ^ ) ^2 ) | Z) `| Z by A1, Th56
.= ((cos ^ ) (#) (cos ^ )) `| Z by A4, FDIFF_2:16
.= (((cos ^ ) `| Z) (#) (cos ^ )) + (((cos ^ ) `| Z) (#) (cos ^ )) by A3, 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 Th5
.= 2 (#) ((((cos ^ ) (#) tan ) | Z) (#) (cos ^ )) by A1, Th57
.= 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z) by RFUNCT_1:61 ;
hence (diff tan ,Z) . 2 = 2 (#) (((tan (#) (cos ^ )) (#) (cos ^ )) | Z) ; :: thesis: verum