:: deftheorem Def1 defines multMagma-yielding GROUP_7:def 1 :
for R being Relation holds
( R is multMagma-yielding iff for y being set st y in rng R holds
y is non empty multMagma );