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