for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A)))