A1: dom (((AffineMap (1,0)) (#) cosh) - sinh) = [#] 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 FCONT_1:def 4, FUNCT_2:def 1;
then A3: AffineMap (1,0) is_differentiable_on REAL by FDIFF_1:23;
A4: dom ((AffineMap (1,0)) (#) cosh) = [#] REAL by FUNCT_2:def 1;
then A5: (AffineMap (1,0)) (#) cosh is_differentiable_on REAL by A3, FDIFF_1:21, SIN_COS2:35;
A6: for x being Real st x in REAL holds
(((AffineMap (1,0)) (#) cosh) `| REAL) . x = (cosh . x) + (x * (sinh . x))

proof

let x be Real; :: thesis: ( x in REAL implies (((AffineMap (1,0)) (#) cosh) `| REAL) . x = (cosh . x) + (x * (sinh . x)) )
assume x in REAL ; :: thesis: (((AffineMap (1,0)) (#) cosh) `| REAL) . x = (cosh . x) + (x * (sinh . x))
(((AffineMap (1,0)) (#) cosh) `| REAL) . x = ((cosh . x) * (diff ((AffineMap (1,0)),x))) + (((AffineMap (1,0)) . x) * (diff (cosh,x))) by A4, A3, FDIFF_1:21, SIN_COS2:35
.= ((cosh . x) * (((AffineMap (1,0)) `| REAL) . x)) + (((AffineMap (1,0)) . x) * (diff (cosh,x))) by A3, FDIFF_1:def 7
.= ((cosh . x) * 1) + (((AffineMap (1,0)) . x) * (diff (cosh,x))) by A2, FDIFF_1:23
.= (cosh . x) + (((AffineMap (1,0)) . x) * (sinh . x)) by SIN_COS2:35
.= (cosh . x) + (((1 * x) + 0) * (sinh . x)) by FCONT_1:def 4
.= (cosh . x) + (x * (sinh . x)) ;
hence (((AffineMap (1,0)) (#) cosh) `| REAL) . x = (cosh . x) + (x * (sinh . x)) ; :: thesis: verum

end;

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

proof

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

end;

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