for y being set st y in rng (f +* g) holds
y is non empty multMagma

proof

let y be set ; :: thesis: ( y in rng (f +* g) implies y is non empty multMagma )
assume y in rng (f +* g) ; :: thesis: y is non empty multMagma
then y in (rng f) \/ (rng g) by TARSKI:def 3, FUNCT_4:17;

per cases then ( y in rng f or y in rng g ) by XBOOLE_0:def 3;

suppose y in rng f ; :: thesis: y is non empty multMagma

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

end;

suppose y in rng g ; :: thesis: y is non empty multMagma

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

end;

end;

end;

hence f +* g is multMagma-yielding ; :: thesis: verum