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:21
.= (1 (#) (((cos ^) `| Z) (#) (cos ^))) + (1 (#) (((cos ^) `| Z) (#) (cos ^))) by RFUNCT_1:21
.= (1 + 1) (#) (((cos ^) `| Z) (#) (cos ^)) by Th5
.= 2 (#) ((((cos ^) (#) tan) | Z) (#) (cos ^)) by A1, Th57
.= 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) by RFUNCT_1:45 ;
hence (diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) ; :: thesis: verum