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