let Z be open Subset of REAL ; :: thesis:
A1: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then A2: dom (sin `| Z) = Z by FDIFF_1:def 8;
A3: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;
A4: dom ((- sin ) | Z) = (dom ((- 1) (#) sin )) /\ Z by RELAT_1:90
.= (dom sin ) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:27, XBOOLE_1:28 ;
A5: dom (sin | Z) = (dom sin ) /\ Z by RELAT_1:90
.= Z by SIN_COS:27, XBOOLE_1:28 ;
A6: dom (cos | Z) = (dom cos ) /\ Z by RELAT_1:90
.= Z by SIN_COS:27, XBOOLE_1:28 ;
A7: for x being Real st x in Z holds
(sin `| Z) . x = (cos | Z) . x

let x be Real; :: thesis:
assume A8: x in Z ; :: thesis:
(sin `| Z) . x = diff sin ,x by A1, A8, FDIFF_1:def 8
.= cos . x by SIN_COS:69
.= (cos | Z) . x by A6, A8, FUNCT_1:70 ;
hence (sin `| Z) . x = (cos | Z) . x ; :: thesis:

end;

A9: dom (cos `| Z) = Z by A3, FDIFF_1:def 8;
for x being Real st x in Z holds
(cos `| Z) . x = ((- sin ) | Z) . x

let x be Real; :: thesis:
assume A10: x in Z ; :: thesis:
x in dom sin by SIN_COS:27;
then A11: x in dom ((- 1) (#) sin ) by VALUED_1:def 5;
(cos `| Z) . x = diff cos ,x by A3, A10, FDIFF_1:def 8
.= - (sin . x) by SIN_COS:68
.= (- 1) * (sin . x)
.= (- sin ) . x by A11, VALUED_1:def 5
.= ((- sin ) | Z) . x by A4, A10, FUNCT_1:70 ;
hence (cos `| Z) . x = ((- sin ) | Z) . x ; :: thesis:

end;