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