dom f = {} ;
then dom <:g,f:> = {} /\ (dom g) by Def7;
hence <:g,f:> is empty ; :: thesis: verum