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

proof

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

end;

then A3: ].0 ,PI .[ misses sin " {0 } by XBOOLE_0:def 7;
].0 ,PI .[ \ (sin " {0 }) c= (dom sin ) \ (sin " {0 }) by SIN_COS:27, XBOOLE_1:33;
then ].0 ,PI .[ c= (dom sin ) \ (sin " {0 }) by A3, XBOOLE_1:83;
then ].0 ,PI .[ c= (dom cos ) /\ ((dom sin ) \ (sin " {0 })) by SIN_COS:27, XBOOLE_1:19;
hence ].0 ,PI .[ c= dom cot by RFUNCT_1:def 4; :: thesis: verum