reconsider C = D as Subcategory of D by Th8;
take C ; :: thesis: C is full
let c1, c2 be Object of C; :: according to CAT_2:def 6 :: thesis: for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2)
let d1, d2 be Object of D; :: thesis: ( c1 = d1 & c2 = d2 implies Hom (c1,c2) = Hom (d1,d2) )
assume ( c1 = d1 & c2 = d2 ) ; :: thesis: Hom (c1,c2) = Hom (d1,d2)
hence Hom (c1,c2) = Hom (d1,d2) ; :: thesis: verum