let C, D be Categorial Category; :: thesis: ( 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 ; :: thesis: C is Subcategory of D
thus the carrier of C c= the carrier of D :: according to CAT_2:def 4 :: thesis: ( ( for b₁, b₂ being Element of the carrier of C
for b₃, b₄ being Element of the carrier of D holds
( not b₁ = b₃ or not b₂ = b₄ or Hom (b₁,b₂) c= Hom (b₃,b₄) ) ) & the Comp of C c= the Comp of D & ( for b₁ being Element of the carrier of C
for b₂ being Element of the carrier of D holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of C or x in the carrier of D )
assume x in the carrier of C ; :: thesis: x in the carrier of D
then reconsider a = x as Object of C ;
reconsider i = id a as Morphism of D by A1, TARSKI:def 3;
A2: dom (id a) = a by CAT_1:19;
A3: dom i = i `11 by Th13;
dom (id a) = i `11 by Th13;
hence x in the carrier of D by A2, A3; :: thesis: verum

end;

hereby :: thesis: ( the Comp of C c= the Comp of D & ( for b₁ being Element of the carrier of C
for b₂ being Element of the carrier of D holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

let a, b be Object of C; :: thesis: for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of D; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A4: a = a9 and
A5: b = b9 ; :: thesis: Hom (a,b) c= Hom (a9,b9)
thus Hom (a,b) c= Hom (a9,b9) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume x in Hom (a,b) ; :: thesis: 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:85;
f `12 = B by A9, MCART_1:85;
hence x in Hom (a9,b9) by A4, A5, A6, A10, A11, A12; :: thesis: verum

end;

end;

A13: dom the Comp of C c= dom the Comp of D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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:21;
then A16: dom g = cod f by A14, CAT_1:15;
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:15; :: thesis: verum

end;

now

let x be set ; :: thesis: ( 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 ; :: thesis: the Comp of C . x = the Comp of D . x
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;
A21: x = [g,f] by A20, MCART_1:21;
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:15;
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:21
.= g * f by A20, A21, CAT_1:def 1
.= [[(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 1
.= the Comp of D . x by A20, MCART_1:21 ; :: thesis: verum

end;

hence the Comp of C c= the Comp of D by A13, GRFUNC_1:2; :: thesis: for b₁ being Element of the carrier of C
for b₂ being Element of the carrier of D holds
( not b₁ = b₂ or id b₁ = id b₂ )
let a be Object of C; :: thesis: for b₁ being Element of the carrier of D holds
( not a = b₁ or id a = id b₁ )
let a9 be Object of D; :: thesis: ( not a = a9 or id a = id a9 )
assume A26: a = a9 ; :: thesis: 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 ; :: thesis: verum