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