let Z be open Subset of REAL ; :: thesis: ( Z c= dom tan implies ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z ) )
assume A1: Z c= dom tan ; :: thesis: ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z )
A13: for x being Real st x in Z holds
cos . x <> 0 by A1, FDIFF_8:1;
then A15: cos ^ is_differentiable_on Z by FDIFF_4:39;
C5: dom ((cos ^ ) `| Z) = Z by A15, FDIFF_1:def 8;
AA: dom tan = dom (sin (#) (cos ^ )) by RFUNCT_1:47, SIN_COS:def 30
.= (dom sin ) /\ (dom (cos ^ )) by VALUED_1:def 4 ;
(dom sin ) /\ (dom (cos ^ )) c= dom (cos ^ ) by XBOOLE_1:17;
then B4: Z c= dom (cos ^ ) by A1, AA, XBOOLE_1:1;
C7: dom (((cos ^ ) (#) tan ) | Z) = (dom ((cos ^ ) (#) tan )) /\ Z by RELAT_1:90
.= ((dom (cos ^ )) /\ (dom tan )) /\ Z by VALUED_1:def 4
.= Z by B4, A1, XBOOLE_1:19, XBOOLE_1:28 ;
for x being Real st x in Z holds
((cos ^ ) `| Z) . x = (((cos ^ ) (#) tan ) | Z) . x

proof

let x be Real; :: thesis: ( x in Z implies ((cos ^ ) `| Z) . x = (((cos ^ ) (#) tan ) | Z) . x )
assume A18: x in Z ; :: thesis: ((cos ^ ) `| Z) . x = (((cos ^ ) (#) tan ) | Z) . x
D1: dom ((cos ^ ) (#) sin ) = dom tan by RFUNCT_1:47, SIN_COS:def 30;
then dom (((cos ^ ) (#) sin ) (#) (cos ^ )) = (dom tan ) /\ (dom (cos ^ )) by VALUED_1:def 4;
then A23: Z c= dom (((cos ^ ) (#) sin ) (#) (cos ^ )) by B4, A1, XBOOLE_1:19;
((cos ^ ) `| Z) . x = (sin . x) / ((cos . x) ^2 ) by A18, A13, FDIFF_4:39
.= (1 / (cos . x)) * ((sin . x) / (cos . x)) by XCMPLX_1:104
.= ((1 / (cos . x)) * (sin . x)) * (1 / (cos . x)) by XCMPLX_1:100
.= ((1 / (cos . x)) * (sin . x)) * (1 * ((cos . x) " )) by XCMPLX_0:def 9
.= ((1 * ((cos . x) " )) * (sin . x)) * (1 * ((cos . x) " )) by XCMPLX_0:def 9
.= (((cos ^ ) . x) * (sin . x)) * (1 * ((cos . x) " )) by A18, B4, RFUNCT_1:def 8
.= (((cos ^ ) . x) * (sin . x)) * ((cos ^ ) . x) by A18, B4, RFUNCT_1:def 8
.= (((cos ^ ) (#) sin ) . x) * ((cos ^ ) . x) by A18, A1, D1, VALUED_1:def 4
.= (((cos ^ ) (#) sin ) (#) (cos ^ )) . x by A18, A23, VALUED_1:def 4
.= ((((cos ^ ) (#) sin ) (#) (cos ^ )) | Z) . x by A18, FUNCT_1:72
.= (((cos ^ ) (#) tan ) | Z) . x by RFUNCT_1:47, SIN_COS:def 30 ;
hence ((cos ^ ) `| Z) . x = (((cos ^ ) (#) tan ) | Z) . x ; :: thesis: verum

end;

hence ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z ) by C7, C5, A13, FDIFF_4:39, PARTFUN1:34; :: thesis: verum