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