let Z be open Subset of REAL; :: thesis: ( Z c= dom (sin + (#R (1 / 2))) implies ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) )
assume A1: Z c= dom (sin + (#R (1 / 2))) ; :: thesis: ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) )
then Z c= (dom (#R (1 / 2))) /\ (dom sin) by VALUED_1:def 1;
then A2: Z c= dom (#R (1 / 2)) by XBOOLE_1:18;
then A3: #R (1 / 2) is_differentiable_on Z by Lm3;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;

now :: thesis: for x being Real st x in Z holds
((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2))))

let x be Real; :: thesis: ( x in Z implies ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) )
assume A5: x in Z ; :: thesis: ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2))))
then ((sin + (#R (1 / 2))) `| Z) . x = (diff (sin,x)) + (diff ((#R (1 / 2)),x)) by A1, A3, A4, FDIFF_1:18
.= (cos . x) + (diff ((#R (1 / 2)),x)) by SIN_COS:64
.= (cos . x) + (((#R (1 / 2)) `| Z) . x) by A3, A5, FDIFF_1:def 7
.= (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) by A2, A5, Lm3 ;
hence ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ; :: thesis: verum

end;

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