for x being object st x in rng (f +* g) holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng (f +* g) implies x is 1-sorted )
assume x in rng (f +* g) ; :: thesis: x is 1-sorted
then x in (rng f) \/ (rng g) by TARSKI:def 3, FUNCT_4:17;

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

suppose x in rng f ; :: thesis: x is 1-sorted

hence x is 1-sorted by Def11; :: thesis: verum

end;

suppose x in rng g ; :: thesis: x is 1-sorted

hence x is 1-sorted by Def11; :: thesis: verum

end;

end;

end;

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