set f = cos ^ ;
[.0 ,(PI / 2).[ /\ (cos " {0 }) = {}

proof

assume [.0 ,(PI / 2).[ /\ (cos " {0 }) <> {} ; :: thesis: contradiction
then consider rr being set such that
A1: rr in [.0 ,(PI / 2).[ /\ (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 13;
rr in [.0 ,(PI / 2).[ by A1, XBOOLE_0:def 4;
then cos . rr <> 0 by Lm1, COMPTRIG:27;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum

end;

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