for x being set st x in rng (p ^ q) holds
x is non empty multMagma

proof

let x be set ; :: thesis: ( x in rng (p ^ q) implies x is non empty multMagma )
assume x in rng (p ^ q) ; :: thesis: x is non empty multMagma
then x in (rng p) \/ (rng q) by FINSEQ_1:31;

per cases then ( x in rng p or x in rng q ) by XBOOLE_0:def 3;

suppose x in rng p ; :: thesis: x is non empty multMagma

hence x is non empty multMagma by Def1; :: thesis: verum

end;

suppose x in rng q ; :: thesis: x is non empty multMagma

hence x is non empty multMagma by Def1; :: thesis: verum

end;

end;

end;

hence p ^ q is multMagma-yielding ; :: thesis: verum