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;
hence
((AffineMap (1,0)) (#) cosh) - sinh is_differentiable_on REAL
by A1, FDIFF_1:19, SIN_COS2:34; for x being Real holds ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x)
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;
( x in REAL implies (((AffineMap (1,0)) (#) cosh) `| REAL) . x = (cosh . x) + (x * (sinh . x)) )
assume A7:
x in REAL
;
(((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, A7
.=
((cosh . x) * (((AffineMap (1,0)) `| REAL) . x)) + (((AffineMap (1,0)) . x) * (diff (cosh,x)))
by A3, FDIFF_1:def 7, A7
.=
((cosh . x) * 1) + (((AffineMap (1,0)) . x) * (diff (cosh,x)))
by A2, FDIFF_1:23, A7
.=
(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))
;
verum
end;
A8:
for x being Real st x in REAL holds
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x)
proof
let x be
Real;
( x in REAL implies ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x) )
assume A9:
x in REAL
;
((((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, A9
.=
((((AffineMap (1,0)) (#) cosh) `| REAL) . x) - (diff (sinh,x))
by A5, FDIFF_1:def 7, A9
.=
((cosh . x) + (x * (sinh . x))) - (diff (sinh,x))
by A6, A9
.=
((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)
;
verum
end;
let x be Real; ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x)
x in REAL
by XREAL_0:def 1;
hence
((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x)
by A8; verum