thus ( f is TolStr-yielding implies for x being set st x in dom f holds
f . x is TolStr ) by FUNCT_1:3; :: thesis: ( ( for x being set st x in dom f holds
f . x is TolStr ) implies f is TolStr-yielding )
assume A1: for x being set st x in dom f holds
f . x is TolStr ; :: thesis: f is TolStr-yielding
let P be set ; :: according to PCS_0:def 13 :: thesis: ( P in rng f implies P is TolStr )
assume P in rng f ; :: thesis: P is TolStr
then ex x being object st
( x in dom f & f . x = P ) by FUNCT_1:def 3;
hence P is TolStr by A1; :: thesis: verum