let r, p be Real; :: thesis: for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||
let f, g be PartFunc of REAL,REAL; :: thesis: for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||
let A be non empty closed_interval Subset of REAL; :: thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| )
assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; :: thesis: |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||
|||((r (#) f),(p (#) g),A)||| = integral ((r (#) (f (#) (p (#) g))),A) by RFUNCT_1:12
.= integral ((r (#) (p (#) (f (#) g))),A) by RFUNCT_1:13
.= integral (((r * p) (#) (f (#) g)),A) by RFUNCT_1:17
.= (r * p) * (integral ((f (#) g),A)) by A1, INTEGRA6:9 ;
hence |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| ; :: thesis: verum