theorem Th2: :: INTEGR11:2

( (AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0)))) is_differentiable_on REAL & ( for x being Real holds (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2 ) )