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