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:9;

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:9;
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:23;
then the Source of C1 . (xx `1 ) = the Target of C1 . (xx `2 ) by A12, CAT_1:def 8;
hence x in dom the Comp of C2 by A2, A9, A10, A13, CAT_1:def 8; :: 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:23;
then the Source of C2 . (y `1 ) = the Target of C2 . (y `2 ) by A14, CAT_1:def 8;
hence x in dom the Comp of C1 by A2, A9, A10, A15, CAT_1:def 8; :: 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:106;
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:40;
thus the Comp of C1 . x,y = g1 * h1 by A16, CAT_1:def 4
.= [[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 4 ; :: thesis: verum

end;

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

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:9; :: thesis: verum