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 4;
then x in (dom sin ) \ (sin " {0 }) by XBOOLE_0:def 4;
then x in dom (sin ^ ) by RFUNCT_1:def 8;
hence sin . x <> 0 by RFUNCT_1:13; :: thesis: verum