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