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 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp 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 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp 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;
now :: thesis: for x being object st x in the carrier' of C1 holds
the Source of C1 . x = the Source of C2 . x
let x be object ; :: 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 A7: the Source of C1 = the Source of C2 by A2, A3, A4;
A8: now :: thesis: for x being object st x in the carrier' of C1 holds
the Target of C1 . x = the Target of C2 . x
let x be object ; :: 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 A9: the Target of C1 = the Target of C2 by A2, A5, A6;
A10: 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 object ; :: thesis: ( x in dom the Comp of C1 implies x in dom the Comp of C2 )
assume A11: 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;
A12: y = [(xx `1),(xx `2)] by MCART_1:21;
then dom (xx `1) = cod (xx `2) by A11, CAT_1:def 6;
then dom (y `1) = cod (y `2) by A8, A7;
hence x in dom the Comp of C2 by A12, CAT_1:def 6; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of C2 or x in dom the Comp of C1 )
assume A13: 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;
A14: xx = [(y `1),(y `2)] by MCART_1:21;
then dom (y `1) = cod (y `2) by A13, CAT_1:def 6;
then dom (xx `1) = cod (xx `2) by A8, A7;
hence x in dom the Comp of C1 by A14, CAT_1:def 6; :: thesis: verum
end;
now :: thesis: for x, y being object st [x,y] in dom the Comp of C1 holds
the Comp of C1 . (x,y) = the Comp of C2 . (x,y)
let x, y be object ; :: thesis: ( [x,y] in dom the Comp of C1 implies the Comp of C1 . (x,y) = the Comp of C2 . (x,y) )
assume A15: [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
A16: 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
A17: h1 = [[c1,d1],i1] by Def6;
A18: a1 = d1 by A15, CAT_1:15;
thus the Comp of C1 . (x,y) = g1 (*) h1 by A15, CAT_1:def 1
.= [[c1,b1],(f1 * i1)] by A16, A17, A18, Def6
.= g2 (*) h2 by A16, A17, A18, Def6
.= the Comp of C2 . (x,y) by A10, A15, CAT_1:def 1 ; :: thesis: verum
end;
then the Comp of C1 = the Comp of C2 by A2, A10, BINOP_1:20;
hence 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 #) by A1, A2, A7, A9; :: thesis: verum