:: deftheorem defines pcs-yielding PCS_0:def 31 :
for f being Function holds
( f is pcs-yielding iff for x being set st x in dom f holds
f . x is pcs );