dom ^^^f,g__ = (dom f) /\ (dom g) by Def7
.= {} ;
hence ^^^f,g__ is empty ; :: thesis: verum