let x be Real; :: thesis: ( cos . x <> 0 implies tan . x = tan x )
assume A1: cos . x <> 0 ; :: thesis: tan . x = tan x
A2: x in REAL by XREAL_0:def 1;
not x in cos " {0}

proof

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

end;

then x in (dom cos) \ (cos " {0}) by SIN_COS:24, XBOOLE_0:def 5, A2;
then x in (dom sin) /\ ((dom cos) \ (cos " {0})) by SIN_COS:24, XBOOLE_0:def 4, A2;
then x in dom (sin / cos) by RFUNCT_1:def 1;
then tan . x = (sin x) / (cos x) by RFUNCT_1:def 1
.= tan x by SIN_COS4:def 1 ;
hence tan . x = tan x ; :: thesis: verum