let C be Category; :: thesis: for O being non empty Subset of the carrier of C

for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

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: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) )

assume A2: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

set c = the Target of C | M;

set p = the Comp of C || M;

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:61;

A8: rng ( the Source of C | M) c= O

then A12: dom ( the Target of C | M) = M by A6, RELAT_1:62;

A13: dom ( the Target of C | M) = (dom the Target of C) /\ M by RELAT_1:61;

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

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:4; :: thesis: the Comp of C || M is PartFunc of [:M,M:],M

A17: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;

A18: 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

thus verum ; :: thesis: verum

for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

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: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M ) )

assume A2: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: ( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

A3: now :: thesis: for f being Morphism of C st f in M holds

( dom f in O & cod f in O )

set d = the Source of C | M;( dom f in O & cod f in O )

let f be Morphism of C; :: thesis: ( f in M implies ( dom f in O & cod f in O ) )

assume f in M ; :: thesis: ( dom f in O & cod f in O )

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:1; :: thesis: verum

end;assume f in M ; :: thesis: ( dom f in O & cod f in O )

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:1; :: thesis: verum

set c = the Target of C | M;

set p = the Comp of C || M;

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:61;

A8: rng ( the Source of C | M) c= O

proof

A11:
M is non empty Subset of the carrier' of C
by A2, Th15;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Source of C | M) or y in O )

assume y in rng ( the Source of C | M) ; :: thesis: y in O

then consider x being object such that

A9: x in dom ( the Source of C | M) and

A10: y = ( the Source of C | M) . x by FUNCT_1:def 3;

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:47, XBOOLE_0:def 4;

hence y in O by A3, A10; :: thesis: verum

end;assume y in rng ( the Source of C | M) ; :: thesis: y in O

then consider x being object such that

A9: x in dom ( the Source of C | M) and

A10: y = ( the Source of C | M) . x by FUNCT_1:def 3;

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:47, XBOOLE_0:def 4;

hence y in O by A3, A10; :: thesis: verum

then A12: dom ( the Target of C | M) = M by A6, RELAT_1:62;

A13: dom ( the Target of C | M) = (dom the Target of C) /\ M by RELAT_1:61;

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

proof

dom ( the Source of C | M) = M
by A1, A11, RELAT_1:62;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Target of C | M) or y in O )

assume y in rng ( the Target of C | M) ; :: thesis: y in O

then consider x being object such that

A15: x in dom ( the Target of C | M) and

A16: y = ( the Target of C | M) . x by FUNCT_1:def 3;

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:47, XBOOLE_0:def 4;

hence y in O by A3, A16; :: thesis: verum

end;assume y in rng ( the Target of C | M) ; :: thesis: y in O

then consider x being object such that

A15: x in dom ( the Target of C | M) and

A16: y = ( the Target of C | M) . x by FUNCT_1:def 3;

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:47, XBOOLE_0:def 4;

hence y in O by A3, A16; :: thesis: verum

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:4; :: thesis: the Comp of C || M is PartFunc of [:M,M:],M

A17: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;

A18: 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

proof

hence
the Comp of C || M is PartFunc of [:M,M:],M
by A17, RELSET_1:4, XBOOLE_1:17; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Comp of C || M) or y in M )

assume y in rng ( the Comp of C || M) ; :: thesis: y in M

then consider x being object such that

A19: x in dom ( the Comp of C || M) and

A20: y = ( the Comp of C || M) . x by FUNCT_1:def 3;

A21: x in dom the Comp of C by A17, A19, XBOOLE_0:def 4;

then consider g, f being Morphism of C such that

A22: x = [g,f] by A18, DOMAIN_1:1;

A23: [g,f] in [:M,M:] by A17, A19, A22, XBOOLE_0:def 4;

then g in M by ZFMISC_1:87;

then A24: cod g in O by A3;

dom g = cod f by A21, A22, CAT_1:15;

then A25: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by CAT_1:17;

f in M by A23, ZFMISC_1:87;

then dom f in O by A3;

then A26: 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 A24, A25;

A27: g (*) f in Hom ((dom (g (*) f)),(cod (g (*) f))) ;

( the Comp of C || M) . x = the Comp of C . (g,f) by A19, A22, FUNCT_1:47

.= g (*) f by A21, A22, CAT_1:def 1 ;

hence y in M by A2, A20, A26, A27, TARSKI:def 4; :: thesis: verum

end;assume y in rng ( the Comp of C || M) ; :: thesis: y in M

then consider x being object such that

A19: x in dom ( the Comp of C || M) and

A20: y = ( the Comp of C || M) . x by FUNCT_1:def 3;

A21: x in dom the Comp of C by A17, A19, XBOOLE_0:def 4;

then consider g, f being Morphism of C such that

A22: x = [g,f] by A18, DOMAIN_1:1;

A23: [g,f] in [:M,M:] by A17, A19, A22, XBOOLE_0:def 4;

then g in M by ZFMISC_1:87;

then A24: cod g in O by A3;

dom g = cod f by A21, A22, CAT_1:15;

then A25: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by CAT_1:17;

f in M by A23, ZFMISC_1:87;

then dom f in O by A3;

then A26: 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 A24, A25;

A27: g (*) f in Hom ((dom (g (*) f)),(cod (g (*) f))) ;

( the Comp of C || M) . x = the Comp of C . (g,f) by A19, A22, FUNCT_1:47

.= g (*) f by A21, A22, CAT_1:def 1 ;

hence y in M by A2, A20, A26, A27, TARSKI:def 4; :: thesis: verum

thus verum ; :: thesis: verum