let C1, C2 be Categorial Category; ( 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
; 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;
then A7:
the Source of C1 = the Source of C2
by A2, A3, A4;
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
now 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 ;
( [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
;
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
;
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; verum