let f2 be PartFunc of REAL,REAL; :: thesis: 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))
let A be non empty closed_interval Subset of REAL; :: thesis: ( dom tanh = dom f2 & ( for x being Real st x in REAL holds
f2 . x = 1 / ((cosh . x) ^2) ) & f2 | A is continuous implies integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) )
assume that
A1: dom tanh = dom f2 and
A2: for x being Real st x in REAL holds
f2 . x = 1 / ((cosh . x) ^2) and
A3: f2 | A is continuous ; :: thesis: integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A))
A4: for x being Element of REAL st x in dom (tanh `| REAL) holds
(tanh `| REAL) . x = f2 . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (tanh `| REAL) implies (tanh `| REAL) . x = f2 . x )
assume x in dom (tanh `| REAL) ; :: thesis: (tanh `| REAL) . x = f2 . x
(tanh `| REAL) . x = diff (tanh,x) by FDIFF_1:def 7, SIN_COS2:36
.= 1 / ((cosh . x) ^2) by SIN_COS2:33
.= f2 . x by A2 ;
hence (tanh `| REAL) . x = f2 . x ; :: thesis: verum

end;

dom (tanh `| REAL) = dom f2 by A1, FDIFF_1:def 7, SIN_COS2:30, SIN_COS2:36;
then A5: tanh `| REAL = f2 by A4, PARTFUN1:5;
A6: dom tanh = REAL by FUNCT_2:def 1;
then f2 is_integrable_on A by A1, A3, INTEGRA5:11;
hence integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) by A1, A3, A6, A5, INTEGRA5:10, INTEGRA5:13, SIN_COS2:36; :: thesis: verum