for r being Real st r in ].(- (PI / 2)),(PI / 2).[ holds
tan is_differentiable_in r

proof

let r be Real; :: thesis: ( r in ].(- (PI / 2)),(PI / 2).[ implies tan is_differentiable_in r )
assume r in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: tan is_differentiable_in r
then cos . r <> 0 by COMPTRIG:11;
hence tan is_differentiable_in r by FDIFF_7:46; :: thesis: verum

end;

hence tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by SIN_COS9:1, FDIFF_1:9; :: thesis: verum