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

proof

assume {} in rng (f +* g) ; :: thesis: contradiction
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: verum

end;

hence f +* g is non-empty by RELAT_1:def 9; :: thesis: verum