let A, B be non empty closed_interval Subset of REAL; :: thesis: for f being Function of REAL,REAL st lower_bound B <> upper_bound B & B c= A & f is_integrable_on A & f | A is bounded & ( for x being Real st x in A \ B holds
f . x = 0 ) & f . (lower_bound B) = 0 & f . (upper_bound B) = 0 holds
centroid (f,A) = centroid (f,B)
let f be Function of REAL,REAL; :: thesis: ( lower_bound B <> upper_bound B & B c= A & f is_integrable_on A & f | A is bounded & ( for x being Real st x in A \ B holds
f . x = 0 ) & f . (lower_bound B) = 0 & f . (upper_bound B) = 0 implies centroid (f,A) = centroid (f,B) )
assume that
A0: lower_bound B <> upper_bound B and
A1: B c= A and
A4: ( f is_integrable_on A & f | A is bounded ) and
A2: for x being Real st x in A \ B holds
f . x = 0 and
A3: ( f . (lower_bound B) = 0 & f . (upper_bound B) = 0 ) ; :: thesis: centroid (f,A) = centroid (f,B)
AA: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
BB: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4
.= ['(lower_bound B),(upper_bound B)'] by INTEGRA5:def 3, SEQ_4:11 ;
lower_bound B <= upper_bound B by SEQ_4:11;
then A7: lower_bound B < upper_bound B by A0, XXREAL_0:1;
A8: ( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A ) by Th12, A1;
for x being Real st x in ['(lower_bound A),(lower_bound B)'] \/ ['(upper_bound B),(upper_bound A)'] holds
f . x = 0

proof

let x be Real; :: thesis: ( x in ['(lower_bound A),(lower_bound B)'] \/ ['(upper_bound B),(upper_bound A)'] implies f . x = 0 )
assume A9: x in ['(lower_bound A),(lower_bound B)'] \/ ['(upper_bound B),(upper_bound A)'] ; :: thesis: f . x = 0

per cases ( x in ['(lower_bound A),(lower_bound B)'] or x in ['(upper_bound B),(upper_bound A)'] ) by A9, XBOOLE_0:def 3;

suppose x in ['(lower_bound A),(lower_bound B)'] ; :: thesis: f . x = 0

then x in [.(lower_bound A),(lower_bound B).] by INTEGRA5:def 3, Th12, A1;
then x in [.(lower_bound A),(lower_bound B).[ \/ {(lower_bound B)} by XXREAL_1:129, Th12, A1;

per cases then ( x in [.(lower_bound A),(lower_bound B).[ or x in {(lower_bound B)} ) by XBOOLE_0:def 3;

suppose x in [.(lower_bound A),(lower_bound B).[ ; :: thesis: f . x = 0

then X1: x in [.(lower_bound A),(lower_bound B).[ \/ ].(upper_bound B),(upper_bound A).] by XBOOLE_0:def 3;
[.(lower_bound A),(lower_bound B).[ \/ ].(upper_bound B),(upper_bound A).] c= [.(lower_bound A),(upper_bound A).] \ [.(lower_bound B),(upper_bound B).] by Th8X, A7, A8;
then x in [.(lower_bound A),(upper_bound A).] \ [.(lower_bound B),(upper_bound B).] by X1;
then x in A \ [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
then x in A \ B by INTEGRA1:4;
hence f . x = 0 by A2; :: thesis: verum

end;

suppose x in {(lower_bound B)} ; :: thesis: f . x = 0

hence f . x = 0 by TARSKI:def 1, A3; :: thesis: verum

end;

end;

end;

suppose x in ['(upper_bound B),(upper_bound A)'] ; :: thesis: f . x = 0

then x in [.(upper_bound B),(upper_bound A).] by INTEGRA5:def 3, Th12, A1;
then x in {(upper_bound B)} \/ ].(upper_bound B),(upper_bound A).] by XXREAL_1:130, Th12, A1;

per cases then ( x in ].(upper_bound B),(upper_bound A).] or x in {(upper_bound B)} ) by XBOOLE_0:def 3;

suppose x in ].(upper_bound B),(upper_bound A).] ; :: thesis: f . x = 0

then X1: x in [.(lower_bound A),(lower_bound B).[ \/ ].(upper_bound B),(upper_bound A).] by XBOOLE_0:def 3;
[.(lower_bound A),(lower_bound B).[ \/ ].(upper_bound B),(upper_bound A).] c= [.(lower_bound A),(upper_bound A).] \ [.(lower_bound B),(upper_bound B).] by Th8X, A8, A7;
then x in [.(lower_bound A),(upper_bound A).] \ [.(lower_bound B),(upper_bound B).] by X1;
then x in A \ [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
then x in A \ B by INTEGRA1:4;
hence f . x = 0 by A2; :: thesis: verum

end;

suppose x in {(upper_bound B)} ; :: thesis: f . x = 0

hence f . x = 0 by TARSKI:def 1, A3; :: thesis: verum

end;

end;

end;

end;

end;

hence centroid (f,A) = centroid (f,B) by BB, Th11X, A7, A8, AA, A4; :: thesis: verum