let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c, d being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = a
let a, b, c, d be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = a
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies centroid (f,A) = a )
assume that
A1: ( b > 0 & c > 0 ) and
A2: d > 0 and
A3: ['(a - c),(a + c)'] c= A and
A4: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: centroid (f,A) = a
( a < a + c & a - c < a ) by XREAL_1:44, XREAL_1:29, A1;
then a - c < a + c by XXREAL_0:2;
then ( lower_bound ['(a - c),(a + c)'] = a - c & upper_bound ['(a - c),(a + c)'] = a + c ) by FUZZY_6:7;
then B1: lower_bound ['(a - c),(a + c)'] <> upper_bound ['(a - c),(a + c)'] by A1;
B2: ( f is_integrable_on A & f | A is bounded ) by A1, A4, Lm22a;
B3: for x being Real st x in A \ ['(a - c),(a + c)'] holds
f . x = 0 by Lm22B3, A1, A2, A4;
( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 ) by A1, A2, A4, Lm22b;
then C1: centroid (f,A) = centroid (f,['(a - c),(a + c)']) by A3, B1, B2, B3, FUZZY_7:24;

per cases ( d < b or d >= b ) ;

suppose d < b ; :: thesis: centroid (f,A) = a

hence a = centroid (f,A) by Lm221, A1, A2, A4, C1; :: thesis: verum

end;

suppose K2: d >= b ; :: thesis: centroid (f,A) = a

for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|))

proof

let x be Real; :: thesis: f . x = max (0,(b - |.((b * (x - a)) / c).|))
|.((b * (x - a)) / c).| >= 0 by COMPLEX1:46;
then (- |.((b * (x - a)) / c).|) + b <= 0 + b by XREAL_1:6;
then max (0,(b - |.((b * (x - a)) / c).|)) <= b by XXREAL_0:28, A1;
then min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) = max (0,(b - |.((b * (x - a)) / c).|)) by XXREAL_0:def 9, XXREAL_0:2, K2;
hence f . x = max (0,(b - |.((b * (x - a)) / c).|)) by A4; :: thesis: verum

end;

hence centroid (f,A) = a by FUZZY_7:34, A1, A3; :: thesis: verum

end;

end;