let A be non empty closed_interval Subset of REAL; integral (((AffineMap (1,0)) (#) sinh),A) = ((((AffineMap (1,0)) (#) cosh) - sinh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) cosh) - sinh) . (lower_bound A))
A1:
for x being Element of REAL st x in dom ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) holds
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = ((AffineMap (1,0)) (#) sinh) . x
proof
let x be
Element of
REAL ;
( x in dom ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) implies ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = ((AffineMap (1,0)) (#) sinh) . x )
assume
x in dom ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL)
;
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = ((AffineMap (1,0)) (#) sinh) . x
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x =
((1 * x) + 0) * (sinh . x)
by Th10
.=
((AffineMap (1,0)) . x) * (sinh . x)
by FCONT_1:def 4
.=
((AffineMap (1,0)) (#) sinh) . x
by VALUED_1:5
;
hence
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = ((AffineMap (1,0)) (#) sinh) . x
;
verum
end;
A2:
dom ((AffineMap (1,0)) (#) sinh) = [#] REAL
by FUNCT_2:def 1;
then
dom ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) = dom ((AffineMap (1,0)) (#) sinh)
by Th10, FDIFF_1:def 7;
then A3:
(((AffineMap (1,0)) (#) cosh) - sinh) `| REAL = (AffineMap (1,0)) (#) sinh
by A1, PARTFUN1:5;
( dom (AffineMap (1,0)) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap (1,0)) . x = (1 * x) + 0 ) )
by FCONT_1:def 4, FUNCT_2:def 1;
then
AffineMap (1,0) is_differentiable_on REAL
by FDIFF_1:23;
then A4:
((AffineMap (1,0)) (#) sinh) | REAL is continuous
by A2, FDIFF_1:21, FDIFF_1:25, SIN_COS2:34;
then A5:
((AffineMap (1,0)) (#) sinh) | A is continuous
by FCONT_1:16;
((AffineMap (1,0)) (#) sinh) | A is bounded
by A2, A4, INTEGRA5:10;
hence
integral (((AffineMap (1,0)) (#) sinh),A) = ((((AffineMap (1,0)) (#) cosh) - sinh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) cosh) - sinh) . (lower_bound A))
by A2, A5, A3, Th10, INTEGRA5:11, INTEGRA5:13; verum