A1: dom (sin `| REAL ) = REAL by FDIFF_1:def 8, SIN_COS:73;
A2: dom (cos | REAL ) = REAL /\ REAL by RELAT_1:90, SIN_COS:27;

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 A2, A3, FUNCT_1:70; :: thesis: verum

end;

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