set R1 = the Relation;
set I = the carrier of R;
set f = the carrier of R --> the Relation;
reconsider f = the carrier of R --> the Relation as ManySortedSet of the carrier of R ;
f is order-sorted ;
then reconsider f = f as OrderSortedSet of R ;
take f ; :: thesis: f is Relation-yielding
for x being object st x in dom f holds
f . x is Relation by FUNCOP_1:7;
hence f is Relation-yielding by FUNCOP_1:def 11; :: thesis: verum