take F = I --> (id c); :: thesis: cods F = I --> c
cods F = I --> (cod (id c)) by Th9;
hence cods F = I --> c by CAT_1:19; :: thesis: verum