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