set A = the 1-sorted ;
set f = I --> the 1-sorted ;
A1: dom (I --> the 1-sorted ) = I by FUNCOP_1:13;
reconsider f = I --> the 1-sorted as ManySortedSet of I ;
take f ; :: thesis: f is 1-sorted-yielding
for i being set st i in dom f holds
f . i is 1-sorted by A1, FUNCOP_1:7;
hence f is 1-sorted-yielding by Def11; :: thesis: verum