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

proof

not x in cos " {0 }

proof

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

end;

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

end;

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