set f = I --> P;
I --> P is pcs-tol-reflexive-yielding

proof

let S be TolStr ; :: according to PCS_0:def 16 :: thesis: ( S in rng (I --> P) implies S is pcs-tol-reflexive )
assume S in rng (I --> P) ; :: thesis: S is pcs-tol-reflexive
hence S is pcs-tol-reflexive by TARSKI:def 1; :: thesis: verum

end;

hence for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-tol-reflexive-yielding ; :: thesis: verum