theorem Th8: :: PDLAX:8

for Z being open Subset of REAL holds
( sin is_differentiable_on Z & sin `| Z = cos | Z & cos is_differentiable_on Z & cos `| Z = - (sin | Z) )