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