let x be Real; :: thesis: ( x in dom tan implies cos . x <> 0 )
assume x in dom tan ; :: thesis: cos . x <> 0
then x in (dom sin) /\ ((dom cos) \ (cos " {0})) by RFUNCT_1:def 1;
then x in (dom cos) \ (cos " {0}) by XBOOLE_0:def 4;
then x in dom (cos ^) by RFUNCT_1:def 2;
hence cos . x <> 0 by RFUNCT_1:3; :: thesis: verum