theorem Th3: :: INTEGRA4:3

for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for r being Real holds
( ( f is total & rng f = {r} ) iff f = r (#) (chi (A,A)) )