let X, Y be set ; :: thesis: for f, g being Function of X,Y holds f +* g = g
let f, g be Function of X,Y; :: thesis: f +* g = g

per cases not ( Y = {} & not X = {} & not ( Y = {} & X <> {} ) ) ;

suppose ( Y = {} implies X = {} ) ; :: thesis: f +* g = g

then ( dom f = X & dom g = X ) by FUNCT_2:def 1;
hence f +* g = g by Th19; :: thesis: verum

end;

suppose ( Y = {} & X <> {} ) ; :: thesis: f +* g = g

then ( f = {} & g = {} ) ;
hence f +* g = g ; :: thesis: verum

end;

end;