hereby :: thesis: ( ( for x being set st x in dom f holds
f . x is pcs-Str ) implies f is pcs-Str-yielding )

assume A1: f is pcs-Str-yielding ; :: thesis: for x being set st x in dom f holds
f . x is pcs-Str
let x be set ; :: thesis: ( x in dom f implies f . x is pcs-Str )
assume x in dom f ; :: thesis: f . x is pcs-Str
then f . x in rng f by FUNCT_1:3;
hence f . x is pcs-Str by A1, Def28; :: thesis: verum

end;

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