let r be Real; :: thesis: for f, g being PartFunc of REAL ,REAL
for A being 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),g,A)||| = r * |||(f,g,A)|||
let f, g be PartFunc of REAL ,REAL ; :: thesis: for A being 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),g,A)||| = r * |||(f,g,A)|||
let A be 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),g,A)||| = r * |||(f,g,A)||| )
assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; :: thesis: |||((r (#) f),g,A)||| = r * |||(f,g,A)|||
|||((r (#) f),g,A)||| = integral (r (#) (f (#) g)),A by RFUNCT_1:24
.= r * (integral (f (#) g),A) by A1, INTEGRA6:9 ;
hence |||((r (#) f),g,A)||| = r * |||(f,g,A)||| ; :: thesis: verum