A1: dom ((- 1) (#) cos ) = [#] REAL by SIN_COS:27, VALUED_1:def 5;
then A2: (- 1) (#) cos is_differentiable_on REAL by FDIFF_1:28, SIN_COS:72;
then A3: dom (((- 1) (#) cos ) `| REAL ) = REAL by FDIFF_1:def 8;
A4: dom (sin | REAL ) = REAL /\ REAL by RELAT_1:90, SIN_COS:27;

now

let x be set ; :: thesis: ( x in dom (((- 1) (#) cos ) `| REAL ) implies (((- 1) (#) cos ) `| REAL ) . x = (sin | REAL ) . x )
assume A5: x in dom (((- 1) (#) cos ) `| REAL ) ; :: thesis: (((- 1) (#) cos ) `| REAL ) . x = (sin | REAL ) . x
then reconsider z = x as real number ;
(((- 1) (#) cos ) `| REAL ) . x = (- 1) * (diff cos ,z) by A1, A5, FDIFF_1:28, SIN_COS:72;
then (((- 1) (#) cos ) `| REAL ) . x = (- 1) * (- (sin . z)) by SIN_COS:68;
hence (((- 1) (#) cos ) `| REAL ) . x = (sin | REAL ) . x by A4, A5, FUNCT_1:70; :: thesis: verum

end;

then ((- 1) (#) cos ) `| REAL = sin | REAL by A3, A4, FUNCT_1:9;
hence (- 1) (#) cos is_integral_of sin , REAL by A2, Lm1; :: thesis: verum