for C being Cocartesian_category
for a being Object of C
for f1, f2 being Morphism of EmptyMS C,a holds f1 = f2