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 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 ) (#) cosh ) = [#] REAL by FUNCT_2:def 1;
then A5: (AffineMap 1,0 ) (#) cosh is_differentiable_on REAL by A3, FDIFF_1:29, 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:29, SIN_COS2:35
.= ((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 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, A5, FDIFF_1:27, SIN_COS2:34
.= ((((AffineMap 1,0 ) (#) cosh ) `| REAL ) . x) - (diff sinh ,x) by A5, FDIFF_1:def 8
.= ((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:27, SIN_COS2:34; :: thesis: verum