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 A1, Th4;
( dom f = dom f9 & cod f = cod f9 ) by A1, Th5;
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 A1, Th4;
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 A1, Def6;
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 A1, Def4;
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 A7, A8, XBOOLE_1:19;
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 A8, XBOOLE_0:def 4;
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 A1, Th4;
[g,f] in dom the Comp of C by A8, A10, A11, XBOOLE_0:def 4;
then A12: dom g9 = cod f9 by CAT_1:15;
( cod f = cod f9 & dom g = dom g9 ) by A1, Th5;
hence x in dom p by A1, A11, A12, CAT_1:15; :: thesis: verum

end;

hence dom p = dom ( the Comp of C || M) by A9, XBOOLE_0:def 10; :: 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 A7, DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p #) ;
A15: dom g = cod f by A1, A13, A14, CAT_1:15;
reconsider f9 = f, g9 = g as Morphism of C by A1, Th4;
A16: ( cod f = cod f9 & dom g = dom g9 ) by A1, Th5;
p . x = p . (g,f) by A14;
hence p . x = g (*) f by A1, A15, CAT_1:16
.= g9 (*) f9 by A1, A15, Th7
.= the Comp of C . (g9,f9) by A16, A1, A13, A14, CAT_1:15, CAT_1:16
.= ( the Comp of C || M) . x by A9, A13, A14, FUNCT_1:47 ;
:: thesis: verum

end;

hence p = the Comp of C || M by FUNCT_1:2; :: thesis: verum