:: deftheorem defines constant PARTFUN2:def 1 :
for C, D being non empty set
for f being PartFunc of C,D holds
( f is constant iff ex d being Element of D st
for c being Element of C st c in dom f holds
f . c = d );