let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom ((- (1 / 2)) (#) (cos * f)) & ( for x being Real st x in Z holds
f . x = 2 * x ) holds
( (- (1 / 2)) (#) (cos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom ((- (1 / 2)) (#) (cos * f)) & ( for x being Real st x in Z holds
f . x = 2 * x ) implies ( (- (1 / 2)) (#) (cos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ) ) )
assume that
A1: Z c= dom ((- (1 / 2)) (#) (cos * f)) and
A2: for x being Real st x in Z holds
f . x = 2 * x ; :: thesis: ( (- (1 / 2)) (#) (cos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ) )
A3: ( Z c= dom (cos * f) & ( for x being Real st x in Z holds
f . x = (2 * x) + 0 ) ) by A1, A2, VALUED_1:def 5;
then A4: cos * f is_differentiable_on Z by FDIFF_4:38;
for x being Real st x in Z holds
(((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x)

proof

let x be Real; :: thesis: ( x in Z implies (((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) )
assume A5: x in Z ; :: thesis: (((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x)
then (((- (1 / 2)) (#) (cos * f)) `| Z) . x = (- (1 / 2)) * (diff ((cos * f),x)) by A1, A4, FDIFF_1:20
.= (- (1 / 2)) * (((cos * f) `| Z) . x) by A4, A5, FDIFF_1:def 7
.= (- (1 / 2)) * (- (2 * (sin . ((2 * x) + 0)))) by A3, A5, FDIFF_4:38
.= sin (2 * x) by SIN_COS:def 17 ;
hence (((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ; :: thesis: verum

end;

hence ( (- (1 / 2)) (#) (cos * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ) ) by A1, A4, FDIFF_1:20; :: thesis: verum