theorem :: PARTFUN2:34

for C, D being non empty set
for SC being Subset of C
for d being Element of D holds
( SC --> d is total iff SC = C )