take F = I --> (id a); :: thesis: doms F = I --> a
doms F = I --> (dom (id a)) by Th8;
hence doms F = I --> a by CAT_1:19; :: thesis: verum