theorem :: INTEGRA8:59

for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds
( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous holds
integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A))