let A be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for f being Function of REAL,REAL st r <> 0 & f is_integrable_on A & f | A is bounded holds
centroid ((r (#) f),A) = centroid (f,A)
let r be Real; :: thesis: for f being Function of REAL,REAL st r <> 0 & f is_integrable_on A & f | A is bounded holds
centroid ((r (#) f),A) = centroid (f,A)
let f be Function of REAL,REAL; :: thesis: ( r <> 0 & f is_integrable_on A & f | A is bounded implies centroid ((r (#) f),A) = centroid (f,A) )
assume that
A0: r <> 0 and
A1: f is_integrable_on A and
A2: f | A is bounded ; :: thesis: centroid ((r (#) f),A) = centroid (f,A)
A3: f | A is integrable by A1, INTEGRA5:def 1;
A4: (f | A) | A is bounded by A2;
B4: integral ((r (#) f),A) = integral ((r (#) f) | A) by INTEGRA5:def 2
.= integral (r (#) (f | A)) by RFUNCT_1:49
.= r * (integral (f | A)) by INTEGRA2:31, A3, A4
.= r * (integral (f,A)) by INTEGRA5:def 2 ;
B5: ( ((id REAL) (#) f) | A is integrable & (((id REAL) (#) f) | A) | A is bounded ) by INTEGRA5:def 1, Lm3, A1, A2;
integral (((id REAL) (#) (r (#) f)),A) = integral ((r (#) ((id REAL) (#) f)),A) by RFUNCT_1:13
.= integral ((r (#) ((id REAL) (#) f)) | A) by INTEGRA5:def 2
.= integral (r (#) (((id REAL) (#) f) | A)) by RFUNCT_1:49
.= r * (integral (((id REAL) (#) f) | A)) by INTEGRA2:31, B5
.= r * (integral (((id REAL) (#) f),A)) by INTEGRA5:def 2 ;
hence centroid ((r (#) f),A) = centroid (f,A) by XCMPLX_1:91, A0, B4; :: thesis: verum