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)

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

hence
Ens W is full Subcategory of Ens V
by CAT_2:def 6; :: thesis: verum
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;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