theorem Th14: :: CAT_5:14

for C1, C2 being Categorial Category st the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 holds
CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)