set f = sin ^ ;
A1: [.(- (PI / 2)),0 .[ \ (sin " {0 }) c= (dom sin ) \ (sin " {0 }) by SIN_COS:27, XBOOLE_1:33;
[.(- (PI / 2)),0 .[ /\ (sin " {0 }) = {}

proof

assume [.(- (PI / 2)),0 .[ /\ (sin " {0 }) <> {} ; :: thesis: contradiction
then consider rr being set such that
A2: rr in [.(- (PI / 2)),0 .[ /\ (sin " {0 }) by XBOOLE_0:def 1;
A3: ( rr in [.(- (PI / 2)),0 .[ & rr in sin " {0 } ) by A2, XBOOLE_0:def 4;
then reconsider rr = rr as real number ;
( - PI < rr & rr < 0 ) by A3, Lm3, XXREAL_1:4;
then ( (- PI ) + (2 * PI ) < rr + (2 * PI ) & rr + (2 * PI ) < 0 + (2 * PI ) ) by XREAL_1:10;
then rr + (2 * PI ) in ].PI ,(2 * PI ).[ ;
then sin . (rr + (2 * PI )) < 0 by COMPTRIG:25;
then A5: sin . rr <> 0 by SIN_COS:83;
sin . rr in {0 } by A3, FUNCT_1:def 13;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

then [.(- (PI / 2)),0 .[ misses sin " {0 } by XBOOLE_0:def 7;
then [.(- (PI / 2)),0 .[ c= (dom sin ) \ (sin " {0 }) by A1, XBOOLE_1:83;
hence [.(- (PI / 2)),0 .[ c= dom cosec by RFUNCT_1:def 8; :: thesis: verum