].0,PI.[ /\ (sin " {0}) = {}
proof
assume ].0,PI.[ /\ (sin " {0}) <> {} ; :: thesis: contradiction
then consider rr being object 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 7;
rr in ].0,PI.[ by A1, XBOOLE_0:def 4;
then sin . rr <> 0 by COMPTRIG:7;
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:24, 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:24, XBOOLE_1:19;
hence ].0,PI.[ c= dom cot by RFUNCT_1:def 1; :: thesis: verum