let Z be open Subset of REAL; :: thesis: ( sin `| Z = cos | Z & cos `| Z = () | Z & dom (sin | Z) = Z & dom (cos | Z) = Z )
A1: dom (sin | Z) = () /\ Z by RELAT_1:61
.= Z by ;
A2: dom (cos | Z) = () /\ Z by RELAT_1:61
.= Z by ;
A3: sin is_differentiable_on Z by ;
A4: for x being Element of REAL st x in Z holds
() . x = (cos | Z) . x
proof
let x be Element of REAL ; :: thesis: ( x in Z implies () . x = (cos | Z) . x )
assume A5: x in Z ; :: thesis: () . x = (cos | Z) . x
() . x = diff (sin,x) by
.= cos . x by SIN_COS:64
.= (cos | Z) . x by ;
hence (sin `| Z) . x = (cos | Z) . x ; :: thesis: verum
end;
A6: cos is_differentiable_on Z by ;
then A7: dom () = Z by FDIFF_1:def 7;
A8: dom (() | Z) = (dom ((- 1) (#) sin)) /\ Z by RELAT_1:61
.= () /\ Z by VALUED_1:def 5
.= Z by ;
A9: for x being Element of REAL st x in Z holds
() . x = (() | Z) . x
proof
let x be Element of REAL ; :: thesis: ( x in Z implies () . x = (() | Z) . x )
assume A10: x in Z ; :: thesis: () . x = (() | Z) . x
x in dom sin by SIN_COS:24;
then A11: x in dom ((- 1) (#) sin) by VALUED_1:def 5;
() . x = diff (cos,x) by
.= - (sin . x) by SIN_COS:63
.= (- 1) * (sin . x)
.= () . x by
.= (() | Z) . x by ;
hence (cos `| Z) . x = (() | Z) . x ; :: thesis: verum
end;
dom () = Z by ;
hence ( sin `| Z = cos | Z & cos `| Z = () | Z & dom (sin | Z) = Z & dom (cos | Z) = Z ) by A8, A1, A2, A4, A7, A9, PARTFUN1:5; :: thesis: verum