let Z be open Subset of REAL; :: thesis: ( Z c= dom tan implies ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) )
set f1 = cos ^ ;
assume A1: Z c= dom tan ; :: thesis: ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z )
A2: (dom sin) /\ (dom (cos ^)) c= dom (cos ^) by XBOOLE_1:17;
A3: dom tan = dom (sin (#) (cos ^)) by RFUNCT_1:31, SIN_COS:def 26
.= (dom sin) /\ (dom (cos ^)) by VALUED_1:def 4 ;
then A4: Z c= dom (cos ^) by A1, A2;
A5: dom ((cos ^) (#) (cos ^)) = (dom (cos ^)) /\ (dom (cos ^)) by VALUED_1:def 4
.= dom (cos ^) ;
then A6: dom (((cos ^) (#) (cos ^)) | Z) = (dom (cos ^)) /\ Z by RELAT_1:61
.= Z by A1, A3, A2, XBOOLE_1:1, XBOOLE_1:28 ;
A7: for x being Real st x in Z holds
tan is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies tan is_differentiable_in x )
assume x in Z ; :: thesis: tan is_differentiable_in x
then A8: cos . x <> 0 by A1, FDIFF_8:1;
( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64;
hence tan is_differentiable_in x by A8, FDIFF_2:14, SIN_COS:def 26; :: thesis: verum

end;

then A9: tan is_differentiable_on Z by A1, FDIFF_1:9;
A10: for x being Element of REAL st x in dom (tan `| Z) holds
(tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (tan `| Z) implies (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x )
assume x in dom (tan `| Z) ; :: thesis: (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x
then A11: x in Z by A9, FDIFF_1:def 7;
then A12: cos . x <> 0 by A1, FDIFF_8:1;
(tan `| Z) . x = diff ((sin / cos),x) by A9, A11, FDIFF_1:def 7, SIN_COS:def 26
.= 1 / ((cos . x) ^2) by A12, FDIFF_7:46
.= (1 / (cos . x)) * (1 / (cos . x)) by XCMPLX_1:102
.= (1 * ((cos . x) ")) * (1 / (cos . x)) by XCMPLX_0:def 9
.= ((cos ^) . x) * (1 / (cos . x)) by A4, A11, RFUNCT_1:def 2
.= ((cos ^) . x) * (1 * ((cos . x) ")) by XCMPLX_0:def 9
.= ((cos ^) . x) * ((cos ^) . x) by A4, A11, RFUNCT_1:def 2
.= ((cos ^) (#) (cos ^)) . x by A4, A5, A11, VALUED_1:def 4
.= (((cos ^) (#) (cos ^)) | Z) . x by A11, FUNCT_1:49 ;
hence (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x ; :: thesis: verum

end;

dom (tan `| Z) = Z by A9, FDIFF_1:def 7;
hence ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) by A1, A7, A6, A10, FDIFF_1:9, PARTFUN1:5; :: thesis: verum