dom F = dom (the_Target_of F) by Def7;
hence not the_Target_of F is empty ; :: thesis: verum