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

proof

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

end;

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