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