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