take
C
; :: thesis: ( the carrier of C c= the carrier of C & ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds

id a = id a9 ) )

thus ( the carrier of C c= the carrier of C & ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds

id a = id a9 ) ) ; :: thesis: verum

Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds

id a = id a9 ) )

thus ( the carrier of C c= the carrier of C & ( for a, b, a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of C c= the Comp of C & ( for a, a9 being Object of C st a = a9 holds

id a = id a9 ) ) ; :: thesis: verum