theorem :: PARTFUN2:37

for X being set
for C, D being non empty set
for f being PartFunc of C,D st X meets dom f holds
( f | X is constant iff ex d being Element of D st rng (f | X) = {d} )