let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st a <= b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & ( for x being Real st x in ['a,b'] holds
f . x = 0 ) holds
centroid (f,['a,c']) = centroid (f,['b,c'])
let f be Function of REAL,REAL; :: thesis: ( a <= b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & ( for x being Real st x in ['a,b'] holds
f . x = 0 ) implies centroid (f,['a,c']) = centroid (f,['b,c']) )
assume that
A1: a <= b and
A2: b < c and
A4: f is_integrable_on ['a,c'] and
A5: f | ['a,c'] is bounded and
A6: for x being Real st x in ['a,b'] holds
f . x = 0 ; :: thesis: centroid (f,['a,c']) = centroid (f,['b,c'])
B1: a <= c by A1, A2, XXREAL_0:2;
reconsider F = f as PartFunc of REAL,REAL ;
B2A: dom f = REAL by FUNCT_2:def 1;
B5: F | ['a,c'] is bounded by A5;
b in [.a,c.] by A1, A2;
then B3: b in ['a,c'] by INTEGRA5:def 3, A1, A2, XXREAL_0:2;
integral (f,['a,b']) = 0 by Lm4, B2A, A6;
then Q2A: integral (f,a,b) = 0 by INTEGRA5:def 4, A1;
D2: integral (f,['a,c']) = integral (f,a,c) by INTEGRA5:def 4, A1, A2, XXREAL_0:2
.= 0 + (integral (f,b,c)) by INTEGRA6:17, A4, B5, B2A, B3, B1, Q2A
.= integral (f,['b,c']) by INTEGRA5:def 4, A2 ;
reconsider xf = (id REAL) (#) F as PartFunc of REAL,REAL ;
E2: dom xf = REAL by FUNCT_2:def 1;
H1: REAL = dom (id REAL) ;
reconsider iF = id REAL as PartFunc of REAL,REAL ;
H2: iF is_integrable_on ['a,c'] by Lm2;
H3: iF | ['a,c'] is bounded by Lm2;
then E4: iF (#) F is_integrable_on ['a,c'] by B2A, A4, B5, H1, H2, INTEGRA6:14;
E5: ((id REAL) (#) F) | ['a,c'] is bounded by H3, B5, INTEGRA6:13;
D1: ( xf is_integrable_on ['a,b'] & xf is_integrable_on ['b,c'] & integral (xf,a,c) = (integral (xf,a,b)) + (integral (xf,b,c)) ) by INTEGRA6:17, E4, E5, E2, B3, B1;
A7: dom ((id REAL) (#) f) = REAL by FUNCT_2:52;
for x being Real st x in ['a,b'] holds
xf . x = 0

proof

let x be Real; :: thesis: ( x in ['a,b'] implies xf . x = 0 )
assume R1: x in ['a,b'] ; :: thesis: xf . x = 0
thus xf . x = ((id REAL) . x) * (f . x) by VALUED_1:5
.= ((id REAL) . x) * 0 by R1, A6
.= 0 ; :: thesis: verum

end;

then Q1: integral (xf,['a,b']) = 0 by A7, Lm4;
D3: integral (xf,['a,c']) = integral (xf,a,c) by INTEGRA5:def 4, A1, A2, XXREAL_0:2
.= 0 + (integral (xf,b,c)) by Q1, D1, INTEGRA5:def 4, A1
.= integral (xf,['b,c']) by A2, INTEGRA5:def 4 ;
centroid (f,['a,c']) = (integral (((id REAL) (#) f),['a,c'])) / (integral (f,['b,c'])) by D2;
hence centroid (f,['a,c']) = centroid (f,['b,c']) by D3; :: thesis: verum