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