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