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)

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_{1}, b_{2} being Element of the carrier of (Ens W)

for b_{3}, b_{4} being Element of the carrier of (Ens V) holds

( not b_{1} = b_{3} or not b_{2} = b_{4} or Hom (b_{1},b_{2}) c= Hom (b_{3},b_{4}) ) ) & the Comp of (Ens W) c= the Comp of (Ens V) & ( for b_{1} being Element of the carrier of (Ens W)

for b_{2} being Element of the carrier of (Ens V) holds

( not b_{1} = b_{2} or id b_{1} = id b_{2} ) ) )

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_{1} being Element of the carrier of (Ens W)

for b_{2} being Element of the carrier of (Ens V) holds

( not b_{1} = b_{2} or id b_{1} = id b_{2} ) ) )

_{1} being Element of the carrier of (Ens W)

for b_{2} being Element of the carrier of (Ens V) holds

( not b_{1} = b_{2} or id b_{1} = id b_{2} )

let a be Object of (Ens W); :: thesis: for b_{1} being Element of the carrier of (Ens V) holds

( not a = b_{1} or id a = id b_{1} )

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

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

set w = the Comp of (Ens W);
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;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

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

for b

( not b

for b

( not 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

for b

( not 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 ) )

hence
the Comp of (Ens W) c= the Comp of (Ens V)
by GRFUNC_1:2; :: thesis: for bthe 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

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;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 be object ; :: thesis: ( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )
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;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

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

for b

( not b

let a be Object of (Ens W); :: thesis: for b

( not a = 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