theorem :: PARTFUN2:32

for C being non empty set
for SC being Subset of C holds
( id SC is total iff SC = C )