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

proof

let S be TolStr ; :: according to PCS_0:def 18 :: thesis: ( S in rng (I --> P) implies S is pcs-tol-symmetric )
assume A1: S in rng (I --> P) ; :: thesis: S is pcs-tol-symmetric
( I = {} or I <> {} ) ;
then ( rng (I --> P) = {P} or rng (I --> P) = {} ) by FUNCOP_1:14, FUNCOP_1:16;
hence S is pcs-tol-symmetric by A1, TARSKI:def 1; :: thesis: verum

end;

hence I --> P is pcs-tol-symmetric-yielding ManySortedSet of I ; :: thesis: verum