dom ^^^g,f__ = dom f by Def6
.= {} ;
hence ^^^g,f__ is empty ; :: thesis: verum