let C be category; :: thesis: 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

let o1, o2 be Object of C; :: thesis: 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

let m, m9 be Morphism of o1,o2; :: thesis: ( m is _zero & m9 is _zero & ex O being Object of C st O is _zero implies m = m9 )

assume that

A1: m is _zero and

A2: m9 is _zero ; :: thesis: ( for O being Object of C holds not O is _zero or m = m9 )

given O being Object of C such that A3: O is _zero ; :: thesis: m = m9

set n = the Morphism of O,O;

set b = the Morphism of O,o2;

set a = the Morphism of o1,O;

thus m = ( the Morphism of O,o2 * (( the Morphism of O,O ") * the Morphism of O,O)) * the Morphism of o1,O by A1, A3

.= m9 by A2, A3 ; :: thesis: verum

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

let o1, o2 be Object of C; :: thesis: 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

let m, m9 be Morphism of o1,o2; :: thesis: ( m is _zero & m9 is _zero & ex O being Object of C st O is _zero implies m = m9 )

assume that

A1: m is _zero and

A2: m9 is _zero ; :: thesis: ( for O being Object of C holds not O is _zero or m = m9 )

given O being Object of C such that A3: O is _zero ; :: thesis: m = m9

set n = the Morphism of O,O;

set b = the Morphism of O,o2;

set a = the Morphism of o1,O;

thus m = ( the Morphism of O,o2 * (( the Morphism of O,O ") * the Morphism of O,O)) * the Morphism of o1,O by A1, A3

.= m9 by A2, A3 ; :: thesis: verum