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

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