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

A2: now :: thesis: for x being object st x in dom (sin `| REAL) holds
(sin `| REAL) . x = (cos | REAL) . x

let x be object ; :: 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 ;
(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 ; :: 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