let Z be open Subset of REAL ; :: thesis: ( Z c= dom tan implies ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z ) )
A1: (dom sin ) /\ (dom (cos ^ )) c= dom (cos ^ ) by XBOOLE_1:17;
assume A2: Z c= dom tan ; :: thesis: ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z )
then A3: for x being Real st x in Z holds
cos . x <> 0 by FDIFF_8:1;
then cos ^ is_differentiable_on Z by FDIFF_4:39;
then A4: dom ((cos ^ ) `| Z) = Z by FDIFF_1:def 8;
dom tan = dom (sin (#) (cos ^ )) by RFUNCT_1:47, SIN_COS:def 30
.= (dom sin ) /\ (dom (cos ^ )) by VALUED_1:def 4 ;
then A5: Z c= dom (cos ^ ) by A2, A1, XBOOLE_1:1;
A6: 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 )
A7: 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 A8: Z c= dom (((cos ^ ) (#) sin ) (#) (cos ^ )) by A2, A5, XBOOLE_1:19;
assume A9: x in Z ; :: thesis: ((cos ^ ) `| Z) . x = (((cos ^ ) (#) tan ) | Z) . x
then ((cos ^ ) `| Z) . x = (sin . x) / ((cos . x) ^2 ) by A3, 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 A5, A9, RFUNCT_1:def 8
.= (((cos ^ ) . x) * (sin . x)) * ((cos ^ ) . x) by A5, A9, RFUNCT_1:def 8
.= (((cos ^ ) (#) sin ) . x) * ((cos ^ ) . x) by A2, A9, A7, VALUED_1:def 4
.= (((cos ^ ) (#) sin ) (#) (cos ^ )) . x by A9, A8, VALUED_1:def 4
.= ((((cos ^ ) (#) sin ) (#) (cos ^ )) | Z) . x by A9, 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;

dom (((cos ^ ) (#) tan ) | Z) = (dom ((cos ^ ) (#) tan )) /\ Z by RELAT_1:90
.= ((dom (cos ^ )) /\ (dom tan )) /\ Z by VALUED_1:def 4
.= Z by A2, A5, XBOOLE_1:19, XBOOLE_1:28 ;
hence ( cos ^ is_differentiable_on Z & (cos ^ ) `| Z = ((cos ^ ) (#) tan ) | Z ) by A3, A4, A6, FDIFF_4:39, PARTFUN1:34; :: thesis: verum