dom F = dom (the_Source_of F) by Def6;
hence the_Source_of F is empty ; :: thesis: verum