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

proof

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

end;

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