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