let f be Function; :: thesis: ( f is Field-yielding implies f is 1-sorted-yielding )
assume f is Field-yielding ; :: thesis: f is 1-sorted-yielding
then for o being object st o in rng f holds
o is 1-sorted ;
hence f is 1-sorted-yielding by PRALG_1:def 11; :: thesis: verum