A1: dom (((AffineMap (1,0)) (#) sinh) - cosh) = [#] REAL by FUNCT_2:def 1;
A2: ( dom (AffineMap (1,0)) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap (1,0)) . x = (1 * x) + 0 ) ) by FUNCT_2:def 1, JORDAN16:def 3;
then A3: AffineMap (1,0) is_differentiable_on REAL by FDIFF_1:31;
A4: dom ((AffineMap (1,0)) (#) sinh) = [#] REAL by FUNCT_2:def 1;
then A5: (AffineMap (1,0)) (#) sinh is_differentiable_on REAL by A3, FDIFF_1:29, SIN_COS2:34;
A6: for x being Real st x in REAL holds
(((AffineMap (1,0)) (#) sinh) `| REAL) . x = (sinh . x) + (x * (cosh . x))

proof

let x be Real; :: thesis: ( x in REAL implies (((AffineMap (1,0)) (#) sinh) `| REAL) . x = (sinh . x) + (x * (cosh . x)) )
assume x in REAL ; :: thesis: (((AffineMap (1,0)) (#) sinh) `| REAL) . x = (sinh . x) + (x * (cosh . x))
(((AffineMap (1,0)) (#) sinh) `| REAL) . x = ((sinh . x) * (diff ((AffineMap (1,0)),x))) + (((AffineMap (1,0)) . x) * (diff (sinh,x))) by A4, A3, FDIFF_1:29, SIN_COS2:34
.= ((sinh . x) * (((AffineMap (1,0)) `| REAL) . x)) + (((AffineMap (1,0)) . x) * (diff (sinh,x))) by A3, FDIFF_1:def 8
.= ((sinh . x) * 1) + (((AffineMap (1,0)) . x) * (diff (sinh,x))) by A2, FDIFF_1:31
.= (sinh . x) + (((AffineMap (1,0)) . x) * (cosh . x)) by SIN_COS2:34
.= (sinh . x) + (((1 * x) + 0) * (cosh . x)) by JORDAN16:def 3
.= (sinh . x) + (x * (cosh . x)) ;
hence (((AffineMap (1,0)) (#) sinh) `| REAL) . x = (sinh . x) + (x * (cosh . x)) ; :: thesis: verum

end;

for x being Real st x in REAL holds
((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x)

proof

let x be Real; :: thesis: ( x in REAL implies ((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x) )
assume x in REAL ; :: thesis: ((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x)
((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = (diff (((AffineMap (1,0)) (#) sinh),x)) - (diff (cosh,x)) by A1, A5, FDIFF_1:27, SIN_COS2:35
.= ((((AffineMap (1,0)) (#) sinh) `| REAL) . x) - (diff (cosh,x)) by A5, FDIFF_1:def 8
.= ((sinh . x) + (x * (cosh . x))) - (diff (cosh,x)) by A6
.= ((sinh . x) + (x * (cosh . x))) - (sinh . x) by SIN_COS2:35
.= x * (cosh . x) ;
hence ((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x) ; :: thesis: verum

end;

hence ( ((AffineMap (1,0)) (#) sinh) - cosh is_differentiable_on REAL & ( for x being Real holds ((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x) ) ) by A1, A5, FDIFF_1:27, SIN_COS2:35; :: thesis: verum