theorem Th13: :: INTEGR11:13

for A being non empty closed_interval Subset of REAL holds integral ((sin ^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))