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 ) } ;
A1: dom the Source of C = the carrier' of C by FUNCT_2:def 1;
let M be non empty set ; :: thesis:
assume A2: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis:

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

end;

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;
A6: dom the Target of C = the carrier' of C by FUNCT_2:def 1;
A7: dom ( the Source of C | M) = (dom the Source of C) /\ M by RELAT_1:90;
A8: rng ( the Source of C | M) c= O

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
A9: x in dom ( the Source of C | M) and
A10: y = ( the Source of C | M) . x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A1, A7, A9, XBOOLE_0:def 4;
( ( the Source of C | M) . f = dom f & f in M ) by A7, A9, FUNCT_1:70, XBOOLE_0:def 4;
hence y in O by A3, A10; :: thesis:

end;

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
A15: x in dom ( the Target of C | M) and
A16: y = ( the Target of C | M) . x by FUNCT_1:def 5;
reconsider f = x as Morphism of C by A6, A13, A15, XBOOLE_0:def 4;
( ( the Target of C | M) . f = cod f & f in M ) by A13, A15, FUNCT_1:70, XBOOLE_0:def 4;
hence y in O by A3, A16; :: thesis:

end;

dom ( the Source of C | M) = M by A1, A11, RELAT_1:91;
hence ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O ) by A8, A14, A12, FUNCT_2:def 1, RELSET_1:11; :: thesis:
A17: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:90;
A18: dom ( the Id of C | O) = (dom the Id of C) /\ O by RELAT_1:90;
A19: rng ( the Id of C | O) c= M

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 A18, A20;
( the Id of C | O) . a = id a by A20, FUNCT_1:70;
then A22: ( the Id of C | O) . a in Hom (a,a) by CAT_1:55;
a in O by A18, A20, XBOOLE_0:def 4;
then Hom (a,a) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
hence y in M by A2, A21, A22, TARSKI:def 4; :: thesis:

end;

A23: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def 18;
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
A24: x in dom ( the Comp of C || M) and
A25: y = ( the Comp of C || M) . x by FUNCT_1:def 5;
A26: x in dom the Comp of C by A17, A24, XBOOLE_0:def 4;
then consider g, f being Morphism of C such that
A27: x = [g,f] by A23, DOMAIN_1:9;
A28: [g,f] in [:M,M:] by A17, A24, A27, XBOOLE_0:def 4;
then g in M by ZFMISC_1:106;
then A29: cod g in O by A3;
dom g = cod f by A26, A27, CAT_1:40;
then A30: ( dom (g * f) = dom f & cod (g * f) = cod g ) by CAT_1:42;
f in M by A28, ZFMISC_1:106;
then dom f in O by A3;
then A31: Hom ((dom (g * f)),(cod (g * f))) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A29, A30;
A32: g * f in Hom ((dom (g * f)),(cod (g * f))) ;
( the Comp of C || M) . x = the Comp of C . (g,f) by A24, A27, FUNCT_1:70
.= g * f by A26, A27, CAT_1:def 4 ;
hence y in M by A2, A25, A31, A32, TARSKI:def 4; :: thesis:

end;