consider R being PLS;
take I --> R ; :: thesis: I --> R is PLS-yielding
let v be set ; :: according to PENCIL_1:def 19 :: thesis: ( v in rng (I --> R) implies v is PLS )
assume A1: v in rng (I --> R) ; :: thesis: v is PLS
rng (I --> R) c= {R} by FUNCOP_1:19;
hence v is PLS by A1, TARSKI:def 1; :: thesis: verum