for n, m being Element of NAT
for A being non empty closed_interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
integral (((sin * (AffineMap (m,0))) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))))) . (upper_bound A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))))) . (lower_bound A))