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;
( dom (id a) = a & dom i = i `11 & dom (id a) = i `11 ) by Th13, CAT_1:44;
hence x in the carrier of D ; :: 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 a', b' being Object of D st a = a' & b = b' holds
Hom a,b c= Hom a',b'
let a', b' be Object of D; :: thesis: ( a = a' & b = b' implies Hom a,b c= Hom a',b' )
assume A2: ( a = a' & b = b' ) ; :: thesis: Hom a,b c= Hom a',b'
thus Hom a,b c= Hom a',b' :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom a,b or x in Hom a',b' )
assume x in Hom a,b ; :: thesis: x in Hom a',b'
then consider f being Morphism of C such that
A3: ( x = f & dom f = a & cod f = b ) ;
reconsider A = a, B = b as Category by Th12;
consider F being Functor of A,B such that
A4: f = [[A,B],F] by A3, Def6;
reconsider f = f as Morphism of D by A1, TARSKI:def 3;
( dom f = f `11 & cod f = f `12 & f `11 = A & f `12 = B ) by A4, Th13, MCART_1:89;
hence x in Hom a',b' by A2, A3; :: thesis: verum

end;

end;

A5: 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 A6: 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 g' = g, f' = f as Morphism of D by A1, TARSKI:def 3;
A7: x = [g,f] by A6, MCART_1:23;
then ( dom g = cod f & dom g = g `11 & dom g' = g `11 & cod f = f `12 & cod f' = f `12 ) by A6, Th13, CAT_1:40;
hence x in dom the Comp of D by A7, CAT_1:40; :: 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 A8: 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 g' = g, f' = f as Morphism of D by A1, TARSKI:def 3;
A9: x = [g,f] by A8, MCART_1:23;
A10: ( dom g = g `11 & cod g = g `12 ) by Th13;
then consider G being Functor of g `11 ,g `12 such that
A11: g = [[(g `11 ),(g `12 )],G] by Def6;
( dom f = f `11 & cod f = f `12 & cod f = dom g ) by A8, A9, Th13, CAT_1:40;
then consider F being Functor of f `11 ,g `11 such that
A12: f = [[(f `11 ),(g `11 )],F] by A10, Def6;
thus the Comp of C . x = the Comp of C . g,f by A8, MCART_1:23
.= g * f by A8, A9, CAT_1:def 4
.= [[(f `11 ),(g `12 )],(G * F)] by A11, A12, Def6
.= g' * f' by A11, A12, Def6
.= the Comp of D . g,f by A5, A8, A9, CAT_1:def 4
.= the Comp of D . x by A8, MCART_1:23 ; :: thesis: verum

end;

hence the Comp of C c= the Comp of D by A5, GRFUNC_1:8; :: 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 a' be Object of D; :: thesis: ( not a = a' or id a = id a' )
assume A13: a = a' ; :: thesis: id a = id a'
reconsider A = a as Category by Th12;
thus id a = [[A,A],(id A)] by Def6
.= id a' by A13, Def6 ; :: thesis: verum