theorem :: INTEGRA8:61

for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st dom tanh = dom f2 & ( for x being Real st x in REAL holds
f2 . x = 1 / ((cosh . x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A))