A1: ( dom (((AffineMap 1,0 ) (#) sinh ) - cosh ) = [#] REAL & dom ((AffineMap 1,0 ) (#) sinh ) = [#] REAL & dom (AffineMap 1,0 ) = [#] REAL ) by FUNCT_2:def 1;
A2: for x being Real st x in REAL holds
(AffineMap 1,0 ) . x = (1 * x) + 0 by JORDAN16:def 3;
then A3: ( AffineMap 1,0 is_differentiable_on REAL & ( for x being Real st x in REAL holds
((AffineMap 1,0 ) `| REAL ) . x = 1 ) ) by A1, FDIFF_1:31;
then A4: (AffineMap 1,0 ) (#) sinh is_differentiable_on REAL by A1, SIN_COS2:34, FDIFF_1:29;
A5: 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 A1, A3, SIN_COS2:34, FDIFF_1:29
.= ((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 A1, 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, A4, SIN_COS2:35, FDIFF_1:27
.= ((((AffineMap 1,0 ) (#) sinh ) `| REAL ) . x) - (diff cosh ,x) by A4, FDIFF_1:def 8
.= ((sinh . x) + (x * (cosh . x))) - (diff cosh ,x) by A5
.= ((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, A4, SIN_COS2:35, FDIFF_1:27; :: thesis: verum