let C1, C2 be strict with_triple-like_morphisms Category; ( the carrier of C1 = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) & the carrier of C2 = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) implies C1 = C2 )
assume that
A1:
the carrier of C1 = F1()
and
A2:
for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C1
and
A3:
for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] )
and
A4:
for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)]
and
A5:
the carrier of C2 = F1()
and
A6:
for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C2
and
A7:
for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] )
and
A8:
for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)]
; C1 = C2
A9:
the carrier' of C1 = the carrier' of C2
A10:
dom the Source of C1 = the carrier' of C1
by FUNCT_2:def 1;
A11:
dom the Source of C2 = the carrier' of C2
by FUNCT_2:def 1;
A12:
dom the Target of C1 = the carrier' of C1
by FUNCT_2:def 1;
A13:
dom the Target of C2 = the carrier' of C2
by FUNCT_2:def 1;
then A15:
the Source of C1 = the Source of C2
by A9, A10, A11;
then A16:
the Target of C1 = the Target of C2
by A9, A12, A13;
A17:
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 A22:
[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 A9;
consider a1,
b1 being
Element of
F1(),
f1 being
Element of
F2()
such that A23:
g1 = [[a1,b1],f1]
and
P1[
a1,
b1,
f1]
by A3;
consider c1,
d1 being
Element of
F1(),
i1 being
Element of
F2()
such that A24:
h1 = [[c1,d1],i1]
and
P1[
c1,
d1,
i1]
by A3;
A25:
a1 =
g1 `11
by A23, MCART_1:85
.=
dom g1
by Th2
.=
cod h1
by A22, CAT_1:15
.=
h1 `12
by Th2
.=
d1
by A24, MCART_1:85
;
thus the
Comp of
C1 . (
x,
y) =
g1 (*) h1
by A22, CAT_1:def 1
.=
[[c1,b1],F3(f1,i1)]
by A4, A23, A24, A25
.=
g2 (*) h2
by A8, A23, A24, A25
.=
the
Comp of
C2 . (
x,
y)
by A17, A22, CAT_1:def 1
;
verum end;
hence
C1 = C2
by A1, A5, A9, A15, A16, A17, BINOP_1:20; verum