let D be Subcategory of C; :: thesis: D is Categorial
A1: the carrier of C is categorial by Def6;
thus the carrier of D is categorial :: according to CAT_5:def 6 :: thesis: ( ( 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)] ) )

proof

let x be Object of D; :: according to CAT_5:def 5 :: thesis: x is Category
x is Object of C by CAT_2:6;
hence x is Category by A1; :: thesis: verum

end;

hereby :: thesis: ( ( 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; :: thesis: for A being Category st a = A holds
id a = [[A,A],(id A)]
let A be Category; :: thesis: ( a = A implies id a = [[A,A],(id A)] )
reconsider b = a as Object of C by CAT_2:6;
assume a = A ; :: thesis: 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; :: thesis: verum

end;

hereby :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

let m1, m2 be Morphism of D; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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] ; :: thesis: 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 ;
:: thesis: verum