consider R1 being Relation;
set I = the carrier of R;
set f = the carrier of R --> R1;
A1: dom (the carrier of R --> R1) = the carrier of R by FUNCOP_1:19;
then reconsider f = the carrier of R --> R1 as ManySortedSet of the carrier of R by PARTFUN1:def 4;
f is order-sorted

proof

let s1, s2 be Element of R; :: according to OSALG_1:def 18 :: thesis: ( not s1 <= s2 or f . s1 c= f . s2 )
assume s1 <= s2 ; :: thesis: f . s1 c= f . s2
f . s1 = R1 by FUNCOP_1:13;
hence f . s1 c= f . s2 by FUNCOP_1:13; :: thesis: verum

end;

then reconsider f = f as OrderSortedSet of R ;
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 MSUALG_4:def 1; :: thesis: verum