let IT be Function; :: thesis: ( IT is Group-yielding implies IT is multMagma-yielding )
assume IT is Group-yielding ; :: thesis: IT is multMagma-yielding
then for x being set st x in rng IT holds
x is non empty multMagma ;
hence IT is multMagma-yielding by GROUP_7:def 1; :: thesis: verum