A1: dom (cos | REAL) = REAL /\ REAL by RELAT_1:61, SIN_COS:24;

A2: now

let x be set ; :: thesis: ( x in dom (sin `| REAL) implies (sin `| REAL) . x = (cos | REAL) . x )
assume A3: x in dom (sin `| REAL) ; :: thesis: (sin `| REAL) . x = (cos | REAL) . x
then reconsider z = x as real number ;
(sin `| REAL) . x = diff (sin,z) by A3, FDIFF_1:def 7, SIN_COS:68;
then (sin `| REAL) . x = cos . z by SIN_COS:64;
hence (sin `| REAL) . x = (cos | REAL) . x by A1, A3, FUNCT_1:47; :: thesis: verum

end;

dom (sin `| REAL) = REAL by FDIFF_1:def 7, SIN_COS:68;
then sin `| REAL = cos | REAL by A1, A2, FUNCT_1:2;
hence sin is_integral_of cos , REAL by Lm1, SIN_COS:68; :: thesis: verum