:: deftheorem defines centroid FUZZY_6:def 1 :
for A being non empty closed_interval Subset of REAL
for f being Function of REAL,REAL holds centroid (f,A) = (integral (((id REAL) (#) f),A)) / (integral (f,A));