for A, B being category
for C being non empty subcategory of A
for F being contravariant Functor of A,B
for a, b being Object of A
for c, d being Object of C st c = a & d = b & <^c,d^> <> {} holds
for f being Morphism of a,b
for g being Morphism of c,d st g = f holds
(F | C) . g = F . f