let F be Function; :: thesis: ( F is Univ_Alg-yielding implies F is 1-sorted-yielding )
assume F is Univ_Alg-yielding ; :: thesis: F is 1-sorted-yielding
then for x being set st x in dom F holds
F . x is 1-sorted by Def10;
hence F is 1-sorted-yielding by Def11; :: thesis: verum