theorem Th64: :: CAT_3:64

for y being set
for C being Category
for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}