let C be Category; :: thesis: for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds
( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds
( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

let M be non empty set ; :: thesis: for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds
( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

let d, c be Function of M,O; :: thesis: for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds
( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

let p be PartFunc of [:M,M:],M; :: thesis: ( CatStr(# O,M,d,c,p #) is full Subcategory of C implies ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M ) )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
set B = CatStr(# O,M,d,c,p #);
assume A1: CatStr(# O,M,d,c,p #) is full Subcategory of C ; :: thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )
A2: for f being Morphism of CatStr(# O,M,d,c,p #) holds
( d . f = the Source of C . f & c . f = the Target of C . f )
proof
let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( d . f = the Source of C . f & c . f = the Target of C . f )
reconsider f9 = f as Morphism of C by ;
( dom f = dom f9 & cod f = cod f9 ) by ;
hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) & ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M ) )
let x be object ; :: thesis: ( ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) & ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M ) )
thus ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) :: thesis: ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M )
proof
assume x in M ; :: thesis: x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f as Morphism of C by ;
set a9 = dom f9;
set b9 = cod f9;
( the Source of CatStr(# O,M,d,c,p #) . f = the Source of C . f9 & the Target of CatStr(# O,M,d,c,p #) . f = the Target of C . f9 ) by A2;
then ( f in Hom ((dom f9),(cod f9)) & Hom ((dom f9),(cod f9)) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) ;
hence x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4; :: thesis: verum
end;
assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: x in M
then consider X being set such that
A3: x in X and
A4: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;
consider a9, b9 being Object of C such that
A5: X = Hom (a9,b9) and
A6: ( a9 in O & b9 in O ) by A4;
reconsider a = a9, b = b9 as Object of CatStr(# O,M,d,c,p #) by A6;
Hom (a,b) = Hom (a9,b9) by ;
hence x in M by A3, A5; :: thesis: verum
end;
hence M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:2; :: thesis: ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )
then reconsider d9 = the Source of C | M, c9 = the Target of C | M as Function of M,O by Th16;
set p9 = the Comp of C || M;
now :: thesis: for f being Element of M holds d . f = d9 . f
let f be Element of M; :: thesis: d . f = d9 . f
d . f = the Source of C . f by A2;
hence d . f = d9 . f by FUNCT_1:49; :: thesis: verum
end;
hence d = the Source of C | M by FUNCT_2:63; :: thesis: ( c = the Target of C | M & p = the Comp of C || M )
now :: thesis: for f being Element of M holds c . f = c9 . f
let f be Element of M; :: thesis: c . f = c9 . f
c . f = the Target of C . f by A2;
hence c . f = c9 . f by FUNCT_1:49; :: thesis: verum
end;
hence c = the Target of C | M by FUNCT_2:63; :: thesis: p = the Comp of C || M
now :: thesis: ( dom p = dom ( the Comp of C || M) & ( for x being object st x in dom p holds
p . x = ( the Comp of C || M) . x ) )
A7: dom p c= [:M,M:] by RELAT_1:def 18;
A8: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
the Comp of CatStr(# O,M,d,c,p #) c= the Comp of C by ;
then dom p c= dom the Comp of C by GRFUNC_1:2;
then A9: dom p c= dom ( the Comp of C || M) by ;
dom ( the Comp of C || M) c= dom p
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ( the Comp of C || M) or x in dom p )
assume A10: x in dom ( the Comp of C || M) ; :: thesis: x in dom p
then x in [:M,M:] by ;
then consider g, f being Element of M such that
A11: x = [g,f] by DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f, g9 = g as Morphism of C by ;
[g,f] in dom the Comp of C by ;
then A12: dom g9 = cod f9 by CAT_1:15;
( cod f = cod f9 & dom g = dom g9 ) by ;
hence x in dom p by ; :: thesis: verum
end;
hence dom p = dom ( the Comp of C || M) by ; :: thesis: for x being object st x in dom p holds
p . x = ( the Comp of C || M) . x

let x be object ; :: thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x )
assume A13: x in dom p ; :: thesis: p . x = ( the Comp of C || M) . x
then consider g, f being Element of M such that
A14: x = [g,f] by ;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ;
A15: dom g = cod f by ;
reconsider f9 = f, g9 = g as Morphism of C by ;
A16: ( cod f = cod f9 & dom g = dom g9 ) by ;
p . x = p . (g,f) by A14;
hence p . x = g (*) f by
.= g9 (*) f9 by A1, A15, Th7
.= the Comp of C . (g9,f9) by
.= ( the Comp of C || M) . x by ;
:: thesis: verum
end;
hence p = the Comp of C || M by FUNCT_1:2; :: thesis: verum