set h = f +* g;
A1: dom (f +* g) = (dom f) \/ (dom g) by Def1;
not {} in rng (f +* g)

assume {} in rng (f +* g) ; :: thesis:
then consider x being object such that
A2: ( x in dom (f +* g) & {} = (f +* g) . x ) by FUNCT_1:def 3;
( not x in dom g or x in dom g ) ;
then ( ( {} = f . x & x in dom f ) or ( {} = g . x & x in dom g ) ) by A1, A2, Def1, XBOOLE_0:def 3;
then ( {} in rng f or {} in rng g ) by FUNCT_1:def 3;
hence contradiction by RELAT_1:def 9; :: thesis:

end;