for y being set st y in rng (X --> M) holds
y is non empty multMagma by TARSKI:def 1;
hence X --> M is multMagma-yielding ; :: thesis: verum