let V be non empty set ; :: thesis: for W being non empty Subset of V holds Ens W is full Subcategory of Ens V
let W be non empty Subset of V; :: thesis: Ens W is full Subcategory of Ens V
reconsider E = Ens W as Subcategory of Ens V by Lm7;
for a, b being Object of E
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 E; :: 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 A1: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)
reconsider aa = a, bb = b as Element of (Ens W) ;
( Hom (aa,bb) = Maps ((@ aa),(@ bb)) & Hom (a9,b9) = Maps ((@ a9),(@ b9)) ) by Th26;
hence Hom (a,b) = Hom (a9,b9) by A1, Lm5; :: thesis: verum

end;

hence Ens W is full Subcategory of Ens V by CAT_2:def 6; :: thesis: verum