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