let A be Category; :: thesis: 1Cat (A,[[A,A],(id A)]) is Categorial
set F = [[A,A],(id A)];
set C = 1Cat (A,[[A,A],(id A)]);
thus for x being Object of (1Cat (A,[[A,A],(id A)])) holds x is Category by TARSKI:def 1; :: according to CAT_5:def 5,CAT_5:def 6 :: thesis: ( ( for a being Object of (1Cat (A,[[A,A],(id A)]))
for A being Category st a = A holds
id a = [[A,A],(id A)] ) & ( for m being Morphism of (1Cat (A,[[A,A],(id A)]))
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 (1Cat (A,[[A,A],(id A)]))
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 (1Cat (A,[[A,A],(id A)]))
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 (1Cat (A,[[A,A],(id A)]))
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 (1Cat (A,[[A,A],(id A)])); :: thesis: for D being Category st a = D holds
id a = [[D,D],(id D)]
let D be Category; :: thesis: ( a = D implies id a = [[D,D],(id D)] )
assume a = D ; :: thesis: id a = [[D,D],(id D)]
then D = A by TARSKI:def 1;
hence id a = [[D,D],(id D)] by TARSKI:def 1; :: thesis: verum

end;

hereby :: thesis: for m1, m2 being Morphism of (1Cat (A,[[A,A],(id A)]))
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 (1Cat (A,[[A,A],(id A)])); :: thesis: for C1, C2 being Category st C1 = dom m & C2 = cod m holds
ex G being Functor of C1,C2 st m = [[C1,C2],G]
let C1, C2 be Category; :: thesis: ( C1 = dom m & C2 = cod m implies ex G being Functor of C1,C2 st m = [[C1,C2],G] )
assume that
A1: C1 = dom m and
A2: C2 = cod m ; :: thesis: ex G being Functor of C1,C2 st m = [[C1,C2],G]
A3: C1 = A by A1, TARSKI:def 1;
A4: C2 = A by A2, TARSKI:def 1;
reconsider G = id A as Functor of C1,C2 by A2, A3, TARSKI:def 1;
take G = G; :: thesis: m = [[C1,C2],G]
thus m = [[C1,C2],G] by A3, A4, TARSKI:def 1; :: thesis: verum

end;

let m1, m2 be Morphism of (1Cat (A,[[A,A],(id A)])); :: 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 A1, B, C be Category; :: thesis: for F being Functor of A1,B
for G being Functor of B,C st m1 = [[A1,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A1,C],(G * F)]
let F1 be Functor of A1,B; :: thesis: for G being Functor of B,C st m1 = [[A1,B],F1] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A1,C],(G * F1)]
let F2 be Functor of B,C; :: thesis: ( m1 = [[A1,B],F1] & m2 = [[B,C],F2] implies m2 (*) m1 = [[A1,C],(F2 * F1)] )
assume that
A5: m1 = [[A1,B],F1] and
A6: m2 = [[B,C],F2] ; :: thesis: m2 (*) m1 = [[A1,C],(F2 * F1)]
A7: [[A1,B],F1] = [[A,A],(id A)] by A5, TARSKI:def 1;
A8: [[B,C],F2] = [[A,A],(id A)] by A6, TARSKI:def 1;
A9: [A1,B] = [A,A] by A7, XTUPLE_0:1;
A10: [A,A] = [B,C] by A8, XTUPLE_0:1;
A11: F1 = id A by A7, XTUPLE_0:1;
A12: F2 = id A by A8, XTUPLE_0:1;
A13: A1 = A by A9, XTUPLE_0:1;
A14: C = A by A10, XTUPLE_0:1;
F2 * F1 = id A by A11, A12, FUNCT_2:17;
hence m2 (*) m1 = [[A1,C],(F2 * F1)] by A13, A14, TARSKI:def 1; :: thesis: verum