let A be non empty closed_interval Subset of REAL; :: thesis: for r1, r2 being Real
for f, F being Function of REAL,REAL st f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r1,(r2 * (f . x))) ) holds
( F is_integrable_on A & F | A is bounded )
let r1, r2 be Real; :: thesis: for f, F being Function of REAL,REAL st f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r1,(r2 * (f . x))) ) holds
( F is_integrable_on A & F | A is bounded )
let f, F be Function of REAL,REAL; :: thesis: ( f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r1,(r2 * (f . x))) ) implies ( F is_integrable_on A & F | A is bounded ) )
assume that
A2: ( f is_integrable_on A & f | A is bounded ) and
A4: for x being Real holds F . x = min (r1,(r2 * (f . x))) ; :: thesis: ( F is_integrable_on A & F | A is bounded )
DD: ( REAL = dom F & REAL = dom (min ((AffineMap (0,r1)),(r2 (#) f))) ) by FUNCT_2:52;
for x being object st x in dom F holds
F . x = (min ((AffineMap (0,r1)),(r2 (#) f))) . x

proof

let x be object ; :: thesis: ( x in dom F implies F . x = (min ((AffineMap (0,r1)),(r2 (#) f))) . x )
assume A0: x in dom F ; :: thesis: F . x = (min ((AffineMap (0,r1)),(r2 (#) f))) . x
reconsider x = x as Element of REAL by A0;
(min ((AffineMap (0,r1)),(r2 (#) f))) . x = min (((AffineMap (0,r1)) . x),((r2 (#) f) . x)) by COUSIN2:def 1
.= min (((0 * x) + r1),((r2 (#) f) . x)) by FCONT_1:def 4
.= min (r1,(r2 * (f . x))) by VALUED_1:6 ;
hence F . x = (min ((AffineMap (0,r1)),(r2 (#) f))) . x by A4; :: thesis: verum

end;

then F = min ((AffineMap (0,r1)),(r2 (#) f)) by FUNCT_1:2, DD;
hence ( F is_integrable_on A & F | A is bounded ) by A2, Th16X; :: thesis: verum