let C1, C2 be Categorial Category; :: thesis:
assume A1: ( the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 ) ; :: thesis:
A2: ( dom the Source of C1 = the carrier' of C1 & dom the Source of C2 = the carrier' of C2 & dom the Target of C1 = the carrier' of C1 & dom the Target of C2 = the carrier' of C2 & dom the Id of C1 = the carrier of C1 & dom the Id of C2 = the carrier of C2 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume x in the carrier' of C1 ; :: thesis:
then reconsider m1 = x as Morphism of C1 ;
reconsider m2 = m1 as Morphism of C2 by A1;
thus the Source of C1 . x = dom m1
.= m1 `11 by Th13
.= dom m2 by Th13
.= the Source of C2 . x ; :: thesis:

end;

then A3: the Source of C1 = the Source of C2 by A1, A2, FUNCT_1:9;

now

let x be set ; :: thesis:
assume x in the carrier' of C1 ; :: thesis:
then reconsider m1 = x as Morphism of C1 ;
reconsider m2 = m1 as Morphism of C2 by A1;
thus the Target of C1 . x = cod m1
.= m1 `12 by Th13
.= cod m2 by Th13
.= the Target of C2 . x ; :: thesis:

end;

then A4: the Target of C1 = the Target of C2 by A1, A2, FUNCT_1:9;
A5: dom the Comp of C1 = dom the Comp of C2

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be set ; :: thesis:
assume A6: x in dom the Comp of C1 ; :: thesis:
then reconsider xx = x as Element of [:the carrier' of C1,the carrier' of C1:] ;
reconsider y = xx as Element of [:the carrier' of C2,the carrier' of C2:] by A1;
A7: y = [(xx `1 ),(xx `2 )] by MCART_1:23;
then the Source of C1 . (xx `1 ) = the Target of C1 . (xx `2 ) by A6, CAT_1:def 8;
hence x in dom the Comp of C2 by A1, A3, A4, A7, CAT_1:def 8; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in dom the Comp of C2 ; :: thesis:
then reconsider xx = x as Element of [:the carrier' of C1,the carrier' of C1:] by A1;
reconsider y = xx as Element of [:the carrier' of C2,the carrier' of C2:] by A1;
A9: xx = [(y `1 ),(y `2 )] by MCART_1:23;
then the Source of C2 . (y `1 ) = the Target of C2 . (y `2 ) by A8, CAT_1:def 8;
hence x in dom the Comp of C1 by A1, A3, A4, A9, CAT_1:def 8; :: thesis:

end;

now

let x, y be set ; :: thesis:
assume A10: [x,y] in dom the Comp of C1 ; :: thesis:
then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:106;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A1;
reconsider a1 = dom g1, b1 = cod g1 as Category by Th12;
consider f1 being Functor of a1,b1 such that
A11: g1 = [[a1,b1],f1] by Def6;
reconsider c1 = dom h1, d1 = cod h1 as Category by Th12;
consider i1 being Functor of c1,d1 such that
A12: h1 = [[c1,d1],i1] by Def6;
A13: a1 = d1 by A10, CAT_1:40;
thus the Comp of C1 . x,y = g1 * h1 by A10, CAT_1:def 4
.= [[c1,b1],(f1 * i1)] by A11, A12, A13, Def6
.= g2 * h2 by A11, A12, A13, Def6
.= the Comp of C2 . x,y by A5, A10, CAT_1:def 4 ; :: thesis:

end;

then A14: the Comp of C1 = the Comp of C2 by A1, A5, BINOP_1:32;

now

let x be set ; :: thesis:
assume x in the carrier of C1 ; :: thesis:
then reconsider a1 = x as Object of C1 ;
reconsider a2 = a1 as Object of C2 by A1;
reconsider A = a1 as Category by Th12;
thus the Id of C1 . x = id a1
.= [[A,A],(id A)] by Def6
.= id a2 by Def6
.= the Id of C2 . x ; :: thesis:

end;

hence CatStr(# the carrier of C1,the carrier' of C1,the Source of C1,the Target of C1,the Comp of C1,the Id of C1 #) = CatStr(# the carrier of C2,the carrier' of C2,the Source of C2,the Target of C2,the Comp of C2,the Id of C2 #) by A1, A2, A3, A4, A14, FUNCT_1:9; :: thesis: