take C ; :: thesis: ( the carrier of C c= the carrier of C & ( for a, b, a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of C c= the Comp of C & ( for a, a' being Object of C st a = a' holds
id a = id a' ) )
thus ( the carrier of C c= the carrier of C & ( for a, b, a', b' being Object of C st a = a' & b = b' holds
Hom a,b c= Hom a',b' ) & the Comp of C c= the Comp of C & ( for a, a' being Object of C st a = a' holds
id a = id a' ) ) ; :: thesis: verum