let C, D be Category; ( 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 #)
; ( 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)]
; CAT_5:def 6 D is Categorial
thus
the carrier of D is categorial
by A1, A2; CAT_5:def 6 ( ( 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)]
( ( 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;
for A being Category st a = A holds
id a = [[A,A],(id A)]let A be
Category;
( a = A implies id a = [[A,A],(id A)] )
reconsider b =
a as
Object of
C by A1;
assume
a = A
;
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;
verum
end;
hereby 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;
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;
( 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
;
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;
verum
end;
let m1, m2 be 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)]
reconsider f1 = m1, f2 = m2 as Morphism of C by A1;
let a, b, c be 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 F be 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 G be Functor of b,c; ( 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]
; 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
;
verum