let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real holds
( (AffineMap (a,b)) | A is bounded & AffineMap (a,b) is_integrable_on A )
let a, b be Real; :: thesis: ( (AffineMap (a,b)) | A is bounded & AffineMap (a,b) is_integrable_on A )
reconsider f = AffineMap (a,b) as PartFunc of REAL,REAL ;
A c= REAL ;
then A1: A c= dom f by FUNCT_2:def 1;
f | A is continuous ;
hence ( (AffineMap (a,b)) | A is bounded & AffineMap (a,b) is_integrable_on A ) by INTEGRA5:11, INTEGRA5:10, A1; :: thesis: verum