theorem :: PARTFUN2:44
for C, D being non empty set
for SC being Subset of C
for d being Element of D holds (SC --> d) | SC is constant