let C, D be Categorial Category; ( the carrier' of C c= the carrier' of D implies C is Subcategory of D )
assume A1:
the carrier' of C c= the carrier' of D
; C is Subcategory of D
thus
the carrier of C c= the carrier of D
CAT_2:def 4 ( ( for b1, b2 being Element of the carrier of C
for b3, b4 being Element of the carrier of D holds
( not b1 = b3 or not b2 = b4 or Hom b1,b2 c= Hom b3,b4 ) ) & the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 ) ) )
hereby ( the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 ) ) )
let a,
b be
Object of
C;
for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9let a9,
b9 be
Object of
D;
( a = a9 & b = b9 implies Hom a,b c= Hom a9,b9 )assume that A4:
a = a9
and A5:
b = b9
;
Hom a,b c= Hom a9,b9thus
Hom a,
b c= Hom a9,
b9
verumproof
let x be
set ;
TARSKI:def 3 ( not x in Hom a,b or x in Hom a9,b9 )
assume
x in Hom a,
b
;
x in Hom a9,b9
then consider f being
Morphism of
C such that A6:
x = f
and A7:
dom f = a
and A8:
cod f = b
;
reconsider A =
a,
B =
b as
Category by Th12;
A9:
ex
F being
Functor of
A,
B st
f = [[A,B],F]
by A7, A8, Def6;
reconsider f =
f as
Morphism of
D by A1, TARSKI:def 3;
A10:
dom f = f `11
by Th13;
A11:
cod f = f `12
by Th13;
A12:
f `11 = A
by A9, MCART_1:89;
f `12 = B
by A9, MCART_1:89;
hence
x in Hom a9,
b9
by A4, A5, A6, A10, A11, A12;
verum
end;
end;
A13:
dom the Comp of C c= dom the Comp of D
proof
let x be
set ;
TARSKI:def 3 ( not x in dom the Comp of C or x in dom the Comp of D )
assume A14:
x in dom the
Comp of
C
;
x in dom the Comp of D
then reconsider g =
x `1 ,
f =
x `2 as
Morphism of
C by MCART_1:10;
reconsider g9 =
g,
f9 =
f as
Morphism of
D by A1, TARSKI:def 3;
A15:
x = [g,f]
by A14, MCART_1:23;
then A16:
dom g = cod f
by A14, CAT_1:40;
A17:
dom g = g `11
by Th13;
A18:
dom g9 = g `11
by Th13;
A19:
cod f = f `12
by Th13;
cod f9 = f `12
by Th13;
hence
x in dom the
Comp of
D
by A15, A16, A17, A18, A19, CAT_1:40;
verum
end;
now let x be
set ;
( x in dom the Comp of C implies the Comp of C . x = the Comp of D . x )assume A20:
x in dom the
Comp of
C
;
the Comp of C . x = the Comp of D . xthen reconsider g =
x `1 ,
f =
x `2 as
Morphism of
C by MCART_1:10;
reconsider g9 =
g,
f9 =
f as
Morphism of
D by A1, TARSKI:def 3;
A21:
x = [g,f]
by A20, MCART_1:23;
A22:
dom g = g `11
by Th13;
cod g = g `12
by Th13;
then consider G being
Functor of
g `11 ,
g `12 such that A23:
g = [[(g `11 ),(g `12 )],G]
by A22, Def6;
A24:
dom f = f `11
by Th13;
cod f = dom g
by A20, A21, CAT_1:40;
then consider F being
Functor of
f `11 ,
g `11 such that A25:
f = [[(f `11 ),(g `11 )],F]
by A22, A24, Def6;
thus the
Comp of
C . x =
the
Comp of
C . g,
f
by A20, MCART_1:23
.=
g * f
by A20, A21, CAT_1:def 4
.=
[[(f `11 ),(g `12 )],(G * F)]
by A23, A25, Def6
.=
g9 * f9
by A23, A25, Def6
.=
the
Comp of
D . g,
f
by A13, A20, A21, CAT_1:def 4
.=
the
Comp of
D . x
by A20, MCART_1:23
;
verum end;
hence
the Comp of C c= the Comp of D
by A13, GRFUNC_1:8; for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of C; for b1 being Element of the carrier of D holds
( not a = b1 or id a = id b1 )
let a9 be Object of D; ( not a = a9 or id a = id a9 )
assume A26:
a = a9
; id a = id a9
reconsider A = a as Category by Th12;
thus id a =
[[A,A],(id A)]
by Def6
.=
id a9
by A26, Def6
; verum