A1: dom (sin | REAL) = REAL /\ REAL by RELAT_1:61, SIN_COS:24;
A2: dom ((- 1) (#) cos) = [#] REAL by SIN_COS:24, 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:20, SIN_COS:67;
then (((- 1) (#) cos) `| REAL) . x = (- 1) * (- (sin . z)) by SIN_COS:63;
hence (((- 1) (#) cos) `| REAL) . x = (sin | REAL) . x by A1, A4, FUNCT_1:47; :: thesis: verum

end;

A5: (- 1) (#) cos is_differentiable_on REAL by A2, FDIFF_1:20, SIN_COS:67;
then dom (((- 1) (#) cos) `| REAL) = REAL by FDIFF_1:def 7;
then ((- 1) (#) cos) `| REAL = sin | REAL by A1, A3, FUNCT_1:2;
hence (- 1) (#) cos is_integral_of sin , REAL by A5, Lm1; :: thesis: verum