let x be Real; :: thesis: ( sin . x <> 0 implies cot . x = cot x )
assume A1: sin . x <> 0 ; :: thesis: cot . x = cot x
A2: x in REAL by XREAL_0:def 1;
not x in sin " {0}
proof
assume x in sin " {0} ; :: thesis: contradiction
then sin . x in {0} by FUNCT_1:def 7;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum
end;
then x in (dom sin) \ (sin " {0}) by SIN_COS:24, XBOOLE_0:def 5, A2;
then x in (dom cos) /\ ((dom sin) \ (sin " {0})) by SIN_COS:24, XBOOLE_0:def 4, A2;
then x in dom (cos / sin) by RFUNCT_1:def 1;
then cot . x = (cos x) / (sin x) by RFUNCT_1:def 1
.= cot x by SIN_COS4:def 2 ;
hence cot . x = cot x ; :: thesis: verum