theorem :: PARTFUN2:40

for C, D being non empty set
for SC being Subset of C
for d being Element of D
for f being PartFunc of C,D st f | SC = (dom (f | SC)) --> d holds
f | SC is constant