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 ['b,c'] holds
f . x = 0 ) holds
centroid (f,['a,c']) = centroid (f,['a,b'])
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 ['b,c'] holds
f . x = 0 ) implies centroid (f,['a,c']) = centroid (f,['a,b']) )
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 ['b,c'] holds
f . x = 0 ; :: thesis: centroid (f,['a,c']) = centroid (f,['a,b'])
B1: a <= c by A1, A2, XXREAL_0:2;
reconsider F = f as PartFunc of REAL,REAL ;
B2: ( dom f = dom F & 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;
C1A: integral (F,a,c) = (integral (F,a,b)) + (integral (F,b,c)) by INTEGRA6:17, B1, A4, B5, B2, B3;
Q2: integral (f,['b,c']) = 0 by Lm4, B2, A6;
D2A: integral (f,['a,c']) = integral (f,a,c) by INTEGRA5:def 4, A1, A2, XXREAL_0:2
.= (integral (f,a,b)) + 0 by C1A, INTEGRA5:def 4, A2, Q2
.= integral (f,['a,b']) by INTEGRA5:def 4, A1 ;
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;
E4: iF (#) F is_integrable_on ['a,c'] by B2, A4, B5, H1, H2, H3, INTEGRA6:14;
E5: ((id REAL) (#) F) | ['a,c'] is bounded by B5, INTEGRA6:13, H3;
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, B1, E4, E5, E2, B3;
A7: dom ((id REAL) (#) f) = REAL by FUNCT_2:52;
for x being Real st x in ['b,c'] holds
xf . x = 0

proof

let x be Real; :: thesis: ( x in ['b,c'] implies xf . x = 0 )
assume R1: x in ['b,c'] ; :: 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,['b,c']) = 0 by A7, Lm4;
D3A: integral (xf,['a,c']) = integral (xf,a,c) by INTEGRA5:def 4, A1, A2, XXREAL_0:2
.= (integral (xf,a,b)) + 0 by Q1, D1, INTEGRA5:def 4, A2
.= integral (xf,['a,b']) by A1, INTEGRA5:def 4 ;
centroid (f,['a,c']) = (integral (((id REAL) (#) f),['a,c'])) / (integral (f,['a,b'])) by D2A;
hence centroid (f,['a,c']) = centroid (f,['a,b']) by D3A; :: thesis: verum