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