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,the Id of C #) = CatStr(# the carrier of D,the carrier' of D,the Source of D,the Target of D,the Comp of D,the Id 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,the Id of C #) = CatStr(# the carrier of D,the carrier' of D,the Source of D,the Target of D,the Comp of D,the Id 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)] ) )

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 A1;
assume a = A ; :: thesis: id a = [[A,A],(id A)]
then [[A,A],(id A)] = id b by A3
.= the Id of C . b ;
hence id a = [[A,A],(id A)] by A1; :: 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 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 ( A = dom m & B = cod m ) ; :: thesis: ex F being Functor of A,B st m = [[A,B],F]
then ( A = dom m' & B = cod m' ) by A1;
hence ex F being Functor of A,B st m = [[A,B],F] by A4; :: 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 A6: ( m1 = [[a,b],F] & 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, Def5;
consider F1 being Functor of a1,b1 such that
A7: f1 = [[a1,b1],F1] by A4;
consider F2 being Functor of a2,b2 such that
A8: f2 = [[a2,b2],F2] by A4;
( dom f2 = m2 `11 & m2 `11 = b & cod f1 = m1 `12 & m1 `12 = b ) by A6, A7, A8, MCART_1:89;
then A9: [f2,f1] in dom the Comp of C by CAT_1:40;
hence m2 * m1 = the Comp of D . m2,m1 by A1, CAT_1:def 4
.= f2 * f1 by A1, A9, CAT_1:def 4
.= [[a,c],(G * F)] by A5, A6 ;
:: thesis: verum