theorem :: CAT_4:59

for C being Cocartesian_category
for a being Object of C holds Hom ((EmptyMS C),a) = {(init a)}