let C1, C2 be strict Category; ( the carrier of C1 = Funct (A,B) & the carrier' of C1 = NatTrans (A,B) & ( for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1 ) & ( for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) & the carrier of C2 = Funct (A,B) & the carrier' of C2 = NatTrans (A,B) & ( for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2 ) & ( for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) implies C1 = C2 )
assume that
A127:
the carrier of C1 = Funct (A,B)
and
A128:
the carrier' of C1 = NatTrans (A,B)
and
A129:
for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 )
and
A130:
for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1
and
A131:
for f, g being Morphism of C1 st [g,f] in dom the Comp of C1 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C1 . [g,f] = [[F,F2],(t1 `*` t)] )
and
for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
and
A132:
the carrier of C2 = Funct (A,B)
and
A133:
the carrier' of C2 = NatTrans (A,B)
and
A134:
for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 )
and
A135:
for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2
and
A136:
for f, g being Morphism of C2 st [g,f] in dom the Comp of C2 holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C2 . [g,f] = [[F,F2],(t1 `*` t)] )
and
for a being Object of C2
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
; C1 = C2
A137:
the Target of C1 = the Target of C2
A138:
now ( dom the Comp of C1 = dom the Comp of C2 & ( for x being object st x in dom the Comp of C1 holds
the Comp of C1 . x = the Comp of C2 . x ) )reconsider S1 =
dom the
Comp of
C1,
S2 =
dom the
Comp of
C2 as
Subset of
[: the carrier' of C1, the carrier' of C1:] by A128, A133, RELAT_1:def 18;
A139:
now for x being Element of [: the carrier' of C1, the carrier' of C1:] holds
( x in S1 iff x in S2 )let x be
Element of
[: the carrier' of C1, the carrier' of C1:];
( x in S1 iff x in S2 )A140:
x = [(x `1),(x `2)]
by MCART_1:21;
then reconsider f1 =
x `2 ,
g1 =
x `1 as
Morphism of
C1 by ZFMISC_1:87;
reconsider f2 =
x `2 ,
g2 =
x `1 as
Morphism of
C2 by A128, A133, A140, ZFMISC_1:87;
A141:
now ( [g2,f2] in S2 implies [g1,f1] in S1 )assume
[g2,f2] in S2
;
[g1,f1] in S1then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A142:
f2 = [[F,F1],t]
and A143:
g2 = [[F1,F2],t1]
and
the
Comp of
C2 . [g2,f2] = [[F,F2],(t1 `*` t)]
by A136;
dom g1 =
(g1 `1) `1
by A129
.=
[F1,F2] `1
by A143
.=
[F,F1] `2
.=
(f2 `1) `2
by A142
.=
cod f1
by A129
;
hence
[g1,f1] in S1
by A130;
verum end; now ( [g1,f1] in S1 implies [g2,f2] in S2 )assume
[g1,f1] in S1
;
[g2,f2] in S2then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A144:
f1 = [[F,F1],t]
and A145:
g1 = [[F1,F2],t1]
and
the
Comp of
C1 . [g1,f1] = [[F,F2],(t1 `*` t)]
by A131;
dom g2 =
(g2 `1) `1
by A134
.=
[F1,F2] `1
by A145
.=
[F,F1] `2
.=
(f1 `1) `2
by A144
.=
cod f2
by A134
;
hence
[g2,f2] in S2
by A135;
verum end; hence
(
x in S1 iff
x in S2 )
by A141, MCART_1:21;
verum end; hence
dom the
Comp of
C1 = dom the
Comp of
C2
by SUBSET_1:3;
for x being object st x in dom the Comp of C1 holds
the Comp of C1 . x = the Comp of C2 . xlet x be
object ;
( x in dom the Comp of C1 implies the Comp of C1 . x = the Comp of C2 . x )assume A146:
x in dom the
Comp of
C1
;
the Comp of C1 . x = the Comp of C2 . x
dom the
Comp of
C1 c= [: the carrier' of C1, the carrier' of C1:]
by RELAT_1:def 18;
then reconsider f =
x `2 ,
g =
x `1 as
Morphism of
C1 by A146, MCART_1:10;
A147:
[g,f] = x
by A146, MCART_1:21;
then consider F9,
F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A148:
f = [[F9,F19],t9]
and A149:
g = [[F19,F29],t19]
and A150:
the
Comp of
C2 . [g,f] = [[F9,F29],(t19 `*` t9)]
by A128, A133, A136, A139, A146;
consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A151:
f = [[F,F1],t]
and A152:
g = [[F1,F2],t1]
and A153:
the
Comp of
C1 . [g,f] = [[F,F2],(t1 `*` t)]
by A131, A146, A147;
A154:
[F,F1] = [F9,F19]
by A151, A148, XTUPLE_0:1;
then A155:
F = F9
by XTUPLE_0:1;
[F1,F2] = [F19,F29]
by A152, A149, XTUPLE_0:1;
then A156:
F2 = F29
by XTUPLE_0:1;
A157:
F1 = F19
by A154, XTUPLE_0:1;
t = t9
by A151, A148, XTUPLE_0:1;
hence
the
Comp of
C1 . x = the
Comp of
C2 . x
by A147, A152, A153, A149, A150, A155, A157, A156, XTUPLE_0:1;
verum end;
the Source of C1 = the Source of C2
hence
C1 = C2
by A127, A132, A137, A138, FUNCT_1:2; verum