theorem :: FUNCT_1:103

for f, g being Function st f is g -compatible & dom f = dom g holds
g is non-empty ;