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

proof

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

end;

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