let Z be open Subset of REAL; :: thesis: ( not 0 in Z implies dom (sin * ((id Z) ^)) = Z )
A1: rng ((id Z) ^) c= REAL by RELAT_1:def 19;
assume A2: not 0 in Z ; :: thesis: dom (sin * ((id Z) ^)) = Z
(id Z) " {0} c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id Z) " {0} or x in {} )
assume A3: x in (id Z) " {0} ; :: thesis: x in {}
then x in dom (id Z) by FUNCT_1:def 7;
then A4: x in Z by FUNCT_1:17;
(id Z) . x in {0} by A3, FUNCT_1:def 7;
then x in {0} by A4, FUNCT_1:18;
hence x in {} by A2, A4, TARSKI:def 1; :: thesis: verum

end;

then A5: (id Z) " {0} = {} by XBOOLE_1:3;
dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def 2
.= Z by A5, FUNCT_1:17 ;
hence dom (sin * ((id Z) ^)) = Z by A1, RELAT_1:27, SIN_COS:24; :: thesis: verum