theorem :: CAT_3:63

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}