let V be non empty set ; :: thesis: for W being non empty Subset of holds Ens W is_full_subcategory_of Ens V
let W be non empty Subset of ; :: thesis: Ens W is_full_subcategory_of Ens V
A1: for a, b being Object of
for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b'

proof

let a, b be Object of ; :: thesis: for a', b' being Object of st a = a' & b = b' holds
Hom a,b = Hom a',b'
let a', b' be Object of ; :: thesis: ( a = a' & b = b' implies Hom a,b = Hom a',b' )
assume A2: ( a = a' & b = b' ) ; :: thesis: Hom a,b = Hom a',b'
( Hom a,b = Maps (@ a),(@ b) & Hom a',b' = Maps (@ a'),(@ b') ) by Th27;
hence Hom a,b = Hom a',b' by A2, Lm5; :: thesis: verum

end;

thus Ens W is Subcategory of Ens V :: according to CAT_2:def 6 :: 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₂ = Hom b₃,b₄ )

proof

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
for a', b' being Object of st a = a' & b = b' holds
Hom a,b c= Hom a',b' 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

A3: dom the Comp of (Ens W) c= [:(Maps W),(Maps W):] by RELAT_1:def 18;
A4: Maps W c= Maps V by Th7;
thus A5: dom the Comp of (Ens W) c= dom the Comp of (Ens V) :: thesis: for x being set 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 set ; :: 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 A6: [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
A7: [x,y] = [m2,m1] by A3, DOMAIN_1:9;
reconsider m1' = m1, m2' = m2 as Element of Maps V by A4, TARSKI:def 3;
A8: ( dom m2' = dom m2 & cod m1' = cod m1 ) ;
dom m2 = cod m1 by A6, A7, Def12;
hence [x,y] in dom the Comp of (Ens V) by A7, A8, Def12; :: thesis: verum

end;

let x be set ; :: thesis: ( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )
assume A9: 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
A10: x = [m2,m1] by A3, DOMAIN_1:9;
reconsider m1' = m1, m2' = m2 as Element of Maps V by A4, TARSKI:def 3;
A11: dom m2' = cod m1' by A5, A9, A10, Def12;
A12: dom m2 = cod m1 by A9, A10, Def12;
then A13: m2 * m1 = [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] by Def7;
( dom m1 = dom m1' & cod m2 = cod m2' ) ;
then m2' * m1' = [[(dom m1),(cod m2)],((m2 `2 ) * (m1 `2 ))] by A11, Def7;
hence the Comp of (Ens W) . x = m2' * m1' by A10, A12, A13, Def12
.= the Comp of (Ens V) . x by A10, A11, Def12 ;
:: thesis: verum

end;

hence the Comp of (Ens W) c= the Comp of (Ens V) by GRFUNC_1:8; :: 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 ; :: thesis: for b₁ being Element of the carrier of (Ens V) holds
( not a = b₁ or id a = id b₁ )
let a' be Object of ; :: thesis: ( not a = a' or id a = id a' )
A14: id$ (@ a) = [[(@ a),(@ a)],(id (@ a))] ;
assume a = a' ; :: thesis: id a = id a'
hence id a = id$ (@ a') by A14, Def13
.= id a' by Def13 ;
:: thesis: verum

end;

thus 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₂ = Hom b₃,b₄ ) by A1; :: thesis: verum