let x be Real; :: thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies tan . x = tan x )
assume x in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: tan . x = tan x
then tan . x = (sin x) / (cos x) by Th1, RFUNCT_1:def 1
.= tan x by SIN_COS4:def 1 ;
hence tan . x = tan x ; :: thesis: verum