let V be non empty set ; :: thesis: for W being non empty Subset of V holds Ens W is Subcategory of Ens V
let W be non empty Subset of V; :: thesis: Ens W is Subcategory of Ens V
A1: for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)

proof

let a, b be Object of (Ens W); :: thesis: for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of (Ens V); :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A2: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)
( Hom (a,b) = Maps ((@ a),(@ b)) & Hom (a9,b9) = Maps ((@ a9),(@ b9)) ) by Th26;
hence Hom (a,b) = Hom (a9,b9) by A2, Lm5; :: thesis: verum

end;

set w = the Comp of (Ens W);
set v = the Comp of (Ens V);
thus the carrier of (Ens W) c= the carrier of (Ens V) ; :: according to CAT_2:def 4 :: thesis: ( ( for b₁, b₂ being Element of the carrier of (Ens W)
for b₃, b₄ being Element of the carrier of (Ens V) holds
( not b₁ = b₃ or not b₂ = b₄ or Hom (b₁,b₂) c= Hom (b₃,b₄) ) ) & the Comp of (Ens W) c= the Comp of (Ens V) & ( for b₁ being Element of the carrier of (Ens W)
for b₂ being Element of the carrier of (Ens V) holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )
thus for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) by A1; :: thesis: ( the Comp of (Ens W) c= the Comp of (Ens V) & ( for b₁ being Element of the carrier of (Ens W)
for b₂ being Element of the carrier of (Ens V) holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

now :: thesis: ( dom the Comp of (Ens W) c= dom the Comp of (Ens V) & ( for x being object st x in dom the Comp of (Ens W) holds
the Comp of (Ens W) . x = the Comp of (Ens V) . x ) )

A3: dom the Comp of (Ens W) c= [:(Maps W),(Maps W):] by RELAT_1:def 18;
thus A4: dom the Comp of (Ens W) c= dom the Comp of (Ens V) :: thesis: for x being object st x in dom the Comp of (Ens W) holds
the Comp of (Ens W) . x = the Comp of (Ens V) . x

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in dom the Comp of (Ens W) or [x,y] in dom the Comp of (Ens V) )
assume A5: [x,y] in dom the Comp of (Ens W) ; :: thesis: [x,y] in dom the Comp of (Ens V)
then consider m2, m1 being Element of Maps W such that
A6: [x,y] = [m2,m1] by A3, DOMAIN_1:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7, TARSKI:def 3;
A7: ( dom m29 = dom m2 & cod m19 = cod m1 ) ;
dom m2 = cod m1 by A5, A6, Def11;
hence [x,y] in dom the Comp of (Ens V) by A6, A7, Def11; :: thesis: verum

end;

let x be object ; :: thesis: ( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )
assume A8: x in dom the Comp of (Ens W) ; :: thesis: the Comp of (Ens W) . x = the Comp of (Ens V) . x
then consider m2, m1 being Element of Maps W such that
A9: x = [m2,m1] by A3, DOMAIN_1:1;
reconsider m19 = m1, m29 = m2 as Element of Maps V by Th7, TARSKI:def 3;
A10: dom m29 = cod m19 by A4, A8, A9, Def11;
A11: dom m2 = cod m1 by A8, A9, Def11;
then A12: m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] by Def6;
( dom m1 = dom m19 & cod m2 = cod m29 ) ;
then m29 * m19 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] by A10, Def6;
hence the Comp of (Ens W) . x = m29 * m19 by A9, A11, A12, Def11
.= the Comp of (Ens V) . x by A9, A10, Def11 ;
:: thesis: verum

end;

hence the Comp of (Ens W) c= the Comp of (Ens V) by GRFUNC_1:2; :: thesis: for b₁ being Element of the carrier of (Ens W)
for b₂ being Element of the carrier of (Ens V) holds
( not b₁ = b₂ or id b₁ = id b₂ )
let a be Object of (Ens W); :: thesis: for b₁ being Element of the carrier of (Ens V) holds
( not a = b₁ or id a = id b₁ )
let a9 be Object of (Ens V); :: thesis: ( not a = a9 or id a = id a9 )
A13: id$ (@ a) = [[(@ a),(@ a)],(id (@ a))] ;
assume a = a9 ; :: thesis: id a = id a9
hence id a = id$ (@ a9) by A13, Th28
.= id a9 by Th28 ;
:: thesis: verum