let C1, C2 be Categorial Category; :: thesis: ( the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 implies 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 #) )
assume that
A1: the carrier of C1 = the carrier of C2 and
A2: the carrier' of C1 = the carrier' of C2 ; :: thesis: 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 #)
A3: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A4: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1;
A5: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A6: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1;
A7: dom the Id of C1 = the carrier of C1 by FUNCT_2:def 1;
A8: dom the Id of C2 = the carrier of C2 by FUNCT_2:def 1;

now

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

end;

then A9: the Source of C1 = the Source of C2 by A2, A3, A4, FUNCT_1:2;

now

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

end;

then A10: the Target of C1 = the Target of C2 by A2, A5, A6, FUNCT_1:2;
A11: dom the Comp of C1 = dom the Comp of C2

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom the Comp of C2 c= dom the Comp of C1

let x be set ; :: thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 )
assume A12: x in dom the Comp of C1 ; :: thesis: x in dom the Comp of C2
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 A2;
A13: y = [(xx `1),(xx `2)] by MCART_1:21;
then the Source of C1 . (xx `1) = the Target of C1 . (xx `2) by A12, CAT_1:def 5;
hence x in dom the Comp of C2 by A2, A9, A10, A13, CAT_1:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 )
assume A14: x in dom the Comp of C2 ; :: thesis: x in dom the Comp of C1
then reconsider xx = x as Element of [: the carrier' of C1, the carrier' of C1:] by A2;
reconsider y = xx as Element of [: the carrier' of C2, the carrier' of C2:] by A2;
A15: xx = [(y `1),(y `2)] by MCART_1:21;
then the Source of C2 . (y `1) = the Target of C2 . (y `2) by A14, CAT_1:def 5;
hence x in dom the Comp of C1 by A2, A9, A10, A15, CAT_1:def 5; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) )
assume A16: [x,y] in dom the Comp of C1 ; :: thesis: the Comp of C1 . (x,y) = the Comp of C2 . (x,y)
then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A2;
reconsider a1 = dom g1, b1 = cod g1 as Category by Th12;
consider f1 being Functor of a1,b1 such that
A17: 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
A18: h1 = [[c1,d1],i1] by Def6;
A19: a1 = d1 by A16, CAT_1:15;
thus the Comp of C1 . (x,y) = g1 * h1 by A16, CAT_1:def 1
.= [[c1,b1],(f1 * i1)] by A17, A18, A19, Def6
.= g2 * h2 by A17, A18, A19, Def6
.= the Comp of C2 . (x,y) by A11, A16, CAT_1:def 1 ; :: thesis: verum

end;

then A20: the Comp of C1 = the Comp of C2 by A2, A11, BINOP_1:20;

now

let x be set ; :: thesis: ( x in the carrier of C1 implies the Id of C1 . x = the Id of C2 . x )
assume x in the carrier of C1 ; :: thesis: the Id of C1 . x = the Id of C2 . x
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: verum

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, A7, A8, A9, A10, A20, FUNCT_1:2; :: thesis: verum