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 object ; :: 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;
A2: dom i = i `11 by Th13;
dom (id a) = i `11 by Th13;
hence x in the carrier of D by A2; :: 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
A3: a = a9 and
A4: b = b9 ; :: thesis: Hom (a,b) c= Hom (a9,b9)
thus Hom (a,b) c= Hom (a9,b9) :: thesis: verum

proof

let x be object ; :: 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
A5: x = f and
A6: dom f = a and
A7: cod f = b ;
reconsider A = a, B = b as Category by Th12;
A8: ex F being Functor of A,B st f = [[A,B],F] by A6, A7, Def6;
reconsider f = f as Morphism of D by A1;
A9: dom f = f `11 by Th13;
A10: cod f = f `12 by Th13;
A11: f `11 = A by A8, MCART_1:85;
f `12 = B by A8, MCART_1:85;
hence x in Hom (a9,b9) by A3, A4, A5, A9, A10, A11; :: thesis: verum

end;

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of C or x in dom the Comp of D )
assume A13: 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;
A14: x = [g,f] by A13, MCART_1:21;
then A15: dom g = cod f by A13, CAT_1:15;
A16: dom g = g `11 by Th13;
A17: dom g9 = g `11 by Th13;
A18: cod f = f `12 by Th13;
cod f9 = f `12 by Th13;
hence x in dom the Comp of D by A14, A15, A16, A17, A18, CAT_1:15; :: thesis: verum

end;

now :: thesis: for x being object st x in dom the Comp of C holds
the Comp of C . x = the Comp of D . x

let x be object ; :: thesis: ( x in dom the Comp of C implies the Comp of C . x = the Comp of D . x )
assume A19: 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;
A20: x = [g,f] by A19, MCART_1:21;
A21: dom g = g `11 by Th13;
cod g = g `12 by Th13;
then consider G being Functor of g `11 ,g `12 such that
A22: g = [[(g `11),(g `12)],G] by A21, Def6;
A23: dom f = f `11 by Th13;
cod f = dom g by A19, A20, CAT_1:15;
then consider F being Functor of f `11 ,g `11 such that
A24: f = [[(f `11),(g `11)],F] by A21, A23, Def6;
thus the Comp of C . x = the Comp of C . (g,f) by A19, MCART_1:21
.= g (*) f by A19, A20, CAT_1:def 1
.= [[(f `11),(g `12)],(G * F)] by A22, A24, Def6
.= g9 (*) f9 by A22, A24, Def6
.= the Comp of D . (g,f) by A12, A19, A20, CAT_1:def 1
.= the Comp of D . x by A19, MCART_1:21 ; :: thesis: verum

end;

hence the Comp of C c= the Comp of D by A12, 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 A25: 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 A25, Def6 ; :: thesis: verum