theorem :: SIN_COS9:3

( tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ & ( for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,x) = 1 / ((cos . x) ^2) ) ) by Lm1, Lm3;