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= {}

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

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

then A5:
(id Z) " {0} = {}
by XBOOLE_1:3;
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;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

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