set R = the Relation;
set f = I --> the Relation;
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 FUNCOP_1:7;
hence f is Relation-yielding ; :: thesis: verum