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