theorem Th9: :: CAT_2:13

for C being Category
for E being Subcategory of C holds id E is Functor of E,C