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
A103:
the carrier of C1 = Funct (A,B)
and
A104:
the carrier' of C1 = NatTrans (A,B)
and
A105:
for f being Morphism of C1 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 )
and
A106:
for f, g being Morphism of C1 st dom g = cod f holds
[g,f] in dom the Comp of C1
and
A107:
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
A108:
for a being Object of C1
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
and
A109:
the carrier of C2 = Funct (A,B)
and
A110:
the carrier' of C2 = NatTrans (A,B)
and
A111:
for f being Morphism of C2 holds
( dom f = (f `1) `1 & cod f = (f `1) `2 )
and
A112:
for f, g being Morphism of C2 st dom g = cod f holds
[g,f] in dom the Comp of C2
and
A113:
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
A114:
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
A115:
the Target of C1 = the Target of C2
A116:
now 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 A104, A110, RELAT_1:def 18;
now let x be
Element of
[: the carrier' of C1, the carrier' of C1:];
( x in S1 iff x in S2 )A117:
x = [(x `1),(x `2)]
by MCART_1:23;
then reconsider f1 =
x `2 ,
g1 =
x `1 as
Morphism of
C1 by ZFMISC_1:106;
reconsider f2 =
x `2 ,
g2 =
x `1 as
Morphism of
C2 by A104, A110, A117, ZFMISC_1:106;
A118:
now 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 A119:
f2 = [[F,F1],t]
and A120:
g2 = [[F1,F2],t1]
and
the
Comp of
C2 . [g2,f2] = [[F,F2],(t1 `*` t)]
by A113;
dom g1 =
(g1 `1) `1
by A105
.=
[F1,F2] `1
by A120, MCART_1:7
.=
F1
by MCART_1:7
.=
[F,F1] `2
by MCART_1:7
.=
(f2 `1) `2
by A119, MCART_1:7
.=
cod f1
by A105
;
hence
[g1,f1] in S1
by A106;
verum end; now 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 A121:
f1 = [[F,F1],t]
and A122:
g1 = [[F1,F2],t1]
and
the
Comp of
C1 . [g1,f1] = [[F,F2],(t1 `*` t)]
by A107;
dom g2 =
(g2 `1) `1
by A111
.=
[F1,F2] `1
by A122, MCART_1:7
.=
F1
by MCART_1:7
.=
[F,F1] `2
by MCART_1:7
.=
(f1 `1) `2
by A121, MCART_1:7
.=
cod f2
by A111
;
hence
[g2,f2] in S2
by A112;
verum end; hence
(
x in S1 iff
x in S2 )
by A118, MCART_1:23;
verum end; hence A123:
dom the
Comp of
C1 = dom the
Comp of
C2
by SUBSET_1:8;
for x being set st x in dom the Comp of C1 holds
the Comp of C1 . x = the Comp of C2 . xlet x be
set ;
( x in dom the Comp of C1 implies the Comp of C1 . x = the Comp of C2 . x )assume A124:
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 A124, MCART_1:10;
A126:
[g,f] = x
by A124, MCART_1:23;
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 A127:
f = [[F9,F19],t9]
and A128:
g = [[F19,F29],t19]
and A129:
the
Comp of
C2 . [g,f] = [[F9,F29],(t19 `*` t9)]
by A104, A110, A113, A123, A124;
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 A130:
f = [[F,F1],t]
and A131:
g = [[F1,F2],t1]
and A132:
the
Comp of
C1 . [g,f] = [[F,F2],(t1 `*` t)]
by A107, A124, A126;
A133:
[F,F1] = [F9,F19]
by A130, A127, ZFMISC_1:33;
then A134:
F = F9
by ZFMISC_1:33;
[F1,F2] = [F19,F29]
by A131, A128, ZFMISC_1:33;
then A135:
F2 = F29
by ZFMISC_1:33;
A136:
F1 = F19
by A133, ZFMISC_1:33;
t = t9
by A130, A127, ZFMISC_1:33;
hence
the
Comp of
C1 . x = the
Comp of
C2 . x
by A126, A131, A132, A128, A129, A134, A136, A135, ZFMISC_1:33;
verum end;
A137:
the Id of C1 = the Id of C2
the Source of C1 = the Source of C2
hence
C1 = C2
by A103, A104, A109, A110, A115, A116, A137, FUNCT_1:9; verum