let Z be open Subset of REAL; :: thesis: ( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z )
A1: dom (sin | Z) = (dom sin) /\ Z by RELAT_1:61
.= Z by SIN_COS:24, XBOOLE_1:28 ;
A2: dom (cos | Z) = (dom cos) /\ Z by RELAT_1:61
.= Z by SIN_COS:24, XBOOLE_1:28 ;
A3: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
A4: for x being Element of REAL st x in Z holds
(sin `| Z) . x = (cos | Z) . x

proof

let x be Element of REAL ; :: thesis: ( x in Z implies (sin `| Z) . x = (cos | Z) . x )
assume A5: x in Z ; :: thesis: (sin `| Z) . x = (cos | Z) . x
(sin `| Z) . x = diff (sin,x) by A3, A5, FDIFF_1:def 7
.= cos . x by SIN_COS:64
.= (cos | Z) . x by A2, A5, FUNCT_1:47 ;
hence (sin `| Z) . x = (cos | Z) . x ; :: thesis: verum

end;

A6: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
then A7: dom (cos `| Z) = Z by FDIFF_1:def 7;
A8: dom ((- sin) | Z) = (dom ((- 1) (#) sin)) /\ Z by RELAT_1:61
.= (dom sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24, XBOOLE_1:28 ;
A9: for x being Element of REAL st x in Z holds
(cos `| Z) . x = ((- sin) | Z) . x

proof

let x be Element of REAL ; :: thesis: ( x in Z implies (cos `| Z) . x = ((- sin) | Z) . x )
assume A10: x in Z ; :: thesis: (cos `| Z) . x = ((- sin) | Z) . x
x in dom sin by SIN_COS:24;
then A11: x in dom ((- 1) (#) sin) by VALUED_1:def 5;
(cos `| Z) . x = diff (cos,x) by A6, A10, FDIFF_1:def 7
.= - (sin . x) by SIN_COS:63
.= (- 1) * (sin . x)
.= (- sin) . x by A11, VALUED_1:def 5
.= ((- sin) | Z) . x by A8, A10, FUNCT_1:47 ;
hence (cos `| Z) . x = ((- sin) | Z) . x ; :: thesis: verum

end;

dom (sin `| Z) = Z by A3, FDIFF_1:def 7;
hence ( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z ) by A8, A1, A2, A4, A7, A9, PARTFUN1:5; :: thesis: verum