set f = cos ^ ;
A1: ].(PI / 2),PI .] \ (cos " {0 }) c= (dom cos ) \ (cos " {0 }) by SIN_COS:27, XBOOLE_1:33;
].(PI / 2),PI .] /\ (cos " {0 }) = {}

proof

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

end;

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