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 )
A1: rng (I --> R) c= {R} by FUNCOP_1:19;
assume v in rng (I --> R) ; :: thesis: v is PLS
hence v is PLS by A1, TARSKI:def 1; :: thesis: verum