:: deftheorem Def33 defines pcs-yielding PCS_0:def 33 :
for I being set
for f being ManySortedSet of I holds
( f is pcs-yielding iff for x being set st x in I holds
f . x is pcs );