let a, b, c, d be Real; :: thesis: for f, F being Function of REAL,REAL st b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) & ( for x being Real holds F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)'])
let f, F be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) & ( for x being Real holds F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)']) )
assume A1: ( b > 0 & c > 0 & d > 0 ) ; :: thesis: ( ex x being Real st not f . x = max (0,(b - |.((b * (x - a)) / c).|)) or ex x being Real st not F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) or centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)']) )
assume A2: for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: ( ex x being Real st not F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) or centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)']) )
assume A3: for x being Real holds F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)'])

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

suppose d < b ; :: thesis: centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)'])

then centroid (F,['(a - c),(a + c)']) = a by Lm221, A1, A3;
hence centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)']) by FUZZY_7:31, A1, A2; :: thesis: verum

end;

suppose A5: d >= b ; :: thesis: centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)'])

A4: dom f = REAL by FUNCT_2:def 1
.= dom F by FUNCT_2:def 1 ;
for x being object st x in dom f holds
f . x = F . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = F . x )
assume Xac: x in dom f ; :: thesis: f . x = F . x
reconsider x = x as Real by Xac;
A6: d >= max (0,(b - |.((b * (x - a)) / c).|))

proof

per cases ( max (0,(b - |.((b * (x - a)) / c).|)) = 0 or max (0,(b - |.((b * (x - a)) / c).|)) = b - |.((b * (x - a)) / c).| ) by XXREAL_0:16;

suppose max (0,(b - |.((b * (x - a)) / c).|)) = 0 ; :: thesis: d >= max (0,(b - |.((b * (x - a)) / c).|))

hence d >= max (0,(b - |.((b * (x - a)) / c).|)) by A1; :: thesis: verum

end;

suppose B2: max (0,(b - |.((b * (x - a)) / c).|)) = b - |.((b * (x - a)) / c).| ; :: thesis: d >= max (0,(b - |.((b * (x - a)) / c).|))

b - |.((b * (x - a)) / c).| <= b by L724x;
hence d >= max (0,(b - |.((b * (x - a)) / c).|)) by A5, XXREAL_0:2, B2; :: thesis: verum

end;

end;

end;

F . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) by A3
.= max (0,(b - |.((b * (x - a)) / c).|)) by XXREAL_0:def 9, A6
.= f . x by A2 ;
hence f . x = F . x ; :: thesis: verum

end;

hence centroid (f,['(a - c),(a + c)']) = centroid (F,['(a - c),(a + c)']) by FUNCT_1:2, A4; :: thesis: verum

end;

end;