for C being category
for o1, o2 being Object of C
for m, m9 being Morphism of o1,o2 st m is _zero & m9 is _zero & ex O being Object of C st O is _zero holds
m = m9