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:11;
hence diff (tan,x) = 1 / ((cos . x) ^2) by FDIFF_7:46; :: thesis: verum