A1: the Target of C . (id o) = cod (id o)
.= o ;
A2: o in {o} by TARSKI:def 1;
dom the Target of C = the carrier' of C by FUNCT_2:def 1;
hence not Hom o is empty by A1, A2, FUNCT_1:def 7; :: thesis: verum