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