dom f = {} ;
then dom [:g,f:] = [:(dom g),{}:] by FUNCT_3:def 9;
hence [:g,f:] is empty by ZFMISC_1:113; :: thesis: verum