consider R being non empty reflexive RelStr ;
set J = I --> R;
A2: rng (I --> R) c= {R} by FUNCOP_1:19;
reconsider J = I --> R as ManySortedSet of I ;
take J ; :: thesis: ( J is RelStr-yielding & J is non-Empty & J is reflexive-yielding )
thus J is RelStr-yielding ; :: thesis: ( J is non-Empty & J is reflexive-yielding )
thus J is non-Empty :: thesis: J is reflexive-yielding

proof

let S be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( S in rng J implies not S is empty )
assume S in rng J ; :: thesis: not S is empty
hence not S is empty by A2, TARSKI:def 1; :: thesis: verum

end;

let S be RelStr ; :: according to WAYBEL_3:def 8 :: thesis: ( S in rng J implies S is reflexive )
assume S in rng J ; :: thesis: S is reflexive
hence S is reflexive by A2, TARSKI:def 1; :: thesis: verum