theorem Th5: :: NATTRA_1:9

for A being Category
for O being non empty Subset of the carrier of A
for M being non empty Subset of the carrier' of A st ( for o being Element of A st o in O holds
id o in M ) holds
for DOM, COD being Function of M,O st DOM = the Source of A | M & COD = the Target of A | M holds
for COMP being PartFunc of [:M,M:],M st COMP = the Comp of A || M holds
CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A