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