for Z being non empty set
for f being Function of Z,REAL holds
( f is constant iff ex r being Real st f = r (#) (chi (Z,Z)) )