let a, b, c, d be Real; :: thesis: for f being Function of REAL,REAL st a <= b & b < c & c <= d & f is_integrable_on ['a,d'] & f | ['a,d'] is bounded & ( for x being Real st x in ['a,b'] \/ ['c,d'] holds
f . x = 0 ) holds
centroid (f,['a,d']) = centroid (f,['b,c'])
let f be Function of REAL,REAL; :: thesis: ( a <= b & b < c & c <= d & f is_integrable_on ['a,d'] & f | ['a,d'] is bounded & ( for x being Real st x in ['a,b'] \/ ['c,d'] holds
f . x = 0 ) implies centroid (f,['a,d']) = centroid (f,['b,c']) )
assume A1: ( a <= b & b < c & c <= d ) ; :: thesis: ( not f is_integrable_on ['a,d'] or not f | ['a,d'] is bounded or ex x being Real st
( x in ['a,b'] \/ ['c,d'] & not f . x = 0 ) or centroid (f,['a,d']) = centroid (f,['b,c']) )
then A4: a < c by XXREAL_0:2;
assume A2: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ; :: thesis: ( ex x being Real st
( x in ['a,b'] \/ ['c,d'] & not f . x = 0 ) or centroid (f,['a,d']) = centroid (f,['b,c']) )
assume A3: for x being Real st x in ['a,b'] \/ ['c,d'] holds
f . x = 0 ; :: thesis: centroid (f,['a,d']) = centroid (f,['b,c'])
A5: for x being Real st x in ['c,d'] holds
f . x = 0

proof

let x be Real; :: thesis: ( x in ['c,d'] implies f . x = 0 )
assume x in ['c,d'] ; :: thesis: f . x = 0
then x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence f . x = 0 by A3; :: thesis: verum

end;

AA: ( a <= a & a <= c & c <= d ) by XXREAL_0:2, A1;
AD: a <= d by XXREAL_0:2, A1, A4;
reconsider F = f as PartFunc of REAL,REAL ;
B2: ( F is_integrable_on ['a,d'] & F | ['a,d'] is bounded ) by A2;
A6: REAL = dom f by FUNCT_2:def 1;
( a <= c & c <= d ) by XXREAL_0:2, A1;
then c in [.a,d.] ;
then A9: c in ['a,d'] by XXREAL_0:2, A1, A4, INTEGRA5:def 3;
A8: for x being Real st x in ['a,b'] holds
F . x = 0

proof

let x be Real; :: thesis: ( x in ['a,b'] implies F . x = 0 )
assume x in ['a,b'] ; :: thesis: F . x = 0
then x in ['a,b'] \/ ['c,d'] by XBOOLE_0:def 3;
hence F . x = 0 by A3; :: thesis: verum

end;

reconsider F = F as Function of REAL,REAL ;
A7a: F is_integrable_on ['a,c'] by INTEGRA6:17, AD, A6, A9, B2;
A77a: F | ['a,c'] is bounded by INTEGRA6:18, AA, A6, B2;
thus centroid (f,['a,d']) = centroid (F,['a,c']) by A4, A5, A1, A2, FUZZY_6:8
.= centroid (f,['b,c']) by A8, A1, A7a, A77a, FUZZY_6:9 ; :: thesis: verum