for x being set st x in rng <%M1,M2,M3%> holds
x is non empty multMagma
proof
let x be set ; :: thesis: ( x in rng <%M1,M2,M3%> implies x is non empty multMagma )
assume x in rng <%M1,M2,M3%> ; :: thesis: x is non empty multMagma
then x in {M1,M2,M3} by AFINSQ_1:99;
hence x is non empty multMagma by ENUMSET1:def 1; :: thesis: verum
end;
hence <%M1,M2,M3%> is multMagma-yielding ; :: thesis: verum