let Z be open Subset of REAL; :: thesis: ( sin is_differentiable_on Z & sin `| Z = cos | Z & cos is_differentiable_on Z & cos `| Z = - (sin | Z) )
A1: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
then A3: dom (sin `| Z) = Z by FDIFF_1:def 7;
A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
then A4: dom (cos `| Z) = Z by FDIFF_1:def 7;
dom cos = REAL by FUNCT_2:def 1;
then A5: dom (cos | Z) = Z by RELAT_1:62;
dom sin = REAL by FUNCT_2:def 1;
then dom (sin | Z) = Z by RELAT_1:62;
then A6: dom (- (sin | Z)) = Z by VALUED_1:8;

A7: now :: thesis: for t being object st t in dom (sin `| Z) holds
(sin `| Z) . t = (cos | Z) . t

let t be object ; :: thesis: ( t in dom (sin `| Z) implies (sin `| Z) . t = (cos | Z) . t )
assume A8: t in dom (sin `| Z) ; :: thesis: (sin `| Z) . t = (cos | Z) . t
then reconsider x = t as Real ;
thus (sin `| Z) . t = diff (sin,x) by A1, A3, A8, FDIFF_1:def 7
.= cos . x by SIN_COS:68
.= (cos | Z) . t by A3, A8, FUNCT_1:49 ; :: thesis: verum

end;

now :: thesis: for t being object st t in dom (cos `| Z) holds
(cos `| Z) . t = (- (sin | Z)) . t

let t be object ; :: thesis: ( t in dom (cos `| Z) implies (cos `| Z) . t = (- (sin | Z)) . t )
assume A9: t in dom (cos `| Z) ; :: thesis: (cos `| Z) . t = (- (sin | Z)) . t
then reconsider x = t as Real ;
thus (cos `| Z) . t = diff (cos,x) by A2, A4, A9, FDIFF_1:def 7
.= - (sin . x) by SIN_COS:67
.= - ((sin | Z) . t) by A4, A9, FUNCT_1:49
.= (- (sin | Z)) . t by VALUED_1:8 ; :: thesis: verum

end;

hence ( sin is_differentiable_on Z & sin `| Z = cos | Z & cos is_differentiable_on Z & cos `| Z = - (sin | Z) ) by A3, A4, A5, A6, A7, FDIFF_1:26, FUNCT_1:2, SIN_COS:67, SIN_COS:68; :: thesis: verum