let x be Real; :: thesis: ( x in dom cot implies sin . x <> 0 )

assume x in dom cot ; :: thesis: sin . x <> 0

then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def 1;

then x in (dom sin) \ (sin " {0}) by XBOOLE_0:def 4;

then x in dom (sin ^) by RFUNCT_1:def 2;

hence sin . x <> 0 by RFUNCT_1:3; :: thesis: verum

assume x in dom cot ; :: thesis: sin . x <> 0

then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def 1;

then x in (dom sin) \ (sin " {0}) by XBOOLE_0:def 4;

then x in dom (sin ^) by RFUNCT_1:def 2;

hence sin . x <> 0 by RFUNCT_1:3; :: thesis: verum