let Z be open Subset of REAL ; :: thesis: ( not 0 in Z implies dom (sin * ((id Z) ^ )) = Z )
assume A: not 0 in Z ; :: thesis: dom (sin * ((id Z) ^ )) = Z
B: (id Z) " {0 } = {}

proof

(id Z) " {0 } c= {}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (id Z) " {0 } or x in {} )
assume x in (id Z) " {0 } ; :: thesis: x in {}
then X1: ( x in dom (id Z) & (id Z) . x in {0 } ) by FUNCT_1:def 13;
then X2: x in Z by FUNCT_1:34;
then x in {0 } by X1, FUNCT_1:35;
hence x in {} by X2, A, TARSKI:def 1; :: thesis: verum

end;

hence (id Z) " {0 } = {} by XBOOLE_1:3; :: thesis: verum

end;

A0: dom ((id Z) ^ ) = (dom (id Z)) \ ((id Z) " {0 }) by RFUNCT_1:def 8
.= Z by B, FUNCT_1:34 ;
A1: dom sin = REAL by SIN_COS:27;
rng ((id Z) ^ ) c= REAL by RELAT_1:def 19;
hence dom (sin * ((id Z) ^ )) = Z by A0, A1, RELAT_1:46; :: thesis: verum