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