A1: dom (sin | REAL ) = REAL /\ REAL by RELAT_1:90, SIN_COS:27;
A2: dom ((- 1) (#) cos ) = [#] REAL by SIN_COS:27, VALUED_1:def 5;

A3: now

let x be set ; :: thesis: ( x in dom (((- 1) (#) cos ) `| REAL ) implies (((- 1) (#) cos ) `| REAL ) . x = (sin | REAL ) . x )
assume A4: 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 A2, A4, 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 A1, A4, FUNCT_1:70; :: thesis: verum

end;

A5: (- 1) (#) cos is_differentiable_on REAL by A2, FDIFF_1:28, SIN_COS:72;
then dom (((- 1) (#) cos ) `| REAL ) = REAL by FDIFF_1:def 8;
then ((- 1) (#) cos ) `| REAL = sin | REAL by A1, A3, FUNCT_1:9;
hence (- 1) (#) cos is_integral_of sin , REAL by A5, Lm1; :: thesis: verum