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