let Z be open Subset of REAL; ( 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
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
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; verum