set R = the Relation;
set f = I --> the Relation;
A1: dom (I --> the Relation) = I by FUNCOP_1:13;
reconsider f = I --> the Relation 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:7;
hence f is Relation-yielding by FUNCOP_1:def 11; :: thesis: verum