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

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

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