for x being Real st x in REAL holds
diff (sin,x) = cos . x by SIN_COS:73;
hence sin `| REAL = cos by FDIFF_1:def 8, SIN_COS:27, SIN_COS:73; :: thesis: verum