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 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = centroid (f,['(a - c),(a + c)'])
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 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
centroid (f,A) = centroid (f,['(a - c),(a + c)'])
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & ['(a - c),(a + c)'] c= A & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies centroid (f,A) = centroid (f,['(a - c),(a + c)']) )
assume that
A1: ( b > 0 & c > 0 ) and
A2: d > 0 and
A3: ['(a - c),(a + c)'] c= A and
A4: d < b and
A5: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: centroid (f,A) = centroid (f,['(a - c),(a + c)'])
thus centroid (f,A) = a by A1, A2, A3, Lm22, A5
.= centroid (f,['(a - c),(a + c)']) by A1, A2, A4, A5, Lm221 ; :: thesis: verum