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