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 ; :: 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 b1, b2 being Element of the carrier of (Ens W)
for b3, b4 being Element of the carrier of (Ens V) holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (Ens W) c= the Comp of (Ens V) & ( for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )

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 b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )

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 ;
reconsider m19 = m1, m29 = m2 as Element of Maps V by ;
A7: ( dom m29 = dom m2 & cod m19 = cod m1 ) ;
dom m2 = cod m1 by ;
hence [x,y] in dom the Comp of (Ens V) by ; :: 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 ;
reconsider m19 = m1, m29 = m2 as Element of Maps V by ;
A10: dom m29 = cod m19 by A4, A8, A9, Def11;
A11: dom m2 = cod m1 by ;
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 ;
hence the Comp of (Ens W) . x = m29 * m19 by
.= the Comp of (Ens V) . x by ;
:: thesis: verum
end;
hence the Comp of (Ens W) c= the Comp of (Ens V) by GRFUNC_1:2; :: thesis: for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 )

let a be Object of (Ens W); :: thesis: for b1 being Element of the carrier of (Ens V) holds
( not a = b1 or id a = id b1 )

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
.= id a9 by Th28 ;
:: thesis: verum