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 7, SIN_COS2:30, SIN_COS2:34; :: thesis: verum