let X, Y be set ; :: thesis: for f, g being Function of X,Y st ( Y = {} implies X = {} ) holds
f +* g = g
let f, g be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies f +* g = g )
assume ( Y = {} implies X = {} ) ; :: thesis: f +* g = g
then ( dom f = X & dom g = X ) by FUNCT_2:def 1;
hence f +* g = g by Th20; :: thesis: verum