for x being set st x in rng <%M1%> holds
x is non empty multMagma

proof

let x be set ; :: thesis: ( x in rng <%M1%> implies x is non empty multMagma )
assume x in rng <%M1%> ; :: thesis: x is non empty multMagma
then x in {M1} by AFINSQ_1:33;
hence x is non empty multMagma by TARSKI:def 1; :: thesis: verum

end;

hence <%M1%> is multMagma-yielding ; :: thesis: verum