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

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 8, SIN_COS:73;
then (sin `| REAL) . x = cos . z by SIN_COS:69;
hence (sin `| REAL) . x = (cos | REAL) . x by A1, A3, FUNCT_1:70; :: thesis: verum

end;

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