let C be Category; :: thesis:
let O be non empty Subset of the carrier of C; :: thesis:
set H = { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ;
let M be non empty set ; :: thesis:
assume A1: M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis:
set d = the Source of C | M;
set c = the Target of C | M;
set p = the Comp of C || M;
set i = the Id of C | O;

A2: now

let f be Morphism of C; :: thesis:
assume f in M ; :: thesis:
then consider X being set such that
A3: f in X and
A4: X in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;
ex a, b being Object of C st
( X = Hom a,b & a in O & b in O ) by A4;
hence ( dom f in O & cod f in O ) by A3, CAT_1:18; :: thesis:

end;

A5: ( dom the Source of C = the carrier' of C & dom the Target of C = the carrier' of C ) by FUNCT_2:def 1;
A6: ( dom (the Source of C | M) = (dom the Source of C) /\ M & dom (the Target of C | M) = (dom the Target of C) /\ M ) by RELAT_1:90;
A7: M is non empty Subset of the carrier' of C by A1, Th28;

thus ( dom (the Source of C | M) = M & dom (the Target of C | M) = M ) by A5, A7, RELAT_1:91; :: thesis:
thus rng (the Source of C | M) c= O :: thesis:

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (the Source of C | M) ; :: thesis:
then consider x being set such that
A8: x in dom (the Source of C | M) and
A9: y = (the Source of C | M) . x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A5, A6, A8, XBOOLE_0:def 4;
( (the Source of C | M) . f = dom f & f in M ) by A6, A8, FUNCT_1:70, XBOOLE_0:def 4;
hence y in O by A2, A9; :: thesis:

end;

thus rng (the Target of C | M) c= O :: thesis:

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (the Target of C | M) ; :: thesis:
then consider x being set such that
A10: x in dom (the Target of C | M) and
A11: y = (the Target of C | M) . x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A5, A6, A10, XBOOLE_0:def 4;
( (the Target of C | M) . f = cod f & f in M ) by A6, A10, FUNCT_1:70, XBOOLE_0:def 4;
hence y in O by A2, A11; :: thesis:

end;

hence ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O ) by FUNCT_2:def 1, RELSET_1:11; :: thesis:
thus the Comp of C || M is PartFunc of [:M,M:],M :: thesis:

A12: dom the Comp of C c= [:the carrier' of C,the carrier' of C:] by RELAT_1:def 18;
A13: dom (the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:90;
rng (the Comp of C || M) c= M

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (the Comp of C || M) ; :: thesis:
then consider x being set such that
A14: x in dom (the Comp of C || M) and
A15: y = (the Comp of C || M) . x by FUNCT_1:def 5;
A16: x in dom the Comp of C by A13, A14, XBOOLE_0:def 4;
then consider g, f being Morphism of C such that
A17: x = [g,f] by A12, DOMAIN_1:9;

thus (the Comp of C || M) . x = the Comp of C . g,f by A14, A17, FUNCT_1:70
.= g * f by A16, A17, CAT_1:def 4 ; :: thesis:

[g,f] in [:M,M:] by A13, A14, A17, XBOOLE_0:def 4;
then ( f in M & g in M ) by ZFMISC_1:106;
hence ( dom f in O & cod g in O ) by A2; :: thesis:
dom g = cod f by A16, A17, CAT_1:40;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by CAT_1:42; :: thesis:

end;

hence ( Hom (dom (g * f)),(cod (g * f)) in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } & g * f in Hom (dom (g * f)),(cod (g * f)) ) ; :: thesis:

end;

hence y in M by A1, A15, TARSKI:def 4; :: thesis:

end;

hence the Comp of C || M is PartFunc of [:M,M:],M by A13, RELSET_1:11, XBOOLE_1:17; :: thesis:

end;

now

A18: dom the Id of C = the carrier of C by FUNCT_2:def 1;
A19: dom (the Id of C | O) = (dom the Id of C) /\ O by RELAT_1:90;
thus dom (the Id of C | O) = O by A18, RELAT_1:91; :: thesis:
thus rng (the Id of C | O) c= M :: thesis:

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (the Id of C | O) ; :: thesis:
then consider x being set such that
A20: x in dom (the Id of C | O) and
A21: y = (the Id of C | O) . x by FUNCT_1:def 5;
reconsider a = x as Object of C by A19, A20;
( (the Id of C | O) . a = id a & a in O ) by A19, A20, FUNCT_1:70, XBOOLE_0:def 4;
then ( (the Id of C | O) . a in Hom a,a & Hom a,a in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ) by CAT_1:55;
hence y in M by A1, A21, TARSKI:def 4; :: thesis:

end;

hence the Id of C | O is Function of O,M by FUNCT_2:def 1, RELSET_1:11; :: thesis: