A1: dom cosh = REAL by SIN_COS2:30;
for x being Real st x in REAL holds
diff sinh ,x = cosh . x by SIN_COS2:34;
hence sinh `| REAL = cosh by A1, FDIFF_1:def 8, SIN_COS2:34; :: thesis: verum