let C be Category; :: thesis:
let O be non empty Subset of the carrier of C; :: thesis:
let M be non empty set ; :: thesis:
let d, c be Function of M,O; :: thesis:
let p be PartFunc of [:M,M:],M; :: thesis:
let i be Function of O,M; :: thesis:
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,i #);
assume that
A1: CatStr(# O,M,d,c,p,i #) is Subcategory of C and
A2: for a, b being Object of CatStr(# O,M,d,c,p,i #)
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' ; :: according to CAT_2:def 6 :: thesis:
A3: for f being Morphism of CatStr(# O,M,d,c,p,i #) 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,i #); :: thesis:
reconsider f' = f as Morphism of C by A1, Th14;
( dom f = dom f' & cod f = cod f' & dom f = the Source of CatStr(# O,M,d,c,p,i #) . f & dom f' = the Source of C . f' & cod f = the Target of CatStr(# O,M,d,c,p,i #) . f & cod f' = the Target of C . f' ) by A1, Th15;
hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; :: thesis:

end;

now

let x be set ; :: thesis:
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:

proof

assume x in M ; :: thesis:
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f' = f as Morphism of C by A1, Th14;
set a' = dom f';
set b' = cod f';
( the Source of CatStr(# O,M,d,c,p,i #) . f = the Source of C . f' & the Target of CatStr(# O,M,d,c,p,i #) . f = the Target of C . f' ) by A3;
then ( f in Hom (dom f'),(cod f') & Hom (dom f'),(cod f') 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:

end;

assume x in union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis:
then consider X being set such that
A4: x in X and
A5: X in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;
consider a', b' being Object of C such that
A6: X = Hom a',b' and
A7: ( a' in O & b' in O ) by A5;
reconsider a = a', b = b' as Object of CatStr(# O,M,d,c,p,i #) by A7;
Hom a,b = Hom a',b' by A2;
hence x in M by A4, A6; :: thesis:

end;

hence A8: M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:2; :: thesis:
then reconsider d' = the Source of C | M, c' = the Target of C | M as Function of M,O by Th29;

now

let f be Element of M; :: thesis:

now

thus d . f = the Source of C . f by A3; :: thesis:
thus f in M ; :: thesis:
f is Morphism of C by A1, Th14;
then f in the carrier' of C ;
hence f in dom the Source of C by FUNCT_2:def 1; :: thesis:

end;

hence d . f = d' . f by FUNCT_1:72; :: thesis:

end;

hence d = the Source of C | M by FUNCT_2:113; :: thesis:

now

let f be Element of M; :: thesis:

now

thus c . f = the Target of C . f by A3; :: thesis:
thus f in M ; :: thesis:
f is Morphism of C by A1, Th14;
then f in the carrier' of C ;
hence f in dom the Target of C by FUNCT_2:def 1; :: thesis:

end;

hence c . f = c' . f by FUNCT_1:72; :: thesis:

end;

hence c = the Target of C | M by FUNCT_2:113; :: thesis:
set p' = the Comp of C || M;

now

A9: dom p c= [:M,M:] by RELAT_1:def 18;
A10: dom (the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:90;
A11: dom (the Comp of C || M) c= dom p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A12: x in dom (the Comp of C || M) ; :: thesis:
then x in [:M,M:] by A10, XBOOLE_0:def 4;
then consider g, f being Element of M such that
A13: x = [g,f] by DOMAIN_1:9;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f' = f, g' = g as Morphism of C by A1, Th14;
[g,f] in dom the Comp of C by A10, A12, A13, XBOOLE_0:def 4;
then ( cod f = cod f' & dom g = dom g' & dom g' = cod f' ) by A1, Th15, CAT_1:40;
hence x in dom p by A1, A13, CAT_1:40; :: thesis:

end;

the Comp of CatStr(# O,M,d,c,p,i #) c= the Comp of C by A1, Def4;
then dom p c= dom the Comp of C by GRFUNC_1:8;
then A14: dom p c= dom (the Comp of C || M) by A9, A10, XBOOLE_1:19;
hence dom p = dom (the Comp of C || M) by A11, XBOOLE_0:def 10; :: thesis:
let x be set ; :: thesis:
assume A15: x in dom p ; :: thesis:
then consider g, f being Element of M such that
A16: x = [g,f] by A9, DOMAIN_1:9;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f' = f, g' = g as Morphism of C by A1, Th14;
A17: ( cod f = cod f' & dom g = dom g' & dom g = cod f ) by A1, A15, A16, Th15, CAT_1:40;
p . x = p . g,f by A16;
hence p . x = g * f by A1, A17, CAT_1:41
.= g' * f' by A1, A17, Th17
.= the Comp of C . g',f' by A17, CAT_1:41
.= (the Comp of C || M) . x by A14, A15, A16, FUNCT_1:70 ;
:: thesis:

end;

hence p = the Comp of C || M by FUNCT_1:9; :: thesis:
reconsider i' = the Id of C | O as Function of O,M by A8, Th29;

now

let a be Element of O; :: thesis:

now

reconsider a' = a as Object of C ;
reconsider b = a as Object of CatStr(# O,M,d,c,p,i #) ;
( id b = id a' & id b = the Id of CatStr(# O,M,d,c,p,i #) . b & id a' = the Id of C . a' ) by A1, Def4;
hence i . a = the Id of C . a ; :: thesis:
thus a in O ; :: thesis:
a in the carrier of C ;
hence a in dom the Id of C by FUNCT_2:def 1; :: thesis:

end;

hence i . a = i' . a by FUNCT_1:72; :: thesis:

end;

hence i = the Id of C | O by FUNCT_2:113; :: thesis: