theorem Th16: :: CAT_2:20

for C being Category
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 )