theorem Th16: :: INTEGR11:16

for A being non empty closed_interval Subset of REAL holds integral ((cos ^2),A) = (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (upper_bound A)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (lower_bound A))