let C, D be Category; :: thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) & C is Categorial implies D is Categorial )
assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; :: thesis: ( not C is Categorial or D is Categorial )
assume that
A2: the carrier of C is categorial and
A3: for a being Object of C
for A being Category st a = A holds
id a = [[A,A],(id A)] and
A4: 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] and
A5: 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)] ; :: according to CAT_5:def 6 :: thesis: D is Categorial
thus the carrier of D is categorial by A1, A2; :: 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)] ) )
thus for a being Object of D
for A being Category st a = A holds
id a = [[A,A],(id A)] :: 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)] ) )

proof

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 A1;
assume a = A ; :: thesis: id a = [[A,A],(id A)]
then [[A,A],(id A)] = id b by A3;
hence id a = [[A,A],(id A)] by A1, Lm1; :: 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 A1;
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
A6: A = dom m and
A7: B = cod m ; :: thesis: ex F being Functor of A,B st m = [[A,B],F]
A8: A = dom m9 by A1, A6;
B = cod m9 by A1, A7;
hence ex F being Functor of A,B st m = [[A,B],F] by A4, A8; :: 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)]
reconsider f1 = m1, f2 = m2 as Morphism of C by A1;
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)]
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
A9: m1 = [[a,b],F] and
A10: m2 = [[b,c],G] ; :: thesis: m2 (*) m1 = [[a,c],(G * F)]
reconsider a1 = dom f1, b1 = cod f1, a2 = dom f2, b2 = cod f2 as Category by A2;
A11: ex F1 being Functor of a1,b1 st f1 = [[a1,b1],F1] by A4;
ex F2 being Functor of a2,b2 st f2 = [[a2,b2],F2] by A4;
then A12: dom f2 = m2 `11 by MCART_1:85;
A13: m2 `11 = b by A10, MCART_1:85;
A14: cod f1 = m1 `12 by A11, MCART_1:85;
m1 `12 = b by A9, MCART_1:85;
then A15: [f2,f1] in dom the Comp of C by A12, A13, A14, CAT_1:15;
hence m2 (*) m1 = the Comp of D . (m2,m1) by A1, CAT_1:def 1
.= f2 (*) f1 by A1, A15, CAT_1:def 1
.= [[a,c],(G * F)] by A5, A9, A10 ;
:: thesis: verum