[.(- (PI / 2)),0.[ /\ (sin " {0}) = {}

proof

assume [.(- (PI / 2)),0.[ /\ (sin " {0}) <> {} ; :: thesis: contradiction
then consider rr being object such that
A1: rr in [.(- (PI / 2)),0.[ /\ (sin " {0}) by XBOOLE_0:def 1;
A2: rr in sin " {0} by A1, XBOOLE_0:def 4;
A3: rr in [.(- (PI / 2)),0.[ by A1, XBOOLE_0:def 4;
reconsider rr = rr as Real by A1;
rr < 0 by A3, Lm3, XXREAL_1:4;
then A4: rr + (2 * PI) < 0 + (2 * PI) by XREAL_1:8;
- PI < rr by A3, Lm3, XXREAL_1:4;
then (- PI) + (2 * PI) < rr + (2 * PI) by XREAL_1:8;
then rr + (2 * PI) in ].PI,(2 * PI).[ by A4;
then sin . (rr + (2 * PI)) < 0 by COMPTRIG:9;
then A5: sin . rr <> 0 by SIN_COS:78;
sin . rr in {0} by A2, FUNCT_1:def 7;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

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