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

proof

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

end;

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