consider A being 1-sorted ;
set f = I --> A;
A1: dom (I --> A) = I by FUNCOP_1:19;
then reconsider f = I --> A as ManySortedSet of I by PARTFUN1:def 4;
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:13;
hence f is 1-sorted-yielding by Def11; :: thesis: verum