consider R being Relation;
set f = I --> R;
A1: dom (I --> R) = I by FUNCOP_1:19;
reconsider f = I --> R as ManySortedSet of I ;
take f ; :: thesis: f is Relation-yielding
for x being set st x in dom f holds
f . x is Relation by A1, FUNCOP_1:13;
hence f is Relation-yielding by Def1; :: thesis: verum