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;