let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
centroid (f,A) = a
let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
centroid (f,A) = a
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) implies centroid (f,A) = a )
assume that
A1: b > 0 and
A2: c > 0 and
A4: ['(a - c),(a + c)'] c= A and
A3: for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: centroid (f,A) = a
A5: ( a < a + c & a - c < a ) by XREAL_1:44, XREAL_1:29, A2;
( [.(lower_bound ['(a - c),(a + c)']),(upper_bound ['(a - c),(a + c)']).] = ['(a - c),(a + c)'] & ['(a - c),(a + c)'] = [.(a - c),(a + c).] ) by XXREAL_0:2, A5, INTEGRA5:def 3, INTEGRA1:4;
then A8: ( lower_bound ['(a - c),(a + c)'] = a - c & a + c = upper_bound ['(a - c),(a + c)'] ) by INTEGRA1:5;
A7: for x being Real st x in A \ ['(a - c),(a + c)'] holds
f . x = 0

proof

let x be Real; :: thesis: ( x in A \ ['(a - c),(a + c)'] implies f . x = 0 )
assume A71: x in A \ ['(a - c),(a + c)'] ; :: thesis: f . x = 0
not x in ['(a - c),(a + c)'] by XBOOLE_0:def 5, A71;
hence f . x = 0 by Lm20A, A1, A2, A3; :: thesis: verum

end;

A9: ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 ) by Lm20B, A1, A2, A3;
( f is_integrable_on A & f | A is bounded ) by Lm20, A1, A2, A3;
then centroid (f,A) = centroid (f,['(a - c),(a + c)']) by Th17, A4, A7, A9, A8, A5;
hence centroid (f,A) = a by A1, A2, A3, Th19; :: thesis: verum