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 dom (cos / sin )

proof

not x in sin " {0 }

proof

assume x in sin " {0 } ; :: thesis: contradiction
then sin . x in {0 } by FUNCT_1:def 13;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

then x in (dom sin ) \ (sin " {0 }) by SIN_COS:27, XBOOLE_0:def 5;
then x in (dom cos ) /\ ((dom sin ) \ (sin " {0 })) by SIN_COS:27, XBOOLE_0:def 4;
hence x in dom (cos / sin ) by RFUNCT_1:def 4; :: thesis: verum

end;

cot . x = (cos x) / (sin x) by A2, RFUNCT_1:def 4
.= cot x by SIN_COS4:def 2 ;
hence cot . x = cot x ; :: thesis: verum