let D be Subcategory of C; :: thesis: D is Categorial
A1: ( the carrier of C is categorial & ( for m being Morphism of C
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 C
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)] ) ) 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:12;
hence x is Category by A1, Def4; :: 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:12;
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 m' = m as Morphism of C by CAT_2:14;
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 ( a = dom m & b = cod m ) ; :: thesis: ex F being Functor of a,b st m = [[a,b],F]
then ( dom m' = a & cod m' = b ) by CAT_2:15;
hence ex F being Functor of a,b st m = [[a,b],F] by 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 m1' = m1, m2' = m2 as Morphism of C by CAT_2:14;
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 A2: ( m1 = [[a,b],f] & m2 = [[b,c],g] ) ; :: thesis: m2 * m1 = [[a,c],(g * f)]
( dom m2 = dom m2' & cod m1 = cod m1' & dom m2' = m2 `11 & cod m1' = m1 `12 ) by Th13, CAT_2:15;
then ( dom m2 = b & cod m1 = b ) by A2, MCART_1:89;
hence m2 * m1 = m2' * m1' by CAT_2:17
.= [[a,c],(g * f)] by A2, Def6 ;
:: thesis: verum