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