let D be Subcategory of C; D is Categorial
A1:
the carrier of C is categorial
by Def6;
thus
the carrier of D is categorial
CAT_5:def 6 ( ( for a being Object of D
for A being Category st a = A holds
id a = [[A,A],(id A)] ) & ( for m being Morphism of D
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)] ) )
hereby ( ( for m being Morphism of D
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of D
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)] ) )
let a be
Object of
D;
for A being Category st a = A holds
id a = [[A,A],(id A)]let A be
Category;
( a = A implies id a = [[A,A],(id A)] )reconsider b =
a as
Object of
C by CAT_2:6;
assume
a = A
;
id a = [[A,A],(id A)]then
[[A,A],(id A)] = id b
by Def6;
hence
id a = [[A,A],(id A)]
by CAT_2:def 4;
verum
end;
hereby for m1, m2 being Morphism of D
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)]
let m be
Morphism of
D;
for a, b being Category st a = dom m & b = cod m holds
ex F being Functor of a,b st m = [[a,b],F]reconsider m9 =
m as
Morphism of
C by CAT_2:8;
let a,
b be
Category;
( a = dom m & b = cod m implies ex F being Functor of a,b st m = [[a,b],F] )assume that A2:
a = dom m
and A3:
b = cod m
;
ex F being Functor of a,b st m = [[a,b],F]A4:
dom m9 = a
by A2, CAT_2:9;
cod m9 = b
by A3, CAT_2:9;
hence
ex
F being
Functor of
a,
b st
m = [[a,b],F]
by A4, Def6;
verum
end;
let m1, m2 be Morphism of D; for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)]
let a, b, c be Category; for F being Functor of a,b
for G being Functor of b,c st m1 = [[a,b],F] & m2 = [[b,c],G] holds
m2 (*) m1 = [[a,c],(G * F)]
reconsider m19 = m1, m29 = m2 as Morphism of C by CAT_2:8;
let f be Functor of a,b; for G being Functor of b,c st m1 = [[a,b],f] & m2 = [[b,c],G] holds
m2 (*) m1 = [[a,c],(G * f)]
let g be Functor of b,c; ( m1 = [[a,b],f] & m2 = [[b,c],g] implies m2 (*) m1 = [[a,c],(g * f)] )
assume that
A5:
m1 = [[a,b],f]
and
A6:
m2 = [[b,c],g]
; m2 (*) m1 = [[a,c],(g * f)]
A7:
dom m2 = dom m29
by CAT_2:9;
A8:
cod m1 = cod m19
by CAT_2:9;
A9:
dom m29 = m2 `11
by Th13;
A10:
cod m19 = m1 `12
by Th13;
A11:
dom m2 = b
by A6, A7, A9, MCART_1:85;
cod m1 = b
by A5, A8, A10, MCART_1:85;
hence m2 (*) m1 =
m29 (*) m19
by A11, CAT_2:11
.=
[[a,c],(g * f)]
by A5, A6, Def6
;
verum