theorem :: ALTCAT_3:30

for C being category
for o1, o2, o3 being Object of C
for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero