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 7;
dom tan = dom (sin (#) (cos ^)) by RFUNCT_1:31, SIN_COS:def 26
.= (dom sin) /\ (dom (cos ^)) by VALUED_1:def 4 ;
then A5: Z c= dom (cos ^) by A2, A1;
A6: for x being Element of REAL st x in Z holds
((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x

proof

let x be Element of REAL ; :: thesis: ( x in Z implies ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x )
A7: dom ((cos ^) (#) sin) = dom tan by RFUNCT_1:31, SIN_COS:def 26;
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:103
.= ((1 / (cos . x)) * (sin . x)) * (1 / (cos . x)) by XCMPLX_1:99
.= ((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 2
.= (((cos ^) . x) * (sin . x)) * ((cos ^) . x) by A5, A9, RFUNCT_1:def 2
.= (((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:49
.= (((cos ^) (#) tan) | Z) . x by RFUNCT_1:31, SIN_COS:def 26 ;
hence ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x ; :: thesis: verum

end;

dom (((cos ^) (#) tan) | Z) = (dom ((cos ^) (#) tan)) /\ Z by RELAT_1:61
.= ((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:5; :: thesis: verum