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

proof

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

proof

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

end;

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

end;

then ].(- (PI / 2)),(PI / 2).[ c= (dom sin ) /\ ((dom cos ) \ (cos " {0 })) by SIN_COS:27, XBOOLE_1:19;
hence ].(- (PI / 2)),(PI / 2).[ c= dom tan by RFUNCT_1:def 4; :: thesis: verum