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

proof

assume ].0,(PI / 2).] /\ (sin " {0}) <> {} ; :: thesis: contradiction
then consider rr being set such that
A1: rr in ].0,(PI / 2).] /\ (sin " {0}) by XBOOLE_0:def 1;
rr in sin " {0} by A1, XBOOLE_0:def 4;
then A2: sin . rr in {0} by FUNCT_1:def 7;
rr in ].0,(PI / 2).] by A1, XBOOLE_0:def 4;
then sin . rr <> 0 by Lm4, COMPTRIG:7;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

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