set A = the 1-sorted ;
set f = I --> the 1-sorted ;
reconsider f = I --> the 1-sorted as ManySortedSet of I ;
take f ; :: thesis: f is 1-sorted-yielding
thus f is 1-sorted-yielding by FUNCOP_1:7; :: thesis: verum