theorem :: PARTFUN2:41
for x being set
for C, D being non empty set
for f being PartFunc of C,D holds f | {x} is constant